mlsanityData to 7 Oct 2026

A formal proof of the Kepler conjecture

arXiv 1501.02155 ↗First posted 9 Jan 2015math.MG cs.LOcited by 42

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 6; 2022: 6; 2023: 4; 2024: 6; 2025: 8; 2026: 12.

42 papers.

Sort:

By area:

  1. 2022Autoformalization with Large Language Modelscited by 252
  2. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  3. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  4. 2021Can stable and accurate neural networks be computed? -- On the barriers of deep learning and Smale's 18th problemcited by 53
  5. 2022Generating Natural Language Proofs with Verifier-Guided Searchcited by 52
  6. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  7. 2023Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofscited by 27
  8. 2024Autoformalizing Euclidean Geometrycited by 27
  9. 2023Mathematical Language Models: A Surveycited by 24
  10. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
  11. 2025ProofFlow: A Dependency Graph Approach to Faithful Proof Autoformalizationcited by 18
  12. 2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
30 more
  1. 2022Peano: Learning Formal Mathematical Reasoningcited by 15
  2. 2023Math Agents: Computational Infrastructure, Mathematical Embedding, and Genomicscited by 15
  3. 2024Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4cited by 15
  4. 2022Learning Physically Realizable Skills for Online Packing of General 3D Shapescited by 12
  5. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 11
  6. 20243D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processescited by 6
  7. 2025HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinementcited by 6
  8. 2026Progress in Formalizing Sphere Packing in Dimension 8cited by 6
  9. 2026Automatic Textbook Formalizationcited by 5
  10. 2021A Study of Continuous Vector Representationsfor Theorem Provingcited by 4
  11. 2025Thinking Machines: Mathematical Reasoning in the Age of LLMscited by 4
  12. 2024Intersymbolic AI: Interlinking Symbolic AI and Subsymbolic AIcited by 3
  13. 2025A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Examcited by 3
  14. 2021Smart Proofs via Smart Contracts: Succinct and Informative Mathematical Derivations via Decentralized Marketscited by 2
  15. 2023When can you trust feature selection? -- I: A condition-based analysis of LASSO and generalised hardness of approximationcited by 2
  16. 2025Model-Based and Sample-Efficient AI-Assisted Math Discovery in Sphere Packingcited by 2
  17. 2026Agent Hunt: Bounty Based Collaborative Autoformalization With LLM Agentscited by 2
  18. 2026Multi-agent Autoformalization of Tensor Network Theorycited by 2
  19. 2021Disambiguating Symbolic Expressions in Informal Documentscited by 1
  20. 2026Quantum automated theorem provingcited by 1
  21. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  22. 2026Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Basescited by 1
  23. 2026Does the Proof Prove It That Way? Faithful Formalization of Elements Proofscited by 1
  24. 2021A Reasoning Engine for the Gamification of Loop-Invariant Discoverycited by 0
  25. 2022Feynman on Artificial Intelligence and Machine Learning, with Updatescited by 0
  26. 2024Artifical intelligence and inherent mathematical difficultycited by 0
  27. 2025Self-Validated Learning for Particle Separation: A Correctness-Based Self-Training Framework Without Human Labelscited by 0
  28. 2026Human agency in initial human-AI proof formalization workflowscited by 0
  29. 2026AI with Authority, from Application to Siliconcited by 0
  30. 2026A machine-checked proof of the Dong-Yang classification of optimal (n,4) binary codes for BSCscited by 0