Researched
Four Colour Theorem Proved
Appel and Haken prove (1976) that four colours suffice for any map, the first major theorem proved with a computer.
Open in the interactive tree →The proof reduced the problem to about 1,900 configurations that a computer checked, which started a debate on whether such a proof counts. Gonthier's fully formal verification in Coq (2005) answered the doubt and pointed to today's machine-checked mathematics.
Prerequisites
Unlocks
- Kepler Conjecture & Flyspeck1998-2014
- Formal Proofs (Lean, Rocq)2005-2026Gonthier's formal proof of the four colour theorem (2005) was a landmark of machine-checked proof
- All Mathematics Machine-CheckedopenThe debate over the computer proof pushed the goal of fully machine-checked mathematics