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.
Reading the bibliography…
Lagerungen in der Ebene auf der Kugel und im Raum
L. Fejes Tóth · 1953
Earlier work this paper cites.
Edinburgh LCF: a mechanized logic of computation, volume 78 of lecture notes in computer science, 1979
Michael Gordon, Robin Milner, and Christopher Wadsworth · 1979
Earlier work this paper cites.
Introduction to HOL: a theorem proving environment for higher order logic
Michael JC Gordon and Tom F Melham · 1993
Earlier work this paper cites.
Isabelle/HOL — A Proof Assistant for Higher-Order Logic , volume 2283 of Lect. Notes in Comp. Sci
Tobias Nipkow, Lawrence Paulson, and Markus Wenzel · 2002
Earlier work this paper cites.
A proof of the Kepler conjecture
Thomas C. Hales · 2005
Earlier work this paper cites.
Proving bounds for real linear programs in Isabelle/HOL
Steven Obua · 2005
Earlier work this paper cites.
Formalizing Plane Graph Theory – Towards a Formalized Proof of the Kepler Conjecture
Gertrud Bauer · 2006
Earlier work this paper cites.
Flyspeck I: Tame graphs
Gertrud Bauer and Tobias Nipkow · 2006
Earlier work this paper cites.
Introduction to the Flyspeck project
Thomas C. Hales · 2006
Earlier work this paper cites.
The Kepler conjecture
Thomas C. Hales and Samuel P. Ferguson · 2006
Earlier work this paper cites.
Towards self-verification of HOL Light
John Harrison · 2006
Earlier work this paper cites.
Formal certification of a compiler back-end, or: programming a compiler with a proof assistant
Xavier Leroy · 2006
Earlier work this paper cites.
An interpretation of Isabelle/HOL in HOL Light
Sean McLaughlin · 2006
Earlier work this paper cites.
Flyspeck I: Tame graphs
Tobias Nipkow, Gertrud Bauer, and Paula Schultz · 2006
Earlier work this paper cites.
Importing HOL into Isabelle/HOL
Steven Obua and Sebastian Skalberg · 2006
Earlier work this paper cites.
Flyspeck II: The Basic Linear Programs
Steven Obua · 2008
Cited alongside, same era.
Global Optimization in Type Theory
Roland Zumkeller · 2008
Cited alongside, same era.
Without loss of generality
John Harrison · 2009
Cited alongside, same era.
seL4: formal verification of an OS kernel
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood · 2009
Cited alongside, same era.
The Kepler Conjecture and its proof , pages 3–26
J. Lagarias · 2009
Cited alongside, same era.
Introduction to interval analysis
Ramon E Moore, R Baker Kearfott, and Michael J Cloud · 2009
Cited alongside, same era.
Flyspeck II: the basic linear programs
Steven Obua and Tobias Nipkow · 2009
Cited alongside, same era.
Introducing HOL Zero
Mark Adams · 2010
Cited alongside, same era.
Code generation via higher-order rewrite systems
Florian Haftmann and Tobias Nipkow · 2010
Cited alongside, same era.
A revision of the proof of the Kepler Conjecture
Thomas C. Hales, John Harrison, Sean McLaughlin, Tobias Nipkow, Steven Obua, and Roland Zumkeller · 2010
Cited alongside, same era.
The strong dodecahedral conjecture and Fejes Tóth’s contact conjecture
Thomas C Hales · 2011
Cited alongside, same era.
Study of the Kepler’s conjecture: the problem of the closest packing
Christian Marchal · 2011
Cited alongside, same era.
Recording and refactoring HOL Light tactic proofs
Mark Adams and David Aspinall · 2012
Later among the works it cites.
Dense Sphere Packings: a blueprint for formal proofs , volume 400 of London Math Soc. Lecture Note Series
Thomas C. Hales · 2012
Later among the works it cites.
Formal Methods and Computations
Alexey Solovyev · 2012
Later among the works it cites.
A machine-checked proof of the odd order theorem
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al · 2013
Later among the works it cites.
Scalable LCF-style proof translation
Cezary Kaliszyk and Alexander Krauss · 2013
Later among the works it cites.
Formal Proofs for Global Optimization – Templates and Sums of Squares
Victor Magron · 2013
Later among the works it cites.
Formal Verification of Nonlinear Inequalities with Taylor Interval Approximations
Alexey Solovyev and Thomas C. Hales · 2013
Later among the works it cites.
Formal mathematics on display: A wiki for Flyspeck
Carst Tankink, Cezary Kaliszyk, Josef Urban, and Herman Geuvers · 2013
Later among the works it cites.
Flyspecking Flyspeck
Mark Adams · 2014
Later among the works it cites.
The Flyspeck Project, 2014
Flyspeck · 2014
Later among the works it cites.
Developments in formal proofs
Thomas Hales · 2014
Later among the works it cites.
The HOL Light theorem prover, 2014
John Harrison · 2014
Later among the works it cites.
Learning-assisted theorem proving with millions of lemmas
Cezary Kaliszyk and Josef Urban · 2014
Later among the works it cites.
HOL with definitions: Semantics, soundness, and a verified implementation
Ramana Kumar, Rob Arthan, Magnus O. Myreen, and Scott Owens · 2014
Later among the works it cites.
alphaXiv searches the wider corpus for related work and actual follow-ups.
alphaXiv is searching for related work…