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:
tba