{"id":"5fd0d2f6-8f72-469a-adc2-74d5ee8f8242","arxiv_id":"2604.23468","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"unknown","formal_verification":"full","parameter_count":0,"one_line_summary":"Viazovska's optimal sphere packing theorem in dimension 8 has been fully formalized in Lean, with the final stages completed by Math, Inc.'s autoformalization model Gauss.","lead":"This paper reports a complete formal verification in Lean of Viazovska's sphere packing theorem in dimension 8, with the final stages produced by an AI autoformalization model called Gauss. It matters because it demonstrates that AI can substantially accelerate formal mathematics on a Fields Medal-tier result, and it produces a machine-checked proof artifact for a landmark theorem.","discovery_kind":"unclear","skeptic_critique":{"model":"glm-5.2","headline":"The sorry-free claim is mechanically verifiable but the artifact is not independently accessible from the paper; the reader's 'mathematically vacuous' concern is imprecise for Lean.","rationale":"The reader correctly identifies that the paper is a progress report with verifiability gaps, and the CONDITIONAL verdict is appropriate. However, the reader's framing of the concern — that Lean proofs could be 'formally valid but mathematically vacuous' — is imprecise. In a dependent type theory like Lean's, a sorry-free proof of a non-trivial theorem statement using standard axioms is mathematically valid; there is no category of 'type-correct but vacuous' proof for a substantive theorem. The real concern is more mundane: the artifact is not independently accessible from the paper (no URL, no commit hash), so the sorry-free claim cannot be verified without locating the repository. The paper's own statement that 'the exact correspondence between the autoformalization and the intended proof path is still being investigated' is about mathematical exposition and maintainability, not about correctness. If the theorem type-checks without sorry, it is proven. The paper is honest about its limitations — it explicitly frames itself as a progress report with full technical details forthcoming. The authors include Viazovska herself, lending strong credibility to the mathematical content. The CONDITIONAL verdict correctly reflects that the claim is credible but not yet fully substantiated by what the paper provides. The confidence level of MODERATE is reasonable.","tokens_in":8473,"tokens_out":3396,"duration_ms":66109,"concrete_test":"Locate the repository (likely the 'sphere-packing' or 'lean-sphere-packing' project on GitHub by Hariharan/Viazovska), check out PR #341, and run `lake build` with Lean 4. If the build completes with zero `sorry` warnings (check via `#print axioms` on the main theorem), the central claim is verified. Additionally, run `#print axioms sphere_packing_in_eight_dimensions` to confirm only standard Lean axioms (propext, Quot.sound, Classical.choice) are used.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The reader's weakest_assumption frames the concern as whether Lean's acceptance 'faithfully represents a mathematically valid proof' vs. being 'formally valid but mathematically vacuous.' This framing does not precisely land. In Lean, a sorry-free proof of a correctly stated theorem using standard axioms is mathematically valid by construction — there is no room for 'vacuous but type-correct' proofs of non-trivial theorem statements. The only way the central claim could fail is if (a) the proof is not actually sorry-free, (b) non-standard axioms were introduced, or (c) the formal theorem statement does not encode the intended mathematical claim. The paper's Section 2 definitions of SpherePacking, density, E8, and the main theorem statement all appear standard and correct. The paper's own acknowledgment that 'the exact correspondence between the autoformalization and the intended proof path is still being investigated' concerns mathematical exposition and understandability, not correctness — if the main theorem is sorry-free, it is proven regardless of whether the intermediate lemmas follow the intended path. The genuine load-bearing gap is simpler and more concrete: the paper references 'PR #341' without providing a repository URL or commit hash, so the sorry-free claim cannot be independently verified from the paper alone. This is a verifiability deficit, not a logical flaw in the argument.","agreement_with_reader":"partial"},"referee_report":{"model":"glm-5.2","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.","tokens_in":8510,"tokens_out":1661,"duration_ms":31762,"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":[{"comment":"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.","section":null},{"comment":"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.","section":null}],"minor_comments":[{"comment":"Reference [4]: 'A First Course in Modular Farms' should read 'A First Course in Modular Forms.'","section":null},{"comment":"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.","section":null},{"comment":"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.","section":null},{"comment":"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.","section":null},{"comment":"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.","section":null},{"comment":"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.","section":null}],"recommendation":"major_revision","confidential_remarks":"The paper is essentially a project progress report rather than a traditional research paper, and much of the technical detail is deferred to a 'forthcoming paper.' The central claim — a sorry-free Lean formalization exists — is significant and likely true, but the lack of an accessible artifact URL or commit hash means it cannot be verified from the paper alone. This is the primary reason for the major revision recommendation; if the authors provide a verifiable artifact link and confirm the axiom basis, the paper could proceed to minor revision. The paper may also be better suited to a venue that publishes project announcements or formalization reports, though this is an editorial judgment."},"author_rebuttal":{"model":"glm-5.2","summary":"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.","responses":[{"response":"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_made":"yes","referee_comment":"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."},{"response":"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_made":"yes","referee_comment":"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."}],"tokens_in":7981,"tokens_out":582,"duration_ms":19961,"standing_objections":[]},"desk_editor":{"model":"glm-5.2","letter":"The headline: a sorry-free Lean formalization of Viazovska's dimension-8 sphere packing theorem exists, with roughly 40,000 lines of the 60,000-line development completed by Math, Inc.'s autoformalization model Gauss in five days. That is a real milestone — no prior formalization of this result existed, and the scale of AI-assisted proof completion here is genuinely new. The author list includes Viazovska herself, which adds credibility to the formalization strategy and the theorem statement. The Lean definitions in Section 2 (SpherePacking, density, E8 lattice, the main theorem statement) all look standard and correctly encode the intended mathematics. The human-written portions — modular form infrastructure, contour parametrizations, the `complex_norm` tactic — are solid work that would be useful to the broader Lean community regardless of the main theorem. The paper is also refreshingly honest about the state of the project: it calls itself a progress report, not a finished account, and a full technical paper is forthcoming. That framing is appropriate and accurate. The soft spots are concrete and mostly minor. The main one: the paper references PR #341 but gives no repository URL or commit hash, so the sorry-free claim cannot be independently verified from the paper alone. This is a verifiability deficit, not a logical flaw — if the proof is sorry-free under standard axioms, it is correct by construction. The reader's worry about 'mathematically vacuous but type-correct' proofs does not really apply to Lean: a sorry-free proof of a correctly stated theorem using standard axioms is a valid proof. The paper's own acknowledgment that 'the exact correspondence between the autoformalization and the intended proof path is still being investigated' concerns mathematical exposition and understandability of the Gauss-generated lemmas, not the correctness of the main theorem. The Section 4 discussion of Gauss's code quality (auxiliary definitions with no API, reproof of trivial facts, long unmaintainable proofs) is a legitimate concern for the codebase but not for the correctness of the result. One thing I disagree with in the reader's take: the significance score of 8.0 is if anything slightly low. A machine-checked proof of a Fields Medal result, combined with a demonstration that current AI autoformalization can complete frontier-level formalization at this scale, is a landmark for both formal mathematics and AI-assisted theorem proving. This paper is for formal mathematicians, AI-for-math researchers, and anyone interested in the state of automated proof completion. It deserves a serious referee who can check the Lean artifact and assess the Gauss-generated portions. The paper should be sent back with a request to add the repository URL and commit hash before acceptance — that is a small, fixable gap that currently prevents independent verification.","headline":"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.","tokens_in":9215,"tokens_out":661,"would_cite":true,"duration_ms":43760,"reading_group":"no","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["52C17","11F11","68V20"],"pacs":[],"model":"glm-5.2","headline":"Lean formally verifies the E8 sphere packing theorem in dimension 8","keywords":["sphere packing","formalization","Lean theorem prover","E8 lattice","modular forms","autoformalization","Cohn-Elkies bound","quasimodular forms"],"falsifier":"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.","tokens_in":8508,"feed_emoji":"🔵","tokens_out":1093,"duration_ms":46516,"temperature":0.7,"pith_summary":"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.","feed_headline":"E8 sphere packing theorem formally verified in Lean","feed_subtitle":"A 60,000-line proof with no gaps, completed with help from an autoformalization model, confirms the densest packing in eight dimensions.","key_machinery":"Cohn-Elkies linear programming bound; Viazovska's magic function constructed from quasimodular forms; contour integration identities; modular form dimension formulas","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Lean formally verifies Viazovska's E8 sphere packing proof","E8 sphere packing: fully formalized in Lean","Dimension-8 sphere packing theorem verified in Lean","No sorries: E8 sphere packing formalized in Lean","Human-AI collaboration formalizes E8 packing proof in Lean"],"cache_read_input_tokens":0,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Lean formally verifies Viazovska's E8 sphere packing proof","E8 sphere packing: fully formalized in Lean","Dimension-8 sphere packing theorem verified in Lean","No sorries: E8 sphere packing formalized in Lean","Human-AI collaboration formalizes E8 packing proof in Lean","Viazovska's magic function: E8 packing formally verified","Lean proof confirms optimal sphere packing in dimension 8","E8 lattice optimality: sorry-free formal proof in Lean","Formal proof of E8 sphere packing completed in Lean","Cohn-Elkies bound to Viazovska: E8 packing formalized in Lean","Gauss autoformalization model closes E8 packing proof in Lean","E8 packing density pi^4/384: formally verified, no gaps"]},"model":"glm-5.2","effort":"high","cost_usd":0.0,"raw_usage":{"total_tokens":824,"prompt_tokens":444,"completion_tokens":380,"prompt_tokens_details":null},"tokens_in":444,"tokens_out":380,"duration_ms":6910,"temperature":1.0,"reasoning_tokens":208,"cache_read_input_tokens":0,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-07-04T14:17:17.421910+00:00","model_set":{"reader":"glm-5.2"},"falsifier":"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.","supporting_citations":[],"review_version":2}