Seminarium Fizyki Materii Skondensowanej

The Lean programming language and interactive theorem has recently made headlines following the announcements of AI-assisted breakthroughs, including the solution to the Navier-Stokes Millennium Prize Problem and over 700 novel mathematical results, where Lean served as a formal verifier. While Large Language Models have made generating complex mathematical derivations and proofs easier than ever, ensuring that these results are genuinely rigorous and do not rely on hidden or incorrect assumptions, requires being able to read and understand the underlying Lean code. In this talk I will provide a practical introduction to Lean 4 language and give examples of how it can be used to formalize calculations in condensed matter physics.