Formalization and Interactive Theorem Proving
Foundational work in the early twentieth century established that mathematical proofs can be formalized, that is, represented using formal mathematical languages and formal proof systems based on axioms and rules. Contemporary proof assistants enable the formalization of proofs in practice. 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, and there are associated proof assistants and libraries.
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 following:
- 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.
For more background on formalization and proof assistants, we recommend the following:
- 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, and you can find information, documentation, and tutorials on the Lean Community web pages. The Lean Zulip social media platform is welcoming to newcomers.