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:
-
Ablation: A Tool for Probing Creativity and Constraint in Formalization Agents
Zhengqin Fan, Simon DeDeo
-
Automatically translating definitions and proofs
Jovan Gerbscheid
-
The sphere packing project
Sidharth Hariharan
-
Formalising Polychromatic Colourings of Integers
Bhavik Mehta
-
The Generalized Quantum Stein's Lemma
Alex Meiburg
-
Formalizing Quasi-Borel Spaces in Lean 4
Anthony Vandikas, Kiarash Sotoudeh
-
Reflections on Trusting Lean
Lorenzo Bresolin, Marcello Mamino