{"id":"arxiv/2604.23468","url":"https://arxiv.org/abs/2604.23468","tags":["math.MG","cs.AI","cs.LO","math.NT"],"score":0,"title":"Progress in Formalizing Sphere Packing in Dimension 8","domain":"math.MG","source":"arxiv","authors":["Sidharth Hariharan","Christopher Birkbeck","Seewoo Lee","Ho Kiu Gareth Ma","Bhavik Mehta","Auguste Poiroux","Maryna Viazovska"],"reviews":0,"subject":"math.MG","summary":"In 2016, Viazovska famously solved the sphere packing problem in dimension $8$, using modular forms to construct a 'magic' function satisfying optimality conditions determined by Cohn and Elkies in 2003. In March 2024, Hariharan and Viazovska launched a project to formalize this solution and related mathematical facts in the Lean Theorem Prover. A significant milestone was achieved in February 2026: the result was formally verified, with the final stages of the verification done by Math, Inc.'s autoformalization model 'Gauss'. We discuss the techniques used to achieve this milestone, reflect…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-25","reactions":{}}