DeepMind sfiora la medaglia d’oro all’IMO: AlphaProof stupisce il mondo della matematica.
Ogni estate, tra silenziose aule universitarie e fogli pieni di simboli, i migliori talenti matematici del pianeta si sfidano in quella che è conosciuta come la “Coppa del Mondo della matematica”: l’International Mathematical Olympiad (IMO). Un palcoscenico dove genio, intuizione e rigore si fondono in sei problemi da risolvere in due giorni.
Negli ultimi anni, l’IMO ha smesso di essere soltanto un’arena per giovani umani prodigio. È diventata anche un banco di prova per l’intelligenza artificiale, che tenta di avvicinarsi a un territorio finora inaccessibile: la risoluzione rigorosa di problemi matematici complessi. Un obiettivo che un tempo sembrava utopia e che ora, grazie ai progressi nei modelli linguistici e nel formalismo matematico, appare sempre più concreto.
Tra le sfide più ardue, una è rimasta costante: non basta “indovinare” la risposta. Serve costruire un’intera dimostrazione, passo dopo passo, senza errori. Ed è qui che il linguaggio naturale ha spesso mostrato i suoi limiti, rendendo necessaria una nuova frontiera: la formalizzazione automatica del pensiero matematico.
A questo scopo, DeepMind ha avviato un percorso radicalmente nuovo, unendo il linguaggio formale Lean, le reti neurali su larga scala e un sistema di apprendimento per rinforzo ispirato ad AlphaZero. Il risultato? Una macchina capace di apprendere le regole della dimostrazione matematica come se fossero le mosse di una partita a scacchi.
Il nuovo sistema, chiamato AlphaProof, non ragiona in linguaggio naturale ma traduce i problemi in codice formale Lean, dove ogni passo è controllabile da un computer. Niente scorciatoie o intuizioni vaghe: ogni dimostrazione è verificata meccanicamente. Un approccio che, per la prima volta, ha portato l’AI a ottenere un punteggio da medaglia in un evento d’élite come l’IMO.
AlphaProof ha lavorato su una base di 80 milioni di proposizioni matematiche formalizzate e ha imparato a costruire dimostrazioni attraverso migliaia di simulazioni, usando tecniche simili alla ricerca Monte Carlo. Non prova ogni strada a caso, ma sceglie traiettorie strategiche, proprio come un matematico esperto esplora un teorema.
Nel 2024, AlphaProof ha totalizzato 28 punti su 42 all’IMO, risolvendo quattro problemi su sei, compreso l’infame Problema 6, uno dei più difficili di sempre. Solo 5 studenti umani nel mondo hanno ottenuto il punteggio pieno su quel quesito. Il sistema ha così raggiunto il livello di una medaglia d’argento, mancando l’oro per un solo punto.
Tre problemi sono stati risolti interamente da AlphaProof (due di algebra e uno di teoria dei numeri), mentre una questione di geometria è stata risolta dal modello AlphaGeometry 2, specializzato nel settore. Le due domande di matematica combinatoria, invece, sono rimaste irrisolte a causa della loro struttura difficilmente formalizzabile.
Questo traguardo rappresenta un salto qualitativo nella capacità dell’intelligenza artificiale di ragionare matematicamente. Il noto matematico Timothy Gowers ha definito alcune costruzioni di AlphaProof “ben oltre ciò che pensavo potesse fare un’IA oggi”. Ma il futuro promette ancora di più: se oggi AlphaProof assiste nella verifica, domani potrebbe diventare il compagno ideale per scoprire congetture ancora irrisolte.