The Kepler Conjecture and Flyspeck — Machines Check a Proof Its Referees Could Not

Flyspeck was the international project that checked the proof of the Kepler conjecture step by step inside software known as proof assistants. It was completed on 10 August 2014. It existed because the proof Thomas Hales and Samuel Ferguson announced in 1998 could not be fully verified by the twelve referees the Annals of Mathematics assigned to it, even after years of work. A proof that its referees could only call nearly certain was finally given a guarantee by machine; that is what the event means.

If the four color theorem (1976) raised the question of whether a computer-assisted proof can be trusted, Flyspeck answered it on a very large proof: have a computer check the argument again, this time against the rules of logic.

A 1611 conjecture and a 1998 proof

According to the Flyspeck paper, Kepler stated in his 1611 booklet on the six-cornered snowflake that no packing of congruent balls in three-dimensional space has density greater than the face-centred cubic packing. The paper calls this the oldest problem in discrete geometry and notes that it formed part of Hilbert's 18th problem. In the 1950s László Fejes Tóth gave a coherent strategy for a proof and suggested that computers might be used.

Hales recalls that he and Sam Ferguson announced their solution in August 1998, posting it as a series of preprints on arXiv. The proof combined a vast case analysis with computer calculations, among them linear programs and nonlinear inequalities.

Twelve referees and "99 percent"

The Annals of Mathematics, Hales recalls, assigned a panel of twelve referees. According to George Szpiro's book on how mathematicians work, the effort was led by Gábor Fejes Tóth of the Rényi Institute in Budapest, and "In July 2002, Fejes Tóth reported that he and the other referees were 99 percent certain that the proof was sound." They had found no errors, but could not check everything, the computer calculations above all.

The Flyspeck paper says the delay in publication was caused by the difficulties the referees had in verifying a complex computer proof, and that "In the end, the proof was published without complete certification from the referees." It quotes Lagarias on the review: the nature of the proof "makes it hard for humans to check every step reliably." Looking back in 2022, Hales wrote that "Review dragged on for years, until the referees became exhausted and quit." The Annals issued a policy for computer-assisted proofs stating that the computer part may not be checked line by line.

Flyspeck: making a machine read the proof

Hales announced the formalisation project at the Joint Mathematics Meetings in Baltimore in January 2003. The name expands the acronym FPK, for the Formal Proof of Kepler. According to the Experimental Mathematics blog, Hales estimated it would take 20 years to complete.

To formalise a proof is to rebuild every step from the basic rules of logic and have a proof assistant check it. Flyspeck used two. HOL Light has a logical kernel of just a few hundred lines of code, and its design forces every deduction through that kernel. Isabelle was used to verify the classification of so-called tame plane graphs, one of the large computational parts of the proof.

The scale was considerable. According to the paper, several hundred nonlinear inequalities had their domains partitioned into more than 23,000 inequalities, and verifying them in HOL Light took about 5,000 processor-hours on Microsoft Azure. Run in parallel on 32 cores, the real time was under a week, and the checks were made in July and August 2014. In October 2014 they were rechecked at Radboud University, taking about 9,370 processor-hours over six days, with identical results. In its recorded proof format the main statement runs in about forty minutes on a 2 GHz CPU, and the paper encourages readers to verify it on their own computers.

How the referee's job changed

"A proof assistant largely cuts the mathematical referees out of the verification process," the Flyspeck paper says, before adding that "This is not to say that human oversight is no longer needed." What remains is an audit: checking that the right theorem was formalised and that no unapproved axioms were added. Most of that, the paper argues, can be done by any trained user of the proof assistants rather than a specialist in the mathematics. Citing a separate paper on auditing formal proofs, it adds that the auditor must assume malicious intent rather than innocent error.

The first beneficiaries were the mathematicians who had carried the refereeing burden. The Flyspeck paper has 22 authors, and the project drew in researchers and PhD students from several countries, with Vietnam prominent among them. Its supporters included the NSF, Microsoft Azure Research and Vietnam's Institute of Mathematics.

The formal proof of the Kepler conjecture also became part of the groundwork for research in which AI searches for proofs inside a proof assistant, as AlphaProof (2024) did in Lean. The idea of securing certainty by machine checking carried into the era of Erdős problems and AI (2026). The thread is followed on the AI and mathematics timeline.