Concept
When the proof is too long for humans — the new mathematical methodology.
Understand it in one breath
"Reduce a theorem exhaustively to finitely many cases, then use a computer to verify every case." This differs from checking many examples. The 1976 Four Color Theorem, the 2014 Flyspeck formal verification of the Kepler conjecture, and the 2016 Boolean Pythagorean Triples result are prominent examples. Trust depends on the completeness of the reduction and on independently checking the program or proof certificate.
At a glance
Year | Theorem | Role of the computer | Scale |
|---|---|---|---|
1976 | Four Color Theorem | Checked a finite unavoidable set of configurations by program | Large-scale computation for its time |
1996 | Robbins conjecture (Boolean algebra) | EQP automated prover (McCune) | 8 days of automated search |
1998 | Kepler conjecture (sphere packing) | 5,000 inequalities + LP | Hales 1998 → Flyspeck 2014 |
2014 | Flyspeck (Hales verification) | Fully formal verification in Coq + HOL Light | Years of collaboration |
2016 | Boolean Pythagorean triples | SAT solver | About 200 terabytes of data generated during the computation |
2021+ | Lean and the Mathlib ecosystem | Collaborative formalization of theorems and libraries | Many collaborations, including formalization of the PFR theorem |
Trust in a computer-assisted proof depends less on a computer/no-computer divide than on complete reduction, inspectable code or certificates, independent rechecking, and a clearly identified small trusted base.
Key formula
Key moments
The Four Color Theorem — a landmark computer-assisted proof
Appel and Haken combined a finite reduction with extensive computer checking. The result made the inspectability of computer-dependent proofs a central question.
The Kepler conjecture
Thomas Hales proved that no arrangement of equal spheres is denser than the familiar close-packed arrangements. Checking the proof required years of computer work.
Boolean Pythagorean triples — 200 terabytes
Marijn Heule, Oliver Kullmann, and Victor Marek produced an enormous computer-assisted proof with a 200-terabyte certificate — far beyond what a human could read line by line.
Proof assistants such as Lean
Proof assistants such as Lean, Coq, and Isabelle let computers check formal proofs down to their logical foundations, and their combination with AI is opening a new era.
Modern applications
The Four Color Theorem, the Kepler conjecture, Boolean Pythagorean triples, large-scale checks of Riemann zeros, and formal verification of critical systems.
Beyond MathVoyage
Loading…