A formal proof of the Kepler conjecture
From MaRDI portal
Publication:5280247
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
- scientific article; zbMATH DE number 234014 (Why is no real title available?)
- scientific article; zbMATH DE number 3083197 (Why is no real title available?)
- 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
- 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
(72)- Abstraction boundaries and spec driven development in pure mathematics
- Mathematics and the formal turn
- Strange new universes: Proof assistants and synthetic foundations
- Proofs for a price: tomorrow's ultra-rigorous mathematical culture
- 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
- 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
- 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
- The formal verification of the ctm approach to forcing
- scientific article; zbMATH DE number 7649964 (Why is no real title available?)
- The Kepler Conjecture
- A fully automatic theorem prover with human-style output
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Primitive Floats in Coq
- Flyspeck I: Tame Graphs
- scientific article; zbMATH DE number 7649979 (Why is no real title available?)
- ON A STRONG VERSION OF THE KEPLER CONJECTURE
- Automatic generation of statistical volume elements using multibody dynamics and an erosion-based homogenization method
- Machine learning guidance for connection tableaux
- Efficient formal verification of bounds of linear programs
- A mathematical proof proved correct: the most efficient way to pack spheres
- High-dimensional sphere packing and the modular bootstrap
- Density of triangulated ternary disc packings
- Irrationality and transcendence criteria for infinite series in Isabelle/HOL
- Crystallographic texture and group representations
- The foundations of spectral computations via the solvability complexity index hierarchy
- The role of the Mizar mathematical library for interactive proof development in Mizar
- scientific article; zbMATH DE number 1789934 (Why is no real title available?)
- A formalised theorem in the partition calculus
- Varieties of mathematical understanding
- A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
- Metrically homogeneous graphs of diameter \(3\)
- Big Math and the one-brain barrier: the tetrapod model of mathematical knowledge
- Kepler's conjecture and the dodecahedral conjecture
- Dual linear programming bounds for sphere packing via modular forms
- Formal proof
- Phase field approach to optimal packing problems and related Cheeger clusters
- Pourchet’s theorem in action: decomposing univariate nonnegative polynomials as sums of five squares
- Formalising the double-pushout approach to graph transformation
- Towards the automatic mathematician
- Theorem Proving in Higher Order Logics
- A quantitative stability result for the sphere packing problem in dimensions 8 and 24
- scientific article; zbMATH DE number 2209729 (Why is no real title available?)
- Algorithm and abstraction in formal mathematics
- From LCF to Isabelle/HOL
- Formalization of geometric algebra in HOL Light
- 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
- Placing your coins on a shelf
- Higher-Order Tarski Grothendieck as a Foundation for Formal Proof.
- scientific article; zbMATH DE number 7471719 (Why is no real title available?)
- Dual linear programming bounds for sphere packing via discrete reductions
- Reliability of mathematical inference
- Techniques and results on approximation algorithms for packing circles
- A revision of the proof of the Kepler conjecture
- Single-sized spheres on surfaces (S4)
- Mechanised DPO theory: uniqueness of derivations and Church-Rosser theorem
- Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials
- An introduction to univalent foundations for mathematicians
- Toward Computer-Assisted Discovery and Automated Proofs of Cutting Plane Theorems
- Mathematics education in the computational age: challenges and opportunities
- 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
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)
