Problema di impacchettamento di sfere in dimensione 8 verificato formalmente in Lean

Maryna Viazovska ha affrontato la sfida dell'impacchettamento di sfere in otto dimensioni nel 2016, utilizzando forme modulari per creare una funzione 'magica' che soddisfacesse i criteri di ottimalità stabiliti da Henry Cohn e Noam Elkies nel 2003. Nel marzo 2024, insieme a Nivedita Hariharan, ha avviato un progetto volto a formalizzare questa soluzione all'interno del Lean Theorem Prover. Un risultato significativo è stato raggiunto nel febbraio 2026, quando il risultato ha ricevuto una verifica formale, con le fasi conclusive completate dal modello di autoformalizzazione 'Gauss' di Math, Inc. Questo sforzo mostra una partnership distintiva tra intelletto umano e intelligenza artificiale, con ulteriori obiettivi ancora da perseguire.