A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang and, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron and, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias, Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev,, An Hoai Thi Ta
TL;DR
This paper presents a formal proof of the Kepler conjecture on dense sphere packings, utilizing HOL Light and Isabelle proof assistants, marking the completion of the Flyspeck project.
Contribution
It provides the first fully formalized proof of the Kepler conjecture, combining two proof assistants and documenting the Flyspeck project's results.
Findings
Formal proof verified in HOL Light and Isabelle
Completion of the Flyspeck project
Official published account of the proof
Abstract
This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.