Pith. sign in

REVIEW 2 major objections 6 minor 8 cited by

Lean formally verifies the E8 sphere packing theorem in dimension 8

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · glm-5.2

2026-07-04 14:17 UTC pith:W4K5ZXVJ

load-bearing objection Sorry-free Lean proof of the E8 sphere packing theorem, with AI autoformalization completing ~40k lines in five days. The artifact is referenced as PR #341 but no repository URL or commit hash is given. the 2 major comments →

arxiv 2604.23468 v3 pith:W4K5ZXVJ submitted 2026-04-25 math.MG cs.AIcs.LOmath.NT

Progress in Formalizing Sphere Packing in Dimension 8

Sidharth Hariharan , Christopher Birkbeck , Seewoo Lee , Ho Kiu Gareth Ma , Bhavik Mehta , Auguste Poiroux , Maryna Viazovska This is my paper
classification math.MG cs.AIcs.LOmath.NT MSC 52C1711F1168V20
keywords sphere packingformalizationLean theorem proverE8 latticemodular formsautoformalizationCohn-Elkies boundquasimodular forms
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

The paper reports that Viazovska's 2016 proof identifying the E8 lattice as the densest sphere packing in eight-dimensional space has been fully formalized in the Lean theorem prover with no remaining gaps (no 'sorries'). The formalized theorem states that the optimal sphere packing density in R^8 equals the density of the E8 lattice packing, which equals pi^4/384. The final stages of the roughly 60,000-line formalization were completed by an autoformalization model called Gauss, which extended the human-written development from about 20,000 lines to a complete proof in five days. The human team had built the core infrastructure: definitions of sphere packings, densities, the E8 lattice, the Cohn-Elkies linear programming bound, and the modular-form machinery (Eisenstein series, Jacobi theta functions, quasimodular forms). Gauss filled in remaining proofs including contour-deformation identities for the Fourier eigenfunction argument and finite-dimensionality theory for modular forms. The paper is candid that the exact mathematical correspondence between Gauss-generated proofs and the intended argument is still being audited, and that the formalization follows a modified blueprint rather than Viazovska's original paper line-for-line.

Core claim

The central claim is that the eight-dimensional sphere packing theorem — the density of the optimal packing in R^8 equals pi^4/384, achieved by the E8 lattice — has a complete, sorry-free formal proof in Lean. This was achieved through a collaboration between human formalizers who built the foundational definitions and proof infrastructure, and an autoformalization model (Gauss) that completed the remaining proof obligations in five days, roughly tripling the codebase. The key mathematical objects carrying the argument are the Cohn-Elkies linear programming bound (which reduces the packing problem to constructing a function satisfying three analytic conditions), Viazovska's 'magic function'g

What carries the argument

Cohn-Elkies linear programming bound; Viazovska's magic function constructed from quasimodular forms; contour integration identities; modular form dimension formulas

Load-bearing premise

The paper assumes that the Lean kernel's acceptance of the 60,000-line development — including Gauss-generated proofs of contour deformation identities and modular form theory — faithfully represents a mathematically valid proof of the sphere packing theorem, even though the authors acknowledge that the exact correspondence between the autoformalized proofs and the intended mathematical argument has not yet been fully audited.

What would settle it

Discovery that Gauss-generated proofs, while accepted by the Lean kernel, contain type-correct but mathematically vacuous arguments — for example, proofs that exploit unintended behavior of definitions rather than establishing the intended mathematical content — would undermine the claim that the sphere packing theorem has been genuinely formalized.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • The formalization provides a machine-checkable proof of the dimension-8 sphere packing result, placing it alongside Hales's formal proof of the Kepler conjecture in dimension 3.
  • The success of the human-AI collaboration model suggests that autoformalization can substantially accelerate large-scale formalization projects when built on well-designed human infrastructure.
  • The Lean library infrastructure developed (modular forms, complex integration, sphere packing definitions) is reusable for future formalization work in number theory and discrete geometry.
  • The dimension-24 sphere packing problem (also solved by Viazovska and collaborators using analogous techniques) is a natural next target for formalization using the infrastructure built here.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If Gauss-generated proofs are later found to be formally valid in Lean but mathematically misaligned with the intended argument, this would reveal a subtle but important distinction: a proof can be type-correct and kernel-accepted without faithfully representing the mathematical reasoning it claims to formalize.
  • The fact that generating proofs was easier than compressing them suggests that autoformalization models may currently optimize for coverage rather than code quality, which could become a bottleneck as formalized libraries grow.
  • The independent development of contour integration machinery by multiple formalization projects suggests that complex analysis infrastructure in proof assistants is reaching a tipping point where rapid formalization of analytic number theory results becomes feasible.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 6 minor

Summary. This paper reports on a milestone in the formalization of Viazovska's sphere packing theorem in dimension 8: a sorry-free Lean proof that the optimal sphere packing in R^8 is the E8 lattice packing, with the final stages completed by Math, Inc.'s autoformalization model 'Gauss.' The paper describes the mathematical background (Cohn-Elkies bounds, the magic function, modular form inequalities), the Lean definitions of sphere packings and density, the contour integration challenges, the modular form theory developed, metaprogramming tactics, and the Gauss autoformalization process. It also discusses remaining project objectives and the correspondence between the formalized and informal proofs.

Significance. A sorry-free formalization of the 8-dimensional sphere packing theorem is a significant achievement for formal mathematics. The paper documents a notable human-AI collaboration in formalization and describes reusable infrastructure (definitions for sphere packings, modular form theory, metaprogramming tactics) that will benefit future work. The falsifiable core claim — that a sorry-free Lean proof exists — is in principle mechanically verifiable. The paper is honest about the state of the project, including the ongoing audit of the Gauss-generated proofs and the stylistic issues in the generated code.

major comments (2)
  1. The central claim is that a sorry-free formalization exists, but the paper references only 'PR #341' without providing a repository URL or commit hash. The reader cannot independently verify the sorry-free status or inspect the formalization from the information in the paper. For a paper whose primary contribution is the existence of a verified artifact, this is a load-bearing verifiability gap. The authors should provide a permanent, accessible link (e.g., a DOI, a Zenodo archive, or a repository URL with a specific commit hash). Without this, the central claim cannot be checked by readers or referees.
  2. The paper does not state which axioms are used in the Lean development. A sorry-free proof is only as trustworthy as its axiom basis; the paper should explicitly confirm that only the standard Lean axioms (propext, Classical.choice, Quot.sound) are used, or disclose any additional axioms. This is standard practice in formalization papers and is necessary for the reader to assess the strength of the verification claim.
minor comments (6)
  1. Reference [4]: 'A First Course in Modular Farms' should read 'A First Course in Modular Forms.'
  2. The Lean code snippets in Section 2 are rendered with excessive spacing and inconsistent formatting, making them difficult to read. The authors should verify that code blocks render correctly in the final version.
  3. Section 3 states the development went from 'about 20,000 lines to 80,000 lines' and was then 'reduced to 60,000 lines.' It would help to clarify whether the 60,000-line figure includes the original 20,000 lines of human-written code or refers only to the Gauss contribution after compression.
  4. Section 4 states that 'new proofs might still be used to complete certain parts of the project.' This phrasing is ambiguous — it could mean that parts of the current sorry-free proof might be replaced. The authors should clarify whether the current artifact is a complete proof as-is, or whether replacements are anticipated for correctness rather than stylistic reasons.
  5. The paper would benefit from a brief table or paragraph summarizing which PRs correspond to which mathematical components (e.g., PR #229 for the contour deformation, PR #331 for the modular form inequalities), to help readers navigate the development.
  6. The footnote on page 5 mentions that equivalent results were 'independently proven by contributors to Kontorovich and Tao's open-source' project. A more specific citation or reference would be appropriate.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading and for identifying two concrete, actionable improvements to the manuscript. Both points are well-taken: the paper should provide a permanent, accessible link to the formalization artifact, and it should explicitly state the axiom basis of the Lean development. We will address both in the revised manuscript.

read point-by-point responses

  1. Referee: The central claim is that a sorry-free formalization exists, but the paper references only 'PR #341' without providing a repository URL or commit hash. The reader cannot independently verify the sorry-free status or inspect the formalization from the information in the paper. For a paper whose primary contribution is the existence of a verified artifact, this is a load-bearing verifiability gap. The authors should provide a permanent, accessible link (e.g., a DOI, a Zenodo archive, or a repository URL with a specific commit hash). Without this, the central claim cannot be checked by readers or referees.

    Authors: The referee is entirely correct. For a paper whose central claim is the existence of a sorry-free formalization, the absence of a permanent, inspectable reference is a significant gap that we must close. In the current draft, the reference to 'PR #341' assumes familiarity with the project repository, which is not acceptable for a self-contained publication. We will revise the manuscript to include (1) the full repository URL, (2) the specific commit hash corresponding to the sorry-free state of the development as of February 2026, and (3) a DOI or Zenodo archive link to ensure permanent accessibility. We agree that without this information, the central verifiable claim of the paper cannot be independently checked, and we thank the referee for flagging this. revision: yes

  2. Referee: The paper does not state which axioms are used in the Lean development. A sorry-free proof is only as trustworthy as its axiom basis; the paper should explicitly confirm that only the standard Lean axioms (propext, Classical.choice, Quot.sound) are used, or disclose any additional axioms. This is standard practice in formalization papers and is necessary for the reader to assess the strength of the verification claim.

    Authors: The referee raises a valid and standard point. The trustworthiness of a sorry-free proof depends on the axioms it relies on, and it is standard practice in formalization papers to disclose this explicitly. We will add a statement to the revised manuscript confirming the axiom basis of the development. Our development uses only the three standard Lean axioms — propext, Classical.choice, and Quot.sound — and does not introduce any additional axioms. We will state this explicitly in the paper, and we can also include the output of the #print axioms command on the main theorem statement to provide machine-checked evidence of this fact. revision: yes

Circularity Check

0 steps flagged

No circularity found: formalization is verified by external Lean kernel against independently published mathematics

full rationale

The paper reports a formal verification in Lean of Viazovska's sphere packing theorem. The derivation chain is: (1) definitions of sphere packing, density, E8 lattice, and the main theorem statement are standard mathematical definitions, not defined in terms of the result; (2) the proof formalizes Viazovska's published proof [14] and Lee's published inequalities [10], both independent prior work by external authors (Viazovska is a co-author of this paper but [14] is her independently published, peer-reviewed Annals paper); (3) the correctness of the formalization is checked by the Lean kernel, which is an external verification standard not controlled by the paper's authors; (4) the Cohn-Elkies linear programming bound [2] is an independently published result. The autoformalization model Gauss used the human-written blueprint and Lean code as input, but the output is verified by the Lean kernel — if the kernel accepts a sorry-free proof of a correctly stated theorem using standard axioms, it is mathematically valid by construction. The paper's acknowledgment that 'the exact correspondence between the autoformalization and the intended proof path is still being investigated' concerns mathematical exposition and understandability, not logical circularity. No step in the derivation chain reduces to its own inputs by construction. The self-citation to Viazovska [14] is load-bearing but refers to independently published, peer-reviewed work that predates this formalization project. The reference to Hariharan's master's thesis [7] is for expository detail, not a load-bearing mathematical claim. No fitted parameters are renamed as predictions, no ansatz is smuggled through self-citation, and no uniqueness theorem from the authors is invoked to forbid alternatives.

Axiom & Free-Parameter Ledger

0 free parameters · 5 axioms · 1 invented entities

The formalization has no free parameters — it is a proof, not a fit. The axioms are standard for formalization projects: external mathematical results (Cohn-Elkies, Viazovska's construction, Lee's inequalities) are used as inputs to be formalized, and the Lean kernel's soundness is the foundational assumption. The one invented entity, the Gauss model, is a tool whose outputs are independently verified by the Lean kernel, so its opacity affects reproducibility but not the correctness of the formalization itself.

axioms (5)
  • domain assumption Cohn-Elkies linear programming bound (Theorem in Section 2): if f: R^d -> R satisfies (CE1) f <= 0 decays suitably, (CE2) f-hat(x) <= 0 for |x| >= 1, (CE3) f-hat(x) >= 0 for all x, then the sphere packing density is bounded by f(0) / f-hat(0) * Vol(B_d(0, 1/2)).
    This is the foundational bound from Cohn and Elkies [2] that the entire proof strategy relies on. It is a published, peer-reviewed result used as an external input.
  • domain assumption Viazovska's construction of the magic function g as a linear combination of radial Schwartz Fourier -1-eigenfunctions a and b (defined via contour integrals involving quasimodular forms phi_0 and psi_S).
    The formalization verifies this construction and its properties; the construction itself is from Viazovska [14], used as the mathematical input to be formalized.
  • domain assumption Lee's algebraic proof of the modular form inequalities (2): 0 < phi_0(z) + 36/pi^2 * psi_S(z) and 0 < phi_0(z) - 36/pi^2 * psi_S(z) on the positive imaginary axis.
    The paper states in Section 4 that the project formalizes 'the modified argument in the project blueprint, which differs from the original most notably in its use of Lee's original proof [10] of the inequalities (2).' This is an external published result used as input.
  • standard math The Lean kernel is a sound proof checker — if Lean accepts a proof term, it constitutes a valid proof of the stated theorem.
    This is the foundational assumption of all Lean formalization projects. The paper implicitly relies on it throughout.
  • domain assumption Rectangular contour Cauchy-Goursat theorem and its unbounded variant, as available in Mathlib, are sufficient for the contour deformation arguments needed in the eigenfunction proof.
    Section 2 states that Mathlib 'lacks sufficient contour integration machinery' and the authors chose rectangular contours because Mathlib contains a proof of Cauchy-Goursat for rectangular contours. The sufficiency of this restricted contour class for the needed deformations is a modeling choice.
invented entities (1)
  • Gauss autoformalization model no independent evidence
    purpose: Completing the final stages of the Lean formalization by generating proof code from the human-written blueprint and existing Lean development.
    Gauss is a proprietary model developed by Math, Inc. The paper does not describe its architecture, training data, or methodology in sufficient detail to independently assess its capabilities. Its output is verified by the Lean kernel, which provides correctness guarantees, but the model itself is not independently characterized. The paper notes that 'a complete account of our learnings, along with more technical details of the work done to finish the project, will appear in a forthcoming paper.'

pith-pipeline@v1.1.0-glm · 11377 in / 3642 out tokens · 154262 ms · 2026-07-04T14:17:17.421910+00:00 · methodology

0 comments
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.

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. 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. 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 val￾ues 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 ↗

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 8 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. On the existence problem of regular Gabor frames

    math.FA 2026-06 unverdicted novelty 7.0 full

    For every d>1, explicit lattice criteria with D(Λ)>1 are derived under which no continuous-Zak-transform function generates a Gabor frame, negatively resolving existence questions for several classes of smooth windows.

  2. Hypothesis-Disciplined Multi-Agent Automated Formalization of Asymptotic Statistical Theory

    cs.AI 2026-06 unverdicted novelty 7.0

    A hypothesis-disciplined multi-agent pipeline in Lean 4 produces axiom-clean, source-faithful formalizations of parametric and semi-parametric asymptotic distribution and efficiency theorems.

  3. Formalizing Mathematics at Scale

    cs.AI 2026-05 accept novelty 7.0

    A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable for...

  4. Advancing Mathematics Research with AI-Driven Formal Proof Search

    cs.AI 2026-05 unverdicted novelty 7.0

    LLM-based agents in Lean solved 9 of 353 open Erdős problems and proved 44 of 492 OEIS conjectures at a few hundred dollars each.

  5. Advancing Mathematics Research with AI-Driven Formal Proof Search

    cs.AI 2026-05 conditional novelty 7.0

    An LLM-based agent with Lean verification autonomously solved multiple open Erdős problems and OEIS conjectures in the first large-scale test.

  6. Formalizing Extended Complex Numbers, Mobius Transformations, and Cross Ratio in Lean 4

    math.CV 2026-06 accept novelty 6.0 full

    Lean 4 formalization of extended complex plane via Option ℂ, Möbius transformations identified with PGL(2,ℂ), and machine-checked proofs of uniqueness and cross-ratio invariance.

  7. $L^2$-Stability for STFT phase retrieval

    math.FA 2026-05 unverdicted novelty 6.0 partial

    STFT with Gaussian window performs L²-local stable phase retrieval at the constant function, with Lean 4 autoformalization for an extension to Hermite windows and finite spans of basis vectors.

  8. Towards a Bridge Layer Between Bibliographic and Formalized Mathematical Knowledge

    cs.DL 2026-06 unverdicted novelty 5.0

    Authors propose a bridge database linking math publications to formal proof libraries and introduce a formalization score estimated via cross-document alignment to Lean as a feasibility study.

Reference graph

Works this paper leans on

14 extracted references · 14 canonical work pages · cited by 7 Pith papers · 1 internal anchor

  1. [1]

    Mathematicians in the age of AI

    Avigad, J.: Mathematicians in the age of AI. arXiv preprint arXiv:2603.03684 (2026),��������������������������������

    work page internal anchor Pith review Pith/arXiv arXiv 2026

  2. [2]

    Annals of Math- ematics157(2), 689–714 (2003).���������������������������������������� �������������������,�����������������������������������

    Cohn, H., Elkies, N.: New Upper Bounds on Sphere Packings I. Annals of Math- ematics157(2), 689–714 (2003).���������������������������������������� �������������������,�����������������������������������

    work page 2003

  3. [3]

    arXiv preprint arXiv:2603.13680 (2026),��������������������������������

    DeDeo, S., Duede, E.: A correspondence problem for mathematical proof. arXiv preprint arXiv:2603.13680 (2026),��������������������������������

    work page arXiv 2026

  4. [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). ���������������������������������������������������������

    work page 2006

  5. [5]

    Annals of Mathematics162(3), 1065–1185 (2005).���������������������������������������������������� ��������,������������������������������������

    Hales, T.C.: A Proof of the Kepler Conjecture. Annals of Mathematics162(3), 1065–1185 (2005).���������������������������������������������������� ��������,������������������������������������

    work page 2005

  6. [6]

    Forum of Mathematics, Pi5, e2 (2017).����������������������������������

    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).�������...

    work page 2017

  7. [7]

    MSci Thesis, Imperial College London (2025), �����������������������������������������������������������, Supervised by Bhavik Mehta

    Hariharan, S.: Viazovska’s Magic Function in Dimension 8: An At- tempt at Formalisation. MSci Thesis, Imperial College London (2025), �����������������������������������������������������������, Supervised by Bhavik Mehta

    work page 2025

  8. [8]

    Kepler, J.: Strena seu de nive sexangula. Francofurti ad Moenum : apud Godefridum Tampach (1611).���������������������������������������� ����������,��������������������������������������������������, ETH- Bibliothek Zürich, Rar 4342: 2,����������������������������������

    work page

  9. [9]

    Kontorovich, A., Tao, T.: Prime Number Theorem and More (Jan 2024),������ ��������������������������������������������������

    work page 2024

  10. [10]

    Lee, S.: Algebraic proof of modular form inequalities for optimal sphere packings (2024),��������������������������������

    work page 2024

  11. [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)

    work page 2015

  12. [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

    work page

  13. [13]

    Mathematische Zeitschrift48(1), 676–684 (Dec 1942).����������������������������������,���������������� ������������������

    Tóth, L.F.: Über die dichteste Kugellagerung. Mathematische Zeitschrift48(1), 676–684 (Dec 1942).����������������������������������,���������������� ������������������

    work page 1942

  14. [14]

    Annals of Math- ematics185(3), 991–1015 (2017).���������������������������������������� �������������������,������������������������������������

    Viazovska, M.S.: The sphere packing problem in dimension 8. Annals of Math- ematics185(3), 991–1015 (2017).���������������������������������������� �������������������,������������������������������������

    work page 2017