Apr 2026
Sphere-Packing-Lean
Model / AI: Gauss
machine-checked
the formal verification of Viazovska's sphere-packing optimality in dimensions 8 and 24 completed with Math Inc's Gauss agent: dimension 8 finished in five days, dimension 24 autoformalized from the original paper in two weeks, with Viazovska, Buzzard, Avigad and others as named collaborators. 830 files and 180,661 lines with no sorry, no native_decide and no added axiom. The preprint covers the dimension-8 milestone only.
Source review pending. Imported from the original notes; linked claims and artifacts have not been re-audited in this restructuring.