mlsanityData to 7 Oct 2026

Progress in Formalizing Sphere Packing in Dimension 8

arXiv 2604.23468 ↗First posted 25 Apr 2026math.MG cs.AI cs.LOcited by 6

Not on the map. Why?

Abstract (arXiv)

In 2016, Viazovska famously solved the sphere packing problem in dimension 8, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect on the unique collaboration between humans and Gauss, and discuss project objectives that remain.

Key facts. Cited by 6 papers in the map (data through 7 Oct 2026). Builds on 2 of its 14 references that are in the map. First posted on arXiv 25 Apr 2026.

Builds on

2 of 14 references.

References · 2

  1. 2015A formal proof of the Kepler conjecturecited by 42
  2. 2026Mathematicians in the age of AIcited by 4

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2026: 6.

6 papers.

  1. 2026AI co-mathematician: Accelerating mathematicians with agentic AIcited by 13
  2. 2026Formalizing Mathematics at Scalecited by 5
  3. 2026Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledgecited by 0
  4. 2026Explanations, Prompts, and Formalizations: Arguments for New Norms in LLM-Enabled Mathematical Researchcited by 0
  5. 2026Math for AI safety: an invitation for mathematicianscited by 0
  6. 2026Choir: An Open Protocol for Distributed Multi-Agent Autoformalizationcited by 0