Mathematics in Lean
Session Organizers:
Session Abstract:
This session covers new research in mathematical formalization using Lean as well as new Lean tools for writing mathematics.
Lean is an interactive theorem prover, in which one can express mathematical results and check them formally.
It is increasingly popular among mathematicians and is used to formalize new research.
It is also a programming language, and one can write tools in Lean that accelerate mathematical formalization.
Lean is also used extensively to verify AI-generated output.
The aim of the session is to highlight new research done in Lean and to present new tools and software that improve the capabilities of Lean for mathematical developments, both with presentations and tutorials.
Session Talks:
Thursday 23 July 10:30
The sphere packing project
Sidharth Hariharan
Thursday 23 July 11:00
Ablation: A Tool for Probing Creativity and Constraint in Formalization Agents
Zhengqin Fan, Simon DeDeo
Thursday 23 July 11:30
Automatically translating definitions and proofs
Jovan Gerbscheid
Thursday 23 July 14:00
Formalising Polychromatic Colourings of Integers
Bhavik Mehta
Thursday 23 July 14:30
The Generalized Quantum Stein's Lemma
Alex Meiburg
Thursday 23 July 15:00
Formalizing Quasi-Borel Spaces in Lean 4
Anthony Vandikas, Kiarash Sotoudeh
Thursday 23 July 16:00
Reflections on Trusting Lean
Lorenzo Bresolin, Marcello Mamino