Gauss: AI-assisted sphere-packing formalization in dimensions 8 and 24

Understanding the problem

Why it matters

If correct, supplies a landmark AI-assisted formalization of established mathematics, with substantial reusable analytic and geometric infrastructure.

What counts as progress

A sourced advance or substantial formalization with the exact target, hypotheses, baseline and AI role stated. Importance and verification are assessed separately.

What to watch for

• Compare the precise hypotheses and baseline; retain human and prior-work attribution.
• 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.

Background review: 2026-10-11. Selected sources:

• Math, Inc.: reported formalization and scope
• Pinned Gauss-assisted Lean development
• Project maintainers: attribution, checking and remaining work
• Human project paper: dimension-eight formalization