Users enter their proofs in the assistant's proof language, like a programming language, contributing to and building on results from formal libraries. Contemporary proof assistants with substantial mathematical libraries include the following:
Several researchers are also exploring foundations based on homotopy type theory, with associated proof assistants and libraries.
Landmarks
Two early landmarks in the field were the verification of the Feit–Thompson Odd Order Theorem, completed by Gonthier et al. in 2014, and the verification of the Kepler conjecture, completed by Hales et al. in 2016. Notable mathematical formalization projects since then include:
- The Liquid Tensor Experiment
- The Sphere Eversion Theorem
- The Polynomial Freiman–Ruzsa Theorem
- Upper Bounds to Ramsey's theorem (in Lean, and then Isabelle)
- Carleson's Theorem
- Higher-Dimensional Sphere Packing
- Fermat's Last Theorem
Most of these are collaborative projects that use Patrick Massot's blueprint software.
Background reading
For more on formalization and proof assistants, we recommend:
- History of Interactive Theorem Proving, by Harrison, Urban, and Wiedijk
- What is the Point of Computers? A Question for Pure Mathematicians, by Buzzard
- Mathematics and the Formal Turn, by Avigad
- Algorithm and Abstraction in Formal Mathematics, by Macbeth
Getting started
Most proof assistants have online documentation, tutorials, and user communities. Mathematics is especially active in the Lean community — see the Lean Community web pages for information, documentation, and tutorials. The Lean Zulip social media platform is welcoming to newcomers.