A Brief History of Computer-Assisted Mathematics
Timeline of some events in computer-assisted mathematics and formalization in proof assistants
With the recent rise of proof assistants and AI systems, computers are set to be indispensable tools for mathematicians in the future. Let’s take a look at important moments in the history of computer-assisted mathematics, from symbolic systems and human formalizations to modern AI and autoformalization tools.
Timeline
- 1956Logic Theorist proves 38 theorems in Principia Mathematica
- 1967Common Fixed-Point Problem is disproved with a computer program (independently alongside a human proof)
- 1986Feigenbaum Constants' Universality is proved with computer-assisted interval arithmetic
- 1986Gödel's Incompleteness Theorem is formalized in Nqthm
- 1989Four-Color Theorem becomes one of the first major computer-assisted proofs
- 1989Lam's Problem is solved using a supercomputer
- 1991Finite Projective Plane of Order 10 is proven impossible using a computer calculation
- 1996Robbins Conjecture is solved by an equational prover (EQP)
- 1998Kepler Conjecture is solved via a computer proof-by-exhaustion
- 2005Four-Color Theorem is formalized in Rocq
- 2005Prime Number Theorem is formalized in Isabelle
- 2005Jordan Curve Theorem is formalized in HOL and Mizar (separately)
- 2012Odd Order Theorem is formalized in Rocq
- 2014Kepler Conjecture is formalized in Isabelle and HOL
- 2016Boolean Pythagorean Triples Problem is solved using a SAT Solver
- 2017Schur Number Five is found using a SAT Solver with a 2PB proof
- 2019Keller's Conjecture is resolved (last 7-dim case) using a SAT Solver
- 2020Perfectoid Spaces is formalized in Lean
- 2022Liquid Tensor Experiment is completed in Lean
- 2022Unit Fractions Density Conjecture is formalized in Lean
- 2022Polynomial Freiman-Ruzsa Conjecture is formalized in Lean within 3 weeks of being solved
- 2022Sphere Eversion is formalized in Lean
- 2023Packing Chromatic Number of Infinite Square Grid is found using a SAT Solver
- 2024Equational Theories Project is completed in Lean
- 2024BB(5) (Busy Beaver) is formalized in Rocq
- 2025AlphaEvolve improves bounds on several math problems
- 2026Sphere Packing in 8 & 24-dim is auto-formalized (starting from a partial human formalization) in Lean by Gauss
Apart from this, there are math libraries in proof assistants like Lean, Isabelle and Rocq that have formalized most of undergrad math and some graduate math.
Notes
This list will be updated with time. The criteria for choosing the currently listed events are purely subjective. Let me know if any other important events should be added to this list.
There’s a lot of progress being made in autoformalization of math since last year. These will be included in the timeline soon.