# A formal proof of the Kepler conjecture

arXiv: https://arxiv.org/abs/1501.02155 · HTML: https://mlsanity.com/paper/1501.02155/

## Key facts

- Cited by 42 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Jan 2015.

## Built on by (most cited first, 30 of 42)

- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Can stable and accurate neural networks be computed? -- On the barriers of deep learning and Smale's 18th problem](https://mlsanity.com/paper/2101.08286/) (2021)
- [Generating Natural Language Proofs with Verifier-Guided Search](https://mlsanity.com/paper/2205.12443/) (2022)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs](https://mlsanity.com/paper/2301.02195/) (2023)
- [Autoformalizing Euclidean Geometry](https://mlsanity.com/paper/2405.17216/) (2024)
- [Mathematical Language Models: A Survey](https://mlsanity.com/paper/2312.07622/) (2023)
- [Autoformalization in the Era of Large Language Models: A Survey](https://mlsanity.com/paper/2505.23486/) (2025)
- [ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalization](https://mlsanity.com/paper/2510.15981/) (2025)
- [Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4](https://mlsanity.com/paper/2410.16429/) (2024)
- [Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning](https://mlsanity.com/paper/2502.13834/) (2025)
- [Peano: Learning Formal Mathematical Reasoning](https://mlsanity.com/paper/2211.15864/) (2022)
- [Math Agents: Computational Infrastructure, Mathematical Embedding, and Genomics](https://mlsanity.com/paper/2307.02502/) (2023)
- [Learning Physically Realizable Skills for Online Packing of General 3D Shapes](https://mlsanity.com/paper/2212.02094/) (2022)
- [LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks](https://mlsanity.com/paper/2606.03303/) (2026)
- [Progress in Formalizing Sphere Packing in Dimension 8](https://mlsanity.com/paper/2604.23468/) (2026)
- [Automatic Textbook Formalization](https://mlsanity.com/paper/2604.03071/) (2026)
- [3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes](https://mlsanity.com/paper/2410.11133/) (2024)
- [HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinement](https://mlsanity.com/paper/2505.15740/) (2025)
- [A Study of Continuous Vector Representationsfor Theorem Proving](https://mlsanity.com/paper/2101.09142/) (2021)
- [Thinking Machines: Mathematical Reasoning in the Age of LLMs](https://mlsanity.com/paper/2508.00459/) (2025)
- [Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AI](https://mlsanity.com/paper/2406.11563/) (2024)
- [A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Exam](https://mlsanity.com/paper/2504.04945/) (2025)
- [Model-Based and Sample-Efficient AI-Assisted Math Discovery in Sphere Packing](https://mlsanity.com/paper/2512.04829/) (2025)
- [Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases](https://mlsanity.com/paper/2607.13292/) (2026)
- [Smart Proofs via Smart Contracts: Succinct and Informative Mathematical Derivations via Decentralized Markets](https://mlsanity.com/paper/2102.03044/) (2021)
- [When can you trust feature selection? -- I: A condition-based analysis of LASSO and generalised hardness of approximation](https://mlsanity.com/paper/2312.11425/) (2023)
- [Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agents](https://mlsanity.com/paper/2603.06737/) (2026)

## Abstract (arXiv)

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.