An AI finished making a Fields Medal proof about packing spheres fully computer-checked
A team began in 2024 to turn Maryna Viazovska's proof into code a computer can check. Math Inc's AI, Gauss, finished it in February 2026.
Maryna Viazovska proved that one arrangement, called E8, is the densest way to pack spheres in eight dimensions. The work is part of what won her a Fields Medal. That proof is now fully checked by computer, with an AI finishing work that people had been building for two years.
In March 2024 a team began rewriting the proof in Lean, a language in which a computer checks every step. A paper posted on 25 April 2026 (arXiv 2604.23468, by Hariharan, Birkbeck, Lee, Ma, Mehta, Poiroux and Viazovska) reports that the whole proof passed Lean’s final check in February 2026.
The final stages were done by Gauss, an AI from Math, Inc. that turns human-written maths into a form a computer can check (autoformalization). Its code passes the check but is messy. The authors list redundant helper definitions and re-proofs of results already in Mathlib, Lean’s shared library, and say clean-up is ongoing.
What it means
For this proof, nobody has to rely on experts’ word any more: a computer has checked every step. AI can now do part of the slow work of turning a proof into that checkable form, though people still have to tidy its output. The proof itself is Viazovska’s; the AI translated it.
Caveats
- Gauss translated an existing human proof into checkable code. It did not find the proof, and its code still needs cleaning up.
- The paper does not give the exact day in February 2026; this entry is dated by the paper’s April publication.
- Widely repeated figures for how long Gauss took and how much code it wrote could not be verified and are not included here.