---
id: "2026-03-01-gauss-sphere-packing-formalization"
url: "https://postcutoff.com/e/2026-03-01-gauss-sphere-packing-formalization/"
as_of: "2026-11-13T13:49:00+01:00"
date: "2026-03-01"
date_precision: month
category: science
importance: 4
confidence: high
status: [Result confirmed]
verification: Lean-verified
sources: 2
editor: human editor
human_review: null
version: "2026-10-04"
---

As of: 2026-11-13 13:49 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-03-01-gauss-sphere-packing-formalization/

# Math Inc's Gauss formalises Viazovska's sphere-packing proofs in dimensions 8 and 24, fixing errors in the originals

Math Inc's Gauss agent completed the Lean formalisation of Maryna Viazovska's Fields-Medal proofs of optimal sphere packing in dimensions 8 (5 days) and 24 (~2 weeks), about 180,000 lines. Along the way it found and fixed a sign error and an incomplete step in the published proofs.

## Key facts
- Dimension 8: 5 days, code grew from ~20k to ~60k lines; dimension 24: ~2 weeks
- Final code ~180k lines (some sources say ~200k)
- Found a sign error in Proposition 7 (dim 8) and an incomplete step in Appendix A (dim 24)
- Write-up arXiv 2604.23468; exact announcement day not verified

## What happened

Gauss took over a partial human Lean project on sphere packing and finished both dimensions, reporting the errors it found in the literature.

## Why it matters

AI autoformalization reached Fields-Medal-level proofs, strengthening the case that formal verification can keep up with the flood of AI-generated mathematics.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): in its training data
- Claude Opus 5.5 (training cutoff June 2026): in its training data
- Gemini 4 Hydrogen (training cutoff March 2026): in its training data
- Grok 4.7 (training cutoff May 2026): in its training data

## Sources

1. [Formalizing sphere packing in dimensions 8 and 24 (arXiv 2604.23468)](https://arxiv.org/abs/2604.23468) (arxiv.org, paper)
2. [GitHub: math-inc/Sphere-Packing-Lean](https://github.com/math-inc/Sphere-Packing-Lean) (github.com, code)

## Changes

- 2026-09-29 (filed): Created

## Related

- 2026-09-04: [Claude produces the first complete machine-checked proof of Fermat's Last Theorem in Lean, in 11 days](https://postcutoff.com/e/2026-09-04-claude-formalizes-fermats-last-theorem/index.md)
- 2025-09-10: [Math Inc's Gauss agent completes the Strong Prime Number Theorem formalisation in Lean in three weeks](https://postcutoff.com/e/2025-09-10-math-inc-gauss-strong-pnt/index.md)