Proofs as programs in Lean
This is the website for a discussion group on using Lean, held at NCTS in May-June 2025.
Lean is a programming language designed for writing mathematical proofs. It allows the computer to help verify that your proof is correct. In particular, writing a proof using Lean should “make it harder to prove things that are not true.” (borrowing words from Leslie Lamport.)
For this discussion group, we will use code in this github repository.
Project topics
For details, see the About section.
Newton’s theorem on real roots
Cauchy interlacing theorem
Puiseux’s theorem
Descartes’s rule of signs
Sturm’s theorem for polynomial roots
Newton’s theorem for valued fields
Lean resources
Official documentation: https://leanprover-community.github.io/mathlib4_docs/
Quick search
Human-language search: Zulip chat
LLM-assisted human-language search: Leansearch
Source code search (type signatures, etc.): Loogle
Textbooks
- Hitchhiker’s Guide to Logical Verification, by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Johannes Hölzl, and Jannis Limperg
Philosophical commentary
- Is mathematics obsolete?, Jeremy Avigad
Website built using Just the Class, a template that extends the popular Just the Docs theme, which provides a robust and thoroughly-tested foundation for your website.