What was already known
The mathematical optimality results were established by Viazovska and by Cohn, Kumar, Miller, Radchenko and Viazovska in 2016. The new contribution is formalization, building on the human project begun by Hariharan and Viazovska in 2024.
What changed and why it matters
Supplies a landmark AI-assisted formalization of established mathematics, with substantial reusable analytic and geometric infrastructure.
The AI contribution
Gauss completed remaining proofs on top of the human repository, blueprint and mathematical design. Retain the work of Hariharan, Viazovska, Birkbeck, Lee, Ma, Mehta and the wider Lean community, as well as the original theorem authors. The dimension-24 work used the original paper and automated literature searches.
Limitations
This is not a new mathematical resolution of sphere-packing optimality, and periodic uniqueness does not assert uniqueness for every conceivable packing. Reported checking was not rerun by AIProofWatch. Completion of these theorem proofs does not finish the maintainers’ broader work on reusable, maintainable formal infrastructure. The date records the maintainers’ joint public account; their paper describes the dimension-eight milestone as February 2026.
Verification evidence
Evidence labels show what supports the claim. Importance rates its impact if correct.
Author claim
The cited source reports the scoped contribution. Statement and significance review does not establish a complete proof audit.
Accessible artifact / proof
The supporting manuscript, formal development or construction data is accessible; AIProofWatch has not independently reproduced its checks.
Formal checking
Checking is attributed to the linked account and was not rerun by AIProofWatch.
Checker: Sphere Packing maintainers and David Renshaw (reported)
Scope: Maintainers report checking unchanged definitions and standard Lean axioms, and manual/lean4checker checks of the dimension-eight code; Math, Inc. reports completion of dimensions 8 and 24.
Basis: Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Correction and publication history
News-led review of the precise source statement, baseline, AI attribution and importance. Historical inclusion without subscriber alerts; no AIProofWatch full proof audit.
Read this published revision