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.
Recommendations
Cites work
- A formulation of the Kepler conjecture
- A machine-checked proof of the odd order theorem
- A proof of the Kepler conjecture
- A revision of the proof of the Kepler conjecture
- An Interpretation of Isabelle/HOL in HOL Light
- Code generation via higher-order rewrite systems
- Dense sphere packings. A blueprint for formal proofs
- Developments in formal proofs
- Edinburgh LCF. A mechanized logic of computation
- Efficient formal verification of bounds of linear programs
- Flyspeck I: Tame Graphs
- Flyspeck II: The basic linear programs
- Flyspecking Flyspeck
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Formal mathematics on display: a wiki for Flyspeck
- HOL Light: An Overview
- HOL with definitions: semantics, soundness, and a verified implementation
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 3083197 (Why is no real title available?)
- Introduction to Interval Analysis
- Isabelle/HOL. A proof assistant for higher-order logic
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- Learning-assisted theorem proving with millions of lemmas
- Scalable LCF-style proof translation
- Study of the Kepler's conjecture: the problem of the closest packing
- Theorem Proving in Higher Order Logics
- Towards Self-verification of HOL Light
- Verified efficient enumeration of plane graphs modulo isomorphism
- Without Loss of Generality
Cited in
(89)- The role of the Mizar mathematical library for interactive proof development in Mizar
- Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials
- Single-sized spheres on surfaces (S4)
- Machine learning guidance for connection tableaux
- Verification of dynamic bisimulation theorems in Coq
- Towards the automatic mathematician
- Techniques and results on approximation algorithms for packing circles
- Bayesian ranking for strategy scheduling in automated theorem provers
- Automatic generation of statistical volume elements using multibody dynamics and an erosion-based homogenization method
- Crystallographic texture and group representations
- From LCF to Isabelle/HOL
- Phase field approach to optimal packing problems and related Cheeger clusters
- Sphere packing and quantum gravity
- Formalization of geometric algebra in HOL Light
- First steps towards a formalization of forcing
- A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
- A fully automatic theorem prover with human-style output
- Kepler's conjecture and the dodecahedral conjecture
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- High-dimensional sphere packing and the modular bootstrap
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Reliability of mathematical inference
- Toward Computer-Assisted Discovery and Automated Proofs of Cutting Plane Theorems
- A mathematical proof proved correct: the most efficient way to pack spheres
- The Kepler Conjecture
- Mathematics education in the computational age: challenges and opportunities
- Flyspeck I: Tame Graphs
- scientific article; zbMATH DE number 1789934 (Why is no real title available?)
- An introduction to univalent foundations for mathematicians
- ON A STRONG VERSION OF THE KEPLER CONJECTURE
- Metrically homogeneous graphs of diameter \(3\)
- Dual linear programming bounds for sphere packing via modular forms
- Fixed points theorems for non-transitive relations
- Formalizing ordinal partition relations using Isabelle/HOL
- Irrationality and transcendence criteria for infinite series in Isabelle/HOL
- Placing your coins on a shelf
- Efficient formal verification of bounds of linear programs
- Formal proof
- Theorem Proving in Higher Order Logics
- scientific article; zbMATH DE number 2209729 (Why is no real title available?)
- Varieties of mathematical understanding
- Primitive Floats in Coq
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- scientific article; zbMATH DE number 7649964 (Why is no real title available?)
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
- A proof system for graph (non)-isomorphism verification
- The foundations of spectral computations via the solvability complexity index hierarchy
- A formalised theorem in the partition calculus
- Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares
- Density of triangulated ternary disc packings
- What is the point of computers? A question for pure mathematicians
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- Towards an annotation standard for STEM documents. Datasets, benchmarks, and spotters
- The work of Maryna Viazovska
- Mathematics and the formal turn
- Abstraction boundaries and spec driven development in pure mathematics
- Strange new universes: Proof assistants and synthetic foundations
- From sphere packing to Fourier interpolation
- The formal verification of the ctm approach to forcing
- A quantitative stability result for the sphere packing problem in dimensions 8 and 24
- On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems
- Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
- Proofs for a price: tomorrow's ultra-rigorous mathematical culture
- An experiment of a formal proof of an intermediate-level theorem in algebra
- On the computation of geometric features of spectra of linear operators on Hilbert spaces
- Formalising the double-pushout approach to graph transformation
- Algorithm and abstraction in formal mathematics
- Incorporating a database of graphs into a proof assistant
- Dual linear programming bounds for sphere packing via discrete reductions
- Chain Bounding, the Leanest Proof of Zorn’s Lemma, and an Illustration of Computerized Proof Formalization
- Exploring formal math on the blockchain: an explorer for Proofgold
- Growing Mathlib: maintenance of a large scale mathematical library
- Artificial intelligence and inherent mathematical difficulty
- The influence of cell phenotype on collective cell invasion into the extracellular matrix
- Notes on Gödel's and Scott's variants of the ontological argument
- Undecidability in physics: a review
- Voronoi conjecture for five-dimensional parallelohedra
- Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
- A mechanised semantics for HOL with ad-hoc overloading
- Translating HOL-Light proofs to Coq
- Packing squares into a disk with optimal worst-case density
- Error resilient space partitioning
- What is a modular form, or why do we need curved spaces?
- Anselm's God in Isabelle/HOL
- Complete Non-Orders and Fixed Points
- Variations on five-dimensional sphere packings
- Guaranteed deterministic approach to superhedging: sensitivity of solutions of the Bellman-Isaacs equations and numerical methods
- A revision of the proof of the Kepler conjecture
Describes a project that uses
Uses Software
This page was built for publication: A formal proof of the Kepler conjecture
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5280247)
