Math, Inc., a startup that develops an AI system called Gauss, says Gauss has helped complete a formal proof of Maryna Viazovska's sphere-packing results in dimensions 8 and 24. The proof is written in Lean, a proof assistant: software that checks every step of a proof mechanically.[1, 3] Viazovska proved the dimension-8 result in 2016 and the dimension-24 result with collaborators soon after, work that earned her the 2022 Fields Medal.[2] IEEE Spectrum reported on 2 March 2026 that Math, Inc. had announced the dimension-24 result that day, after a dimension-8 announcement on 23 February.[3]
According to EPFL, the project Formalising Sphere Packing in Lean began in 2024 after Viazovska met mathematician Sidharth Hariharan in Lausanne. The team wrote a detailed blueprint of the dimension-8 proof, a human-readable map of its components. It then translated the blueprint into Lean step by step.[2, 3]
Math, Inc. says Gauss then proved all remaining results needed for dimension 8 in five days. In two weeks it formalized the dimension-24 case using only the original paper as input, searching the literature when needed. The company puts the released formalization at about 200,000 lines of Lean, after automated refactoring reduced it from a peak of roughly 500,000 lines.[1]
EPFL calls Gauss's role decisive and describes it as helping to complete certain intermediate steps.[2] According to IEEE Spectrum, Gauss also found and fixed a typo in the published dimension-8 paper. The magazine adds that Gauss had no human blueprint to work from for the dimension-24 case.[3]
Sources
Check or correct this page
Verification record
The digest below shows whether the text you are reading matches the published source. It does not show that the reporting is correct. The build computes it from this page's Markdown source and lists it in the site manifest.
a46d00d9dd0ef3ae74aa1a6377d1d161ec23766e167608f69af11aabd386f6f5
