Difference between revisions
kepler-conjecture
Source +0 −0
… 30 unchanged lines
Revision 27 as rendered
Hales reduced the problem to thousands of inequalities checked by computer. Referees said they were 99% certain it was right and could not be fully certain. Hales answered by leading the Flyspeck project, which completed a formal proof in HOL Light and Isabelle in 2014. It became the standard example of formal verification settling a proof that humans could not referee.
Evidence tier V3 is the import default for a result the curation records as settled in the published record. No formal proof or certificate is attached to this page yet.
Posed 1611, Johannes Kepler. Closed 1998, Thomas Hales with Samuel Ferguson; formally verified 2014.
What would settle it
Formal proof: Flyspeck (HOL Light, Isabelle)
Related problems
- The original curation links this problem to Sphere packing in dimensions 8 and 24; the argument for the link has not been written yet.