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

Proposed dates, still to be confirmed. Each session lasts two hours.

TBP