Researched
Kepler Conjecture & Flyspeck
Thomas Hales's computer-assisted proof (1998) that stacked spheres fill at most 74% of space was checked line by line by the Flyspeck project (2014).
Open in the interactive tree →Hales announced the proof in August 1998 and Annals of Mathematics published its non-computer part in 2005, after referees said they were 99% certain of it. The Flyspeck project, using the proof assistants HOL Light and Isabelle, announced a complete formal proof on 10 August 2014, accepted by Forum of Mathematics, Pi in 2017.
Prerequisites
- Geometry (Euclid)~300 BC
- Four Colour Theorem Proved1976
Unlocks
- Formal Proofs (Lean, Rocq)2005-2026Flyspeck (2014) is an early full formalisation of a long computer-assisted proof