A FORMAL PROOF OF THE KEPLER CONJECTURE

DOI10.1017/fmp.2017.1zbMath1379.52018arXiv1501.02155OpenAlexW1825294361WikidataQ56267705 ScholiaQ56267705MaRDI QIDQ5280247

No author found.

Publication date: 20 July 2017

Published in: Forum of Mathematics, Pi (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1501.02155

zbMATH Keywords

ball packingformal proofIsabelle proof assistantKepler conjectureFlyspeck projectHOL Light proof assistant

Mathematics Subject Classification ID

Related Items (52)

A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture ⋮ A proof system for graph (non)-isomorphism verification ⋮ 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 ⋮ Guaranteed deterministic approach to superhedging: sensitivity of solutions of the Bellman-Isaacs equations and numerical methods ⋮ Automatic generation of statistical volume elements using multibody dynamics and an erosion-based homogenization method ⋮ Crystallographic texture and group representations ⋮ The role of the Mizar mathematical library for interactive proof development in Mizar ⋮ 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 ⋮ Formalizing Ordinal Partition Relations Using Isabelle/HOL ⋮ Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL ⋮ 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 ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A quantitative stability result for the sphere packing problem in dimensions 8 and 24 ⋮ Reliability of mathematical inference ⋮ Unnamed Item ⋮ Mathematics Education in the Computational Age: Challenges and Opportunities ⋮ Algorithms for weighted sum of squares decomposition of non-negative univariate polynomials ⋮ Primitive Floats in Coq ⋮ Higher-Order Tarski Grothendieck as a Foundation for Formal Proof. ⋮ Single-sized spheres on surfaces (S4) ⋮ An introduction to univalent foundations for mathematicians ⋮ From LCF to Isabelle/HOL ⋮ Machine learning guidance for connection tableaux ⋮ Verification of dynamic bisimulation theorems in Coq ⋮ Placing your Coins on a Shelf ⋮ Phase field approach to optimal packing problems and related Cheeger clusters ⋮ Sphere packing and quantum gravity ⋮ Towards the automatic mathematician ⋮ Toward Computer-Assisted Discovery and Automated Proofs of Cutting Plane Theorems ⋮ Metrically homogeneous graphs of diameter 3 ⋮ Formalization of geometric algebra in HOL Light ⋮ Techniques and results on approximation algorithms for packing circles ⋮ First steps towards a formalization of forcing ⋮ Varieties of mathematical understanding ⋮ Bayesian ranking for strategy scheduling in automated theorem provers ⋮ Dual linear programming bounds for sphere packing via modular forms

Uses Software

• ML
• Isabelle/HOL
• GLPK
• HOL
• HOL Light
• LCF
• Flyspeck
• seL4
• HOL Zero
• GitHub
• kepler98
• Tame Graphs
• Archive Formal Proofs
• GNU parallel

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Learning-assisted theorem proving with millions of lemmas
• A formulation of the Kepler conjecture
• A revision of the proof of the Kepler conjecture
• Isabelle/HOL. A proof assistant for higher-order logic
• Edinburgh LCF. A mechanized logic of computation
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Flyspeck II: The basic linear programs
• Study of the Kepler's conjecture: the problem of the closest packing
• A proof of the Kepler conjecture
• Formal Mathematics on Display: A Wiki for Flyspeck
• Flyspecking Flyspeck
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• Developments in Formal Proofs
• Verified Efficient Enumeration of Plane Graphs Modulo Isomorphism
• Without Loss of Generality
• HOL Light: An Overview
• Code Generation via Higher-Order Rewrite Systems
• Introduction to Interval Analysis
• Flyspeck I: Tame Graphs
• Towards Self-verification of HOL Light
• An Interpretation of Isabelle/HOL in HOL Light
• Efficient Formal Verification of Bounds of Linear Programs
• Scalable LCF-Style Proof Translation
• A Machine-Checked Proof of the Odd Order Theorem
• Formal certification of a compiler back-end or
• Theorem Proving in Higher Order Logics

This page was built for publication: A FORMAL PROOF OF THE KEPLER CONJECTURE