A formal proof of the Kepler conjecture
From MaRDI portal
Publication:5280247
DOI10.1017/FMP.2017.1zbMATH Open1379.52018arXiv1501.02155OpenAlexW1825294361WikidataQ56267705 ScholiaQ56267705MaRDI QIDQ5280247FDOQ5280247
Authors:
Publication date: 20 July 2017
Published in: Forum of Mathematics, Pi (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1501.02155
Recommendations
ball packingformal proofIsabelle proof assistantKepler conjectureFlyspeck projectHOL Light proof assistant
Cites Work
- Title not available (Why is that?)
- Edinburgh LCF. A mechanized logic of computation
- Dense sphere packings. A blueprint for formal proofs
- A proof of the Kepler conjecture
- Flyspeck I: Tame Graphs
- A formulation of the Kepler conjecture
- Introduction to Interval Analysis
- Isabelle/HOL. A proof assistant for higher-order logic
- Title not available (Why is that?)
- Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
- HOL with definitions: semantics, soundness, and a verified implementation
- HOL Light: An Overview
- Towards Self-verification of HOL Light
- Formal certification of a compiler back-end or: programming a compiler with a proof assistant
- Code generation via higher-order rewrite systems
- A machine-checked proof of the odd order theorem
- 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
- Flyspeck II: The basic linear programs
- A revision of the proof of the Kepler conjecture
- Theorem Proving in Higher Order Logics
- Verified efficient enumeration of plane graphs modulo isomorphism
- Without Loss of Generality
- Efficient formal verification of bounds of linear programs
- An Interpretation of Isabelle/HOL in HOL Light
- Formal mathematics on display: a wiki for Flyspeck
- Flyspecking Flyspeck
- Developments in formal proofs
Cited In (72)
- Sphere packing and quantum gravity
- Verification of dynamic bisimulation theorems in Coq
- Bayesian ranking for strategy scheduling in automated theorem provers
- Guaranteed deterministic approach to superhedging: sensitivity of solutions of the Bellman-Isaacs equations and numerical methods
- Formalizing ordinal partition relations using Isabelle/HOL
- A proof system for graph (non)-isomorphism verification
- 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
- Title not available (Why is that?)
- The Kepler Conjecture
- A fully automatic theorem prover with human-style output
- Primitive Floats in Coq
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Title not available (Why is that?)
- ON A STRONG VERSION OF THE KEPLER CONJECTURE
- Flyspeck I: Tame Graphs
- Automatic generation of statistical volume elements using multibody dynamics and an erosion-based homogenization method
- Efficient formal verification of bounds of linear programs
- Machine learning guidance for connection tableaux
- A mathematical proof proved correct: the most efficient way to pack spheres
- Density of triangulated ternary disc packings
- High-dimensional sphere packing and the modular bootstrap
- Irrationality and transcendence criteria for infinite series in Isabelle/HOL
- The foundations of spectral computations via the solvability complexity index hierarchy
- Crystallographic texture and group representations
- A formalised theorem in the partition calculus
- Title not available (Why is that?)
- Varieties of mathematical understanding
- A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
- The role of the Mizar mathematical library for interactive proof development in Mizar
- Metrically homogeneous graphs of diameter \(3\)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares
- Dual linear programming bounds for sphere packing via modular forms
- Formal proof
- Kepler's conjecture and the dodecahedral conjecture
- Phase field approach to optimal packing problems and related Cheeger clusters
- Theorem Proving in Higher Order Logics
- Towards the automatic mathematician
- Title not available (Why is that?)
- From LCF to Isabelle/HOL
- Formalization of geometric algebra in HOL Light
- Placing your coins on a shelf
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- Title not available (Why is that?)
- Reliability of mathematical inference
- Techniques and results on approximation algorithms for packing circles
- A revision of the proof of the Kepler conjecture
- An introduction to univalent foundations for mathematicians
- Single-sized spheres on surfaces (S4)
- Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials
- Toward Computer-Assisted Discovery and Automated Proofs of Cutting Plane Theorems
- Mathematics education in the computational age: challenges and opportunities
- Proofs for a price: tomorrow's ultra-rigorous mathematical culture
- From sphere packing to Fourier interpolation
- On the computation of geometric features of spectra of linear operators on Hilbert spaces
- An experiment of a formal proof of an intermediate-level theorem in algebra
- The formal verification of the ctm approach to forcing
- Formalising the double-pushout approach to graph transformation
- A quantitative stability result for the sphere packing problem in dimensions 8 and 24
- Algorithm and abstraction in formal mathematics
- Incorporating a database of graphs into a proof assistant
- On the application of the calculus of positively constructed formulas for the study of controlled discrete-event systems
- Dual linear programming bounds for sphere packing via discrete reductions
- Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
- 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
- Abstraction boundaries and spec driven development in pure mathematics
- Mathematics and the formal turn
- Strange new universes: Proof assistants and synthetic foundations
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)
