Progress in Formalizing Sphere Packing in Dimension 8

Sidharth Hariharan; Christopher Birkbeck; Seewoo Lee; Ho Kiu Gareth Ma; Bhavik Mehta; Auguste Poiroux; Maryna Viazovska

math.MGApr 25, 2026

Progress in Formalizing Sphere Packing in Dimension 8

Authors: Sidharth Hariharan, Christopher Birkbeck, Seewoo Lee, Ho Kiu Gareth Ma, Bhavik Mehta, Auguste Poiroux, Maryna Viazovska

Organizations: Carnegie Mellon University, Pittsburgh PA 15213, United States of America · University of East Anglia, Norwich NR4 7TJ, United Kingdom · University of California, Berkeley, Berkeley CA 94720, United States of America · University of Warwick, Coventry CV4 7AL, United Kingdom · Imperial College London, London SW7 2AZ, United Kingdom · Math, Inc, San Francisco CA 94107, United States of America · 7 École Polytechnique Fédérale de Lausanne, 1015 Lausanne VD, Switzerland

Abstract

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.

Explore similar work

LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization
Jun 3, 2026Yuanhe Zhang, Yuekai Sun, Taiji Suzuki +2Autoformalization Long-Horizon
Formally Solving Answer-Construction Problems in Lean
May 24, 2025Jialiang Sun, Yuzhi Tang, Ao Li +2Theorem Conjecture
Finding Kissing Numbers with Game-theoretic Reinforcement Learning
Nov 17, 2025Chengdong Ma, Théo Tao Zhaowei, Pengyu Li +6

Jun 3, 2026 · cs.AIJ/K move · Enter open · S save

LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

Yuanhe Zhang, Yuekai Sun, Taiji Suzuki, Jason D. Lee+1

Department of Statistics, University of Warwick, UK · Center for Advanced Intelligence Project, RIKEN, Japan · Department of Statistics, University of Michigan, USA · Department of Mathematical Informatics, The University of Tokyo · Department of Electrical Engineering and Computer Sciences, also Department of Statistics, University of California, Berkeley, USA

Long-horizon autoformalization of research mathematics fails not only at hard lemmas, but at scale: statements drift, dependencies tangle, context decays, and local repairs corrupt distant work. We present LeanMarathon, a multi-agent harness for reliable research-level Lean autoformalization. Its core abstraction is an evolving blueprint: a Lean file that serves simultaneously as formal proof skeleton, natural-language proof graph, and shared system of record. Four contract-scoped agents construct, audit, prove, and repair this blueprint. These agents are coordinated by a two-stage orchestrator that first stabilizes target fidelity through adversarial review and then discharges the proof directed acyclic graph (DAG) from its dynamic leaves upward in parallel CI-gated rounds. LeanMarathon turns one brittle multi-hour run into many local, recoverable, parallel transactions. We evaluate LeanMarathon on two recent research papers spanning four Erdős problems (#1051, #1196, #164, #1217). Across three autonomous runs, it formalizes all seven target theorems with no sorry, proving 258 lemmas and theorems. These results show that reliable AI co-mathematics requires not only stronger provers, but durable harnesses that preserve target fidelity across long mathematical developments. The code can be found at https://github.com/YuanheZ/LeanMarathon.

Autoformalization Long-Horizon Autonomous Racing

Open paper Ask about it PDF

Abstract

Explore similar work

LeanMarathon: Toward Reliable AI Co-Mathematicians through Long-Horizon Lean Autoformalization

Formally Solving Answer-Construction Problems in Lean

Finding Kissing Numbers with Game-theoretic Reinforcement Learning