arxiv: 2604.23468 · v2 · submitted 2026-04-25 · 🧮 math.MG · cs.AI· cs.LO· math.NT

Recognition: unknown

A Milestone in Formalization: The Sphere Packing Problem in Dimension 8

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

Authors on Pith no claims yet

Pith reviewed 2026-05-08 06:39 UTC · model grok-4.3

classification 🧮 math.MG cs.AIcs.LOmath.NT

keywords sphere packingformalizationLean theorem proverViazovskamodular formsdimension 8autoformalization

0 comments

The pith

The sphere packing problem in eight dimensions has been formally verified in Lean with AI assistance.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper reports the completion of a formalization effort for Viazovska's 2016 solution to the sphere packing problem in dimension 8. The proof constructs a special function from modular forms that meets the optimality criteria previously identified by Cohn and Elkies. Work began in 2024 with human-written Lean code, and the final verification steps were finished in 2026 by the Gauss autoformalization model. A reader would care because machine-checked proofs remove the possibility of overlooked errors in intricate analytic arguments and illustrate a workable division of labor between people and current AI systems.

Core claim

The sphere packing problem in dimension 8 was formally verified in the Lean theorem prover. The project reached this milestone in February 2026 after human coders supplied the bulk of the Lean development and the Gauss model completed the remaining steps. This confirms Viazovska's construction of a magic function that satisfies the linear programming bounds required to prove that the E8 lattice achieves the densest packing.

What carries the argument

The Lean formalization of Viazovska's modular-form magic function together with the Gauss autoformalization model that finished the last verification stages.

Load-bearing premise

The human-written Lean code and the Gauss AI model together captured every logical detail of Viazovska's original proof without gaps or introduced errors.

What would settle it

An independent Lean run or manual audit that produces a failed proof obligation on one of the key positivity or inequality statements in the modular-form construction.

Figures

Figures reproduced from arXiv: 2604.23468 by Auguste Poiroux, Bhavik Mehta, Christopher Birkbeck, Ho Kiu Gareth Ma, Maryna Viazovska, Seewoo Lee, Sidharth Hariharan.

**Figure 1.** Figure 1: Choosing contours of integration Denote by E2, E4, E6 the weight 2, 4, 6 Eisenstein Series; ∆ the discriminant form; and θ10, θ00, θ01 the Jacobi theta functions. Define ϕ0 and ψS in terms of these quasimodular forms as follows: ϕ0 := (E2E4 − E6) 2 ∆ ψS := 128 θ 4 01 − θ 4 10 θ 8 00 − θ 4 10 + θ 4 00 θ 8 01 view at source ↗

**Figure 2.** Figure 2: Contour needed for eigenfunction property for all x ∈ R 8 with ∥x∥ ≥ √ 2. Replacing ϕ0 with ψS in (1) yields an analogous expression for b. The significance of these representations is that when analytically continued to account for all values of x ∈ R 8 , they yield a convenient expression for g as a certain Laplace transform. A direct computation then shows (CE1), and the proofs of (CE2) and (CE3) can b… view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This is a status report on completing the Lean formalization of Viazovska's 2016 sphere packing proof in dimension 8, with AI assistance on the final steps.

read the letter

The paper reports that the team finished formalizing Viazovska's solution to the sphere packing problem in eight dimensions inside Lean, with the last parts handled by the Gauss autoformalization model in February 2026. The project began in 2024 and focused on encoding the modular-form magic function and the Cohn-Elkies linear-programming bounds. They describe the human-AI workflow and list open tasks that remain. This is useful as a record of what it took to get a major analytic number theory result into a proof assistant. The account of how the AI contributed to the endgame gives a concrete example of scaling formal methods to a result that mixes analysis and optimization. The honesty about remaining objectives is also helpful for anyone planning similar projects. The main limitation is that the text stays at the level of a project update. It gives no code excerpts, no breakdown of which lemmas were hardest, no verification logs, and no discussion of how they checked the AI output for gaps. Without those details or a link to the repository, it is difficult to evaluate the formalization beyond the success claim. Readers in the formal methods and AI-for-math communities will find value here as a case study. Others working on sphere packing or modular forms will not get new mathematical content. I would send this to peer review. Documenting the machine-checked version of a high-profile theorem is worth archiving and discussing, even if the paper needs more technical substance in revision.

Referee Report

2 major / 1 minor

Summary. The paper reports the launch in March 2024 of a Lean formalization project for Viazovska's 2016 solution to the sphere-packing problem in dimension 8 (via modular-form construction of the magic function and Cohn-Elkies linear-programming bounds) and announces that the verification was completed in February 2026, with the final stages performed by Math, Inc.'s Gauss autoformalization model. It describes the human-AI workflow, collaboration techniques, and remaining project objectives.

Significance. If the formalization is complete and faithful to the original argument, the work constitutes a milestone in interactive theorem proving by demonstrating that a high-profile result in discrete geometry can be fully machine-checked. It also provides a concrete case study of AI-assisted formalization that could inform future efforts on similarly intricate analytic and number-theoretic arguments.

major comments (2)

[Abstract and verification section] Abstract and § on verification milestone: the central claim that the result 'was formally verified' is not supported by any description of the formalized statements, total lines of Lean code, coverage of the modular-form construction, or handling of the linear-programming bounds; without such details the milestone cannot be assessed from the manuscript.
[Human-AI collaboration section] Section on human-AI collaboration: the account of Gauss's role does not specify how the model was constrained to avoid introducing or overlooking gaps in the analytic estimates or the optimality conditions, leaving open whether the final verification is fully faithful to Viazovska's original argument.

minor comments (1)

The manuscript should include a link to the public Lean repository or a summary table of formalized theorems so readers can inspect the artifact directly.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thoughtful review and for highlighting areas where the manuscript requires greater specificity. We address each major comment below and will revise the paper to incorporate the requested details on the formalization scope and the human-AI workflow.

read point-by-point responses

Referee: [Abstract and verification section] Abstract and § on verification milestone: the central claim that the result 'was formally verified' is not supported by any description of the formalized statements, total lines of Lean code, coverage of the modular-form construction, or handling of the linear-programming bounds; without such details the milestone cannot be assessed from the manuscript.

Authors: We agree that the current manuscript provides only a high-level announcement without the quantitative and technical details needed to evaluate the verification. In the revised version we will expand the verification section to list the principal formalized statements (including the magic function's key analytic properties and the Cohn-Elkies optimality conditions), report the approximate total lines of Lean code together with a component-wise breakdown, describe the coverage of the modular-form construction (including auxiliary results on Eisenstein series and theta functions), and explain how the linear-programming bounds were encoded and verified. These additions will allow readers to assess the milestone directly from the text. revision: yes
Referee: [Human-AI collaboration section] Section on human-AI collaboration: the account of Gauss's role does not specify how the model was constrained to avoid introducing or overlooking gaps in the analytic estimates or the optimality conditions, leaving open whether the final verification is fully faithful to Viazovska's original argument.

Authors: We accept that the present description of the workflow is insufficiently precise on safeguards. The revised collaboration section will detail the concrete constraints applied: Gauss operated under human-curated prompts that referenced exact sections of Viazovska's paper; every AI-generated lemma or estimate was subjected to line-by-line human review for gaps in analytic bounds or optimality conditions; and an iterative human-AI dialogue protocol was used to cross-check each step against the original argument. We will also note any remaining limitations of the current formalization and how fidelity was maintained throughout. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The manuscript is a progress report on the formalization of Viazovska's 2016 sphere-packing proof in Lean, with final verification steps assisted by the Gauss model. It describes the human-AI workflow, modular-form construction, and Cohn-Elkies bounds but introduces no new derivations, predictions, or self-referential definitions. The central claim (completion of formal verification) rests on the external soundness of Lean and fidelity to the cited 2016 result rather than any reduction to fitted inputs, self-citations, or ansatzes internal to this paper. No load-bearing step equates to its own inputs by construction, so the derivation chain is self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The claim rests on the soundness of the Lean system and the correctness of the 2016 mathematical result being formalized; no new free parameters or invented mathematical entities are introduced.

axioms (2)

standard math The Lean theorem prover implements mathematical logic without errors
Any formal verification claim presupposes the soundness of the underlying proof assistant.
domain assumption Viazovska's 2016 modular-form construction satisfies the Cohn-Elkies optimality conditions for sphere packing in dimension 8
The project formalizes rather than re-derives this prior result.

invented entities (1)

Gauss autoformalization model no independent evidence
purpose: To complete the final stages of the Lean formalization
Presented as a collaborative tool developed by Math, Inc., but no independent evidence of its correctness is supplied in the abstract.

pith-pipeline@v0.9.0 · 5451 in / 1402 out tokens · 119113 ms · 2026-05-08T06:39:19.849384+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

14 extracted references · 10 canonical work pages · 2 internal anchors

[1]

Mathematicians in the age of AI

Avigad, J.: Mathematicians in the age of AI. arXiv preprint arXiv:2603.03684 (2026),https://arxiv.org/abs/2603.03684

work page internal anchor Pith review Pith/arXiv arXiv 2026
[2]

Annals of Math- ematics157(2), 689–714 (2003).https://doi.org/https://doi.org/10.4007/ annals.2003.157.689,http://www.jstor.org/stable/3597215

Cohn, H., Elkies, N.: New Upper Bounds on Sphere Packings I. Annals of Math- ematics157(2), 689–714 (2003).https://doi.org/https://doi.org/10.4007/ annals.2003.157.689,http://www.jstor.org/stable/3597215

work page arXiv 2003
[3]

arXiv preprint arXiv:2603.13680 (2026),https://arxiv.org/abs/2603.13680

DeDeo, S., Duede, E.: A correspondence problem for mathematical proof. arXiv preprint arXiv:2603.13680 (2026),https://arxiv.org/abs/2603.13680

work page arXiv 2026
[4]

Diamond, F., Shurman, J.: A First Course in Modular Farms. No. 228 in Graduate Texts in Mathematics, Springer New York, NY, New York, first edn. (March 2006). https://doi.org/https://doi.org/10.1007/978-0-387-27226-9

work page doi:10.1007/978-0-387-27226-9 2006
[5]

Annals of Mathematics162(3), 1065–1185 (2005).https://doi.org/https://doi.org/10.4007/annals.2005

Hales, T.C.: A Proof of the Kepler Conjecture. Annals of Mathematics162(3), 1065–1185 (2005).https://doi.org/https://doi.org/10.4007/annals.2005. 162.1065,http://www.jstor.org/stable/20159940

work page doi:10.4007/annals.2005 2005
[6]

Thomas Hubert, Rishi Mehta, Laurent Sartran, Miklós Z

Hales, T.C., Adams, M., Bauer, G., Dang, T.D., Harrison, J., Hoang, L.T., Kaliszyk, C., Magron, V., Mclaughlin, S., Nguyen, T.T., Nguyen, Q.T., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, T.H.A., Tran, N.T., Trieu, T.D., Urban, J., Vu, K., Zumkeller, R.: A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi5, e2 (2017).https:/...

work page doi:10.1017/fmp.2017.1 2017
[7]

MSci Thesis, Imperial College London (2025), https://thefundamentaltheor3m.github.io/M4R_Thesis/main.pdf, Supervised by Bhavik Mehta

Hariharan, S.: Viazovska’s Magic Function in Dimension 8: An At- tempt at Formalisation. MSci Thesis, Imperial College London (2025), https://thefundamentaltheor3m.github.io/M4R_Thesis/main.pdf, Supervised by Bhavik Mehta

2025
[8]

Kepler, J.: Strena seu de nive sexangula. Francofurti ad Moenum : apud Godefridum Tampach (1611).https://doi.org/https://doi.org/10.3931/ e-rara-478,https://www.e-rara.ch/zut/content/titleinfo/135387, ETH- Bibliothek Zürich, Rar 4342: 2,https://doi.org/10.3931/e-rara-478

work page doi:10.3931/e-rara-478
[9]

Kontorovich, A., Tao, T.: Prime Number Theorem and More (Jan 2024),https: //github.com/AlexKontorovich/PrimeNumberTheoremAnd

2024
[10]

Lee, S.: Algebraic proof of modular form inequalities for optimal sphere packings (2024),https://arxiv.org/abs/2406.14659

work page internal anchor Pith review Pith/arXiv arXiv 2024
[11]

In: Felty, A.P., Middeldorp, A

de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean Theorem Prover (System Description). In: Felty, A.P., Middeldorp, A. (eds.) Au- tomated Deduction - CADE-25. pp. 378–388. Springer International Publishing, Cham (2015)

2015
[12]

Forhandlingerne ved de Skandinaviske Naturforskeres14(1892), zbl 24.0259.01

Thue, A.: Om nogle geometrisk-taltheoretiske Theoremer. Forhandlingerne ved de Skandinaviske Naturforskeres14(1892), zbl 24.0259.01
[13]

Mathematische Zeitschrift48(1), 676–684 (Dec 1942).https://doi.org/10.1007/BF01180035,https://doi.org/ 10.1007/BF01180035

Tóth, L.F.: Über die dichteste Kugellagerung. Mathematische Zeitschrift48(1), 676–684 (Dec 1942).https://doi.org/10.1007/BF01180035,https://doi.org/ 10.1007/BF01180035

work page doi:10.1007/bf01180035 1942
[14]

Annals of Math- ematics185(3), 991–1015 (2017).https://doi.org/https://doi.org/10.4007/ annals.2017.185.3.7,http://www.jstor.org/stable/26395747

Viazovska, M.S.: The sphere packing problem in dimension 8. Annals of Math- ematics185(3), 991–1015 (2017).https://doi.org/https://doi.org/10.4007/ annals.2017.185.3.7,http://www.jstor.org/stable/26395747

work page arXiv 2017