Aug 10, 2014
Kepler conjecture, Flyspeck
Model / AI: Flyspeck (no ML)
machine-checked
Hales's proof fully verified in HOL Light and Isabelle; journal version in Forum of Mathematics Pi (2017).
Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.