A FORMAL PROOF OF THE KEPLER CONJECTURE

2017/01/01 by Thomas Hales, Mark Adams, Gertrud Bauer +19 · 2 citations
Physics and Astronomy · Mathematics · Medicine · #Advanced Mathematical Theories and Applications #History and Theory of Mathematics #Mathematics and Applications #Formal proof #Kepler #HOL #Conjecture #Proof assistant #Mathematics #Computer science #Calculus (dental) #Discrete mathematics #Programming language #Mathematical proof #Medicine #Stars #Geometry

paper · pdf · doi:10.1017/fmp.2017.1

openalex publication_date 2017/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/04

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.

Citations

• Introduction to the Flyspeck Project
• Code Generation via Higher-Order Rewrite Systems
• Developments in Formal Proofs
• Study of the Kepler’s conjecture: the problem of the closest packing
• Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations
• A proof of the Kepler conjecture

Cited by

• Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
• Kepler conjecture [wikipedia]