You have probably heard of Lean, the language that is gaining prominence following recent advances in artificial intelligence in mathematics. Lean allows us to write definitions, theorems, and proofs in a way that enables a machine to rigorously verify their logical correctness. But there is an important caveat: a machine can certify that a proof is correct with respect to the formalized statement, but it cannot guarantee that this statement accurately captures the mathematical result we actually intended to prove. Ensuring that correspondence remains our responsibility.

It is easy to imagine that, before long, we will be reviewing papers whose main results are formalized in Lean. And as authors, we may also find ourselves asked by a referee to formalize a result if they consider the proof presented insufficiently convincing. In both cases, we will need to understand this language and know how to use it. Just as reading LaTeX is now part of our everyday working lives, reading Lean may soon become a standard skill for mathematicians. This course aims to offer a first introduction to this new world.

Lean is a proof assistant: you write definitions, theorems and proofs, and the computer checks them. Its library, Mathlib, already covers a good part of undergraduate and graduate mathematics. AI has made formalization much faster. This year alone saw Lean proofs of Fermat’s Last Theorem, of Viazovska’s sphere packing results in dimensions 8 and 24, and of the recent disproof of Erdős’s unit distance conjecture, with AI writing much of the code. OpenAI also provided a Lean-checked solution to the Navier–Stokes Millennium Prize Problem.

This course is about how to do this for a theorem in your own area. The key skill is reading Lean statements, since you need to be able to tell whether the AI proved what you actually meant. Everyone is encouraged to bring a result of their own to work on.

Topics

• Lean and Mathlib basics: statements, proofs, tactics, finding things in Mathlib
• From paper to Lean: writing statements, and the usual mistakes
• AI tools: Claude Code, Aristotle, Prove2Me, Gauss, Tau Ceti, OctoSearch, with examples
• Working on your own theorem

Each session lasts two hours.

TBP