Mathematics in Lean — special session at ICMS 2026
A special session on mathematics in the Lean theorem prover at the International Congress on Mathematical Software 2026, Waterloo, Ontario.
The “Mathematics in Lean” special session at the International Congress on Mathematical Software (ICMS 2026), organised by Matthew Ballard, Rémy Degenne and Damiano Testa.
The session covers research on mathematical formalization in Lean, an interactive theorem prover for expressing and formally verifying mathematical results, together with new Lean tools and software for writing mathematics. It highlights recent formalizations, Lean's growing adoption among mathematicians, and its role in validating AI-generated mathematical content.
Seven talks take place on Thursday 23 July:
- Lorenzo Bresolin and Marcello Mamino — Reflections on Trusting Lean
- Zhengqin Fan and Simon DeDeo — Ablation: A Tool for Probing Creativity and Constraint in Formalization Agents
- Jovan Gerbscheid — Automatically translating definitions and proofs
- Sidharth Hariharan — Progress in Formalising Sphere Packing in Dimension 8
- Bhavik Mehta — Formalising Polychromatic Colourings of Integers
- Alex Meiburg — The Generalized Quantum Stein's Lemma
- Anthony Vandikas and Kiarash Sotoudeh — Formalizing Quasi-Borel Spaces in Lean 4
Full schedule and abstracts are on the session page; see ICMS 2026 for the congress itself.
ICMS 2026 runs 20–23 July 2026 at Wilfrid Laurier University and the University of Waterloo in Waterloo, Ontario. It is a satellite meeting of the International Congress of Mathematicians, held the following week in Philadelphia.