Source-linked AI summary
A formal proof of the Kepler conjecture
Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, Roland Zumkeller
TL;DR
The paper addresses the challenge of fully certifying a complex computer-assisted proof of the Kepler conjecture. It describes Flyspeck’s formalization of the proof’s mathematical and computational components in HOL Light and Isabelle. The resulting main statement can be independently verified in about five hours directly from proof scripts or about forty minutes from recorded proof format on a 2 GHz CPU.
Problem
The original computer-assisted proof was difficult for referees to verify step by step and was published without complete certification.
Method
Flyspeck formally verifies the traditional proof text and three computational components, combining HOL Light and Isabelle across separate proof sessions.
Results
About five hours are required to verify the main Kepler statement directly from proof scripts on a 2 GHz CPU, or about forty minutes from recorded proof format.
Takeaways & Limitations
The combined formalization covers every part of the Kepler-conjecture proof and supports independent verification of its main statement.
Takeaways & Limitations
The formalization does not establish that the original proof or its computer code was itself error-free; hundreds of small errors were corrected during formalization.
Abstract
from arXiv · showhide
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.
1. Introduction
The paper presents Flyspeck, a completed project that formally verifies the Kepler conjecture using HOL Light and Isabelle. It addresses the verification difficulties of the original computer-assisted proof and provides an independently checkable account.
- Historical context: The Kepler conjecture states that no congruent-ball packing in Euclidean three-space exceeds the density of the face-centered cubic packing.It originated in Kepler’s 1611 booklet and is part of Hilbert’s 18th problem.
- Verification challenge: The original proof was difficult for referees to verify because it contained a complex computer proof, and publication proceeded without complete certification.Reviewers found specific assertions essentially correct but could not reliably check every step.
- Project scope: Flyspeck formalizes both the traditional mathematical proof and computer-code calculations underlying the Kepler conjecture.The article is the official published account of the completed project.
- Article scope: The paper focuses on the formalization components rather than the mathematical details of the underlying proof.Those mathematical details are presented separately in the book Dense Sphere Packings.
- Scale: The project is comparable in size and complexity to major formalization efforts and may set a record for verification-project lines of code.The comparison includes Feit–Thompson, CompCert, and seL4.
- Verification result: The main Kepler statement verifies in about five hours directly from proof scripts or about forty minutes from recorded proof format on a 2 GHz CPU.The authors encourage independent verification on readers’ computers.
2. The HOL Light proof assistant
HOL Light provides a small-kernel, LCF-based environment for formally checking mathematical proofs, while Isabelle/HOL supplies complementary features used in Flyspeck. Together, these systems support reliable proof construction, execution, and replay.
- Proof-assistant ecosystem: Flyspeck uses HOL Light and Isabelle/HOL, with a second verification of the main statement in HOL Zero.The formal verifications were distributed across these proof assistants.
- HOL Light foundations: HOL Light implements classical HOL logic based on Church’s typed lambda calculus, with a polymorphic type system, ten primitive inference rules, and three mathematical axioms.Its axioms are infinity, extensionality, and choice.
- Kernel architecture: The LCF architecture requires deductions to pass through a kernel, using OCaml’s type system to reduce logical-unsoundness risk to kernel errors.HOL Light’s kernel contains only a few hundred lines of code.
- Reliability: The HOL Light kernel has undergone extensive scrutiny, including formal verification of its correctness.The paper says experts regard false theorem creation as extremely unlikely except under unusual circumstances.
- Mathematical libraries: HOL Light’s libraries include formal results for multivariate integration, differential calculus, transcendental functions, and point-set topology on Rn.These libraries make it suitable for the analytical components of Flyspeck.
- Proof scripting: HOL Light proof scripts are OCaml programs whose mathematical terms use dedicated backquote syntax rather than ordinary machine arithmetic.This distinction prevents informal numeric notation from being confused with OCaml’s arithmetic behavior.
- Syntax: HOL Light notation uses ASCII conventions such as ! for universal quantification, ? for existential quantification, & for real-number embeddings, and |- for theorems.These conventions appear throughout the paper’s displayed formal statements.
- Isabelle/HOL: Isabelle/HOL adds module systems, type classes, extensive front-end support, intuitive scripting, and computational reflection for executable proof terms.Computations can be exported as ML and their results reintegrated into proofs.
3. The statement
The formal statement recasts the Kepler conjecture as an asymptotic bound on points in finite spherical containers and decomposes its proof into text formalization plus three computational components. Combining HOL Light and Isabelle formalizes every part of that decomposition.
- Formal statement: The formalized theorem does not assert uniqueness: several packings, including hexagonal-close and mixed-layer packings, attain the approximately 0.74 density bound.The face-centered cubic packing is one packing achieving the bound.
- Formal statement: Density is represented inside finite spherical containers with an error term whose volume ratio tends to zero as container volume grows.The limiting statement recovers the traditional density formulation of the Kepler conjecture.
- Packing definition: A packing is modeled as centers V in R3 whose distinct points are at least 2 units apart.The distance condition is encoded formally by the displayed implication involving u, v, and dist(u,v).
- Formal statement: The formal conjecture bounds the number of centers inside an open radius-r spherical container by a leading volume term plus a c r^2 error term for r ≥ 1.The statement permits c to depend on the packing V.
- Proof decomposition: The proof combines traditional mathematical arguments with three computer-calculation bodies: nearly a thousand nonlinear inequalities, exhaustive tame-plane-graph classification, and linear-programming results.Each calculation body is expressed as a precise mathematical statement in HOL Light.
- Proof composition: The central single-session theorem derives the Kepler conjecture from the nonlinear-inequality and tame-classification assumptions while formalizing the text proof and linear programming.The remaining assumptions are proved in separate HOL Light and Isabelle sessions, yielding formalization of every proof part.
4. Text formalization
The text formalization organizes the Kepler proof around a blueprint adapted for formal verification, connecting geometric reduction, combinatorial structures, and optimization arguments. The completed formalization combines text proofs with independently formalized computational components and cross-system replay.
- Blueprint adaptation: The formalization closely follows a blueprint proof developed alongside it, with revisions driven by issues discovered during formalization.The blueprint and formal proof use persistent cross-links despite changing lemma and theorem numbering.
- Blueprint proof outline: The proof reduces arbitrary sphere packings to finitely many nearby balls through a Marchal-cell partition and a cell-cluster inequality.Packing centers are represented as a discrete set, and the partition replaces the original decomposition stars.
- Blueprint proof outline: Counterexamples are reduced to contravening packings whose properties yield a combinatorial structure and an optimization problem over nonlinear inequalities.For each tame planar hypermap, linear programming is used to show the relaxed system is infeasible.
- Differences from the original proof: The blueprint replaces plane-graph topology with hypermaps and adopts a geometric partition better suited to formalization.It also organizes the proof around reusable concepts including spherical trigonometry, polyhedra, Voronoi partitions, and linear programming.
- Verification and scope: Hundreds of small proof errors were corrected during formalization, including a significant error in the original proof of the main estimate.The authors state that the original proof itself was not formally verified error-free.
- Verification and scope: The completed project formalizes every part of the proof by combining HOL Light and Isabelle results, with recorded proofs replayable in HOL Zero and other HOL systems.Importing recorded proofs is faster than replaying high-level scripts and provides an additional trustworthiness check.
5. Nonlinear inequalities
The nonlinear-inequality component formalizes interval-based verification for multivariate analytic inequalities. Taylor interval approximations, monotonicity arguments, automated search, and parallel computation make the large verification tractable while preserving formal HOL Light theorems.
- Interval verification: Natural interval subdivision can require enormous numbers of subintervals, especially for multivariate inequalities.The project therefore uses improved interval extensions based on Taylor approximations.
- Taylor approximations: Taylor interval approximations bound function values using interval extensions of the function and its first two derivatives.Choosing the expansion point near the interval midpoint minimizes the width parameter and often reduces subdivisions.
- Taylor approximations: For g(x) = x−arctan(x) on, the Taylor approximation produces [0.108, 0.927], improving on the natural extension.The expensive interval extension of arctan is evaluated only once in this example.
- Monotonicity and sharp cases: Taylor intervals also establish monotonicity when a derivative interval excludes zero, reducing some k-dimensional verifications to abutting rectangles of dimension k−1.Sharp inequalities are handled by exact evaluation at a corner, negativity away from it, and derivative-sign arguments nearby.
- Automation: An automated OCaml/HOL Light procedure separates informal subdivision search from formal verification, which produces the final HOL Light theorem.The search selects subdivisions and auxiliary choices such as monotonicity arguments or disjuncts to verify.
- Scale and rechecking: More than 23,000 partitioned inequalities were verified in HOL Light using approximately 5000 processor-hours, with parallel execution reducing elapsed time to less than a week.A second verification required about 9370 processor-hours over six days and obtained identical results.
6. Combining HOL Light sessions
The project combines nonlinear-inequality proofs generated in parallel HOL Light sessions into one master theorem. A modified HOL Light importer checks theorem histories and reassembles the distributed results without being used to prove other results.
- Session combination: The nonlinear inequalities were proved in separate parallel HOL Light sessions, but ordinary HOL Light cannot transfer theorems between sessions without reconstructing proofs.A specially modified version was introduced to combine the results into a single session.
- Session combination: The importer accepts a theorem only when its constants, types, axioms, and complete histories match exactly across sessions.The theorem and its history are converted to canonical form for export and verification.
- Master theorem: Reassembling the distributed pieces checks that no inequality was overlooked and yields a formal proof of the_nonlinear_inequalities.This theorem is exactly the assumption used in the formal proof of the Kepler conjecture.
- Master theorem: The modified HOL Light version is used only to assemble small theorems from parallel sessions, not to prove any other Kepler-conjecture result.The import mechanism is constrained by OCaml scoping rules.
7. Tame Classification
Flyspeck formalized the tame plane-graph classification in Isabelle/HOL by recasting executable enumeration and proving that the resulting finite set matches the archive. The formalization also exposed a bug in the original enumeration code and required substantial computational optimization.
- 7. Tame Classification: The project formally verified the computer-based classification of tame plane graphs used in the Kepler proof.This work verified the code underlying the original classification.
- 7. Tame Classification: Tame graphs encode possible counterexamples, and the archive is intended to contain every tame graph up to isomorphism.The completeness theorem connects the formal graph classification to the proof’s counterexample elimination.
- 7. Tame Classification: Isabelle/HOL executes a recast enumeration program to produce TameEnum, then proves every tame graph is in TameEnum and every enumerated graph matches an archive graph.The second step is discharged by automatic evaluation of a closed executable formula.
- 7. Tame Classification: The formalization defines plane graphs algorithmically from seed polygons and restricts enumeration using triangle-to-hexagon face sizes and bounded admissible weight.These tameness constraints ensure only finitely many tame graphs up to isomorphism.
- 7. Tame Classification: Approximate tameness checks may generate non-tame graphs but do not remove tame ones, so later proof stages eliminate only spurious candidates.The restriction prioritizes completeness of the enumeration over exact pruning.
- 7. Tame Classification: The final enumeration handles 2 × 10^9 intermediate and final graphs, runs in a few hours, and corrected a symmetry-related bug in the original Java program.The bug affected an early blueprint draft but not the original proof’s output.
8. Importing results from Isabelle
The formal proof remains distributed between Isabelle/HOL and HOL Light because automatic import is unavailable and Isabelle’s reflected computations are not accepted by the HOL Light kernel. The interface therefore relies on manually translated definitions and a theorem treated as an assumption in HOL Light.
- 8. Importing results from Isabelle: The tame graph classification was completed in Isabelle/HOL, while the rest of Flyspeck was carried out in HOL Light.Keeping the systems separate was within the project’s scope, although translation was considered feasible.
- 8. Importing results from Isabelle: Automatic import from Isabelle to HOL Light is not readily available, and Isabelle’s use of computational reflection creates a deeper incompatibility.The HOL Light kernel does not permit reflection, so reflected proof portions would require modification.
- 8. Importing results from Isabelle: HOL Light represents the Isabelle classification through the assumption import_tame_classification, whose right-hand side is a verbatim translation of Isabelle’s completeness theorem.The translated statement asserts that every tame plane graph is isomorphic to an archived graph.
- 8. Importing results from Isabelle: The translated definitions and types were produced by hand, while both systems use an archive generated from the same ML file.The shared archive source helps align the two formal statements.
- 8. Importing results from Isabelle: The authors justify cross-system transfer by observing that the classification statement can be expressed as a first-order propositional SAT problem.The passage frames satisfiability preservation as the basis for relating the two systems.
9. Linear programs
The linear-programming component converts constraints on potential packing counterexamples into formally checkable linear systems, using relaxations, automatic case splitting, and verified dual certificates. The resulting 43,078 programs were formally verified in about 15 hours on a 2.4GHz computer.
- 9. Linear programs: Potential counterexamples are encoded by tame planar hypermaps, and each hypermap generates a linear program whose infeasibility rules out that case.The classification supplies finitely many combinatorial cases for the computational argument.
- 9. Linear programs: Nonlinear inequalities are relaxed by replacing nonlinear expressions with new variables, producing linear systems that may be easier to prove inconsistent.The relaxation deliberately ignores some nonlinear dependencies while retaining consequences such as bounds.
- 9. Linear programs: The generation of linear inequalities is semiautomatic: automatic procedures derive many constraints, while others require manual formal proofs.This separates formal theorem generation from the general verification procedure.
- 9. Linear programs: Irrational coefficients are replaced by rational or integer coefficients automatically, including by multiplying inequalities by a sufficiently large power of 10.The resulting rational system remains inconsistent when the original system is inconsistent.
- 9. Linear programs: About half of the tame-hypermap cases require automatic case splitting because their initial linear relaxations are not sufficiently precise.Splitting on alternatives such as x ≤ a ∨ a ≤ x introduces tighter inequalities.
- 9. Linear programs: A modified dual solution proves infeasibility by combining constraints into the contradiction 0x + 0y ≤ −0.2974, with exact cancellation of variable coefficients.The zero coefficients of x and y are a key feature of the certificate.
- 9. Linear programs: 43,078 linear programs were formally verified in about 15 hours on a 2.4GHz computer using integer dual certificates.External tools find candidate dual solutions, but formal verification checks the resulting arithmetic.
10. Auditing a distributed formal proof
Auditing the distributed formal proof requires checking both the generated theorem and the trustworthiness of the proof infrastructure. Formal assistance reduces routine human verification, but specialized review remains necessary for definitions, translations, axioms, and system modifications.
- 10. Auditing a distributed formal proof: Proof-assistant auditing still requires human oversight, although only a small part demands specialized mathematical expertise.Trained users of HOL Light and Isabelle can perform the remaining audit work.
- 10. Auditing a distributed formal proof: Auditors execute proof scripts, inspect definitions to confirm that the intended Kepler conjecture was formalized, and check that no unapproved axioms were added.They must also audit the formal proof system itself.
- 10. Auditing a distributed formal proof: The most serious audit issue is verifying the hand translation of the tame classification theorem from Isabelle into HOL Light.The authors identify this translation as their greatest vulnerability to error, despite its rote nature.
- 10. Auditing a distributed formal proof: The audit must confirm that the long tame-graph lists in Isabelle and HOL Light are identical and that the modified HOL Light session correctly combines nonlinear inequalities.Both lists were generated from the same master file, but the cross-system correspondence still requires checking.
11. Related work and acknowledgements
The Flyspeck project influenced and supported a broad range of subsequent formalization efforts, and its completion involved many contributors and institutions.
- Related work: Flyspeck inspired or supported research on formal inequalities, proof translation, proof refactoring, machine learning for proofs, and HOL Light extensions.
- Acknowledgements: The project’s members’ roles were documented in the email announcement of its completion.
- Acknowledgements: The authors acknowledge contributions from a large group of researchers and collaborators.
- Acknowledgements: Institutional support came from NSF grants, Microsoft Azure Research, foundations, universities, and research institutes.
12. Appendix on definitions
The appendix records formal definitions underlying the Kepler conjecture, including real-number operations, Euclidean distance, sphere-packing constraints, and finite-set cardinalities.
- Formal definitions: The appendix states that key definitions in the Kepler conjecture have their expected formal meanings.
- Real arithmetic: Absolute value is defined by separate cases for nonnegative and negative real numbers.
- Real arithmetic: Powers, square roots, finite sums, and a pi-over-four series are formalized through recursive or algebraic identities.
- Finite sets: Finite-set cardinality is represented by HAS_SIZE, requiring finiteness and a specified CARD value.
- Euclidean space: The appendix formalizes a bijection between R^3 and ordered triples of reals and gives the standard Euclidean metric on R^3.
- Sphere packings: A packing is constrained so that points in the set cannot be distinct when their distance is less than 2.