Verifica formale della Medaglia Fields tramite AI

Un'intelligenza artificiale ha verificato formalmente le prove matematiche della matematica ucraina Maryna Viazovska, vincitrice della Medaglia Fields nel 2022. Questo risultato segna un progresso significativo nelle capacità dell'AI di assistere nella ricerca matematica.

La ricerca premiata con la Medaglia Fields affrontava il problema dell'impacchettamento di sfere, ovvero come disporre cerchi o sfere identiche nello spazio n-dimensionale in modo più denso possibile. Viazovska aveva risolto il problema in 8 e 24 dimensioni, dimostrando che configurazioni specifiche (E8 e reticolo di Leech) sono le più efficienti.

La collaborazione uomo-AI

Il progetto "Formalising Sphere Packing in Lean" ha visto la luce grazie all'incontro tra Sidharth Hariharan e Viazovska. Hariharan, esperto nella formalizzazione di prove, ha collaborato con altri esperti per creare un "blueprint" leggibile che mappasse i vari elementi della prova in 8 dimensioni.

Successivamente, Math, Inc., una startup che sviluppa l'AI Gauss, ha accelerato il processo. Gauss è un modello linguistico progettato per formalizzare automaticamente le prove. Dopo aver completato la formalizzazione Lean del teorema dei numeri primi, Gauss ha dimostrato diversi fatti relativi al progetto di impacchettamento di sfere.

Risultati e implicazioni

Gauss non solo ha auto-formalizzato il caso a 8 dimensioni, ma ha anche individuato e corretto un errore di battitura nell'articolo pubblicato, il tutto in soli cinque giorni. Successivamente, ha formalizzato la prova a 24 dimensioni in due settimane, senza un blueprint preesistente.

Questo risultato rappresenta un punto di svolta per l'auto-formalizzazione e la collaborazione uomo-AI, aprendo la strada a una trasformazione rivoluzionaria nella matematica, dove le formalizzazioni su larga scala diventano comuni. Questo consente ai matematici di concentrarsi sulla creazione di nuove teorie matematiche.