L'AI risolve problemi matematici impossibili aperti da decenni

Neel Somani ha lasciato ChatGPT a pensare per 15 minuti. Quando è tornato, il modello aveva risolto un problema matematico aperto. Non un esercizio da liceo, ma uno di quei rompicapi che i matematici professionisti lasciano in sospeso perché troppo complicati o perché semplicemente nessuno ha ancora trovato il modo giusto di affrontarli. Somani ha verificato la dimostrazione con uno strumento chiamato Harmonic. E tutto quadrava.

Ero curioso di stabilire un punto di riferimento per capire quando gli LLM siano effettivamente in grado di risolvere problemi matematici aperti, ha raccontato l’ingegnere informatico ed ex ricercatore quantitativo. La sorpresa è stata scoprire che, con GPT 5.2, quella frontiera si era appena spostata un po’ più avanti. E non di poco.

I modelli AI risolvono enigmi matematici che nessuno aveva risolto

Dal Natale scorso, 15 problemi della celebre collezione di Paul Erdős sono passati da “aperti” a “risolti”. Erdős, matematico ungherese leggendario, ha lasciato in eredità oltre 1.000 congetture irrisolte che rappresentano un banco di prova perfetto per chiunque voglia misurarsi con la matematica di alto livello. Umani e, adesso, anche macchine.

Alcuni problemi sono stati risolti completamente dall’AI, altri con l’aiuto umano per verificare e raffinare il lavoro. Ma il punto è che sta succedendo, e anche velocemente.

La “catena di pensiero” di ChatGPT è impressionante da guardare. Il modello snocciola assiomi matematici come la formula di Legendre, il postulato di Bertrand, il teorema della Stella di David, uno dietro l’altro, costruendo ragionamenti complessi che fino a poco tempo fa sembravano prerogativa esclusiva degli esseri umani.

Nel caso testato da Somani, ChatGPT ha anche scovato un post su Math Overflow del 2013 dove il matematico di Harvard Noam Elkies aveva fornito una soluzione elegante a un problema simile. Ma invece di limitarsi a copiare, il modello ha elaborato una dimostrazione diversa in punti significativi e ha fornito una soluzione più completa a una versione del problema originariamente posta da Erdős stesso.

Per chiunque sia scettico nei confronti dell’intelligenza artificiale (e ce ne sono parecchi), questo è un risultato difficile da liquidare.

Non solo ChatGPT

La prima ondata di soluzioni autonome è arrivata a novembre da AlphaEvolve, un modello basato su Gemini. Da lì, altri hanno iniziato a testare GPT 5.2 con problemi di Erdős e hanno scoperto che il modello è più abile nel ragionamento matematico rispetto alle versioni precedenti.

Terence Tao, uno dei matematici più rispettati al mondo, ha offerto un’analisi più sfumata dei progressi sulla sua pagina GitHub. Secondo Tao, ci sono otto problemi in cui i modelli AI hanno compiuto progressi degni di nota, con altri sei casi in cui il progresso è avvenuto individuando e sviluppando ricerche precedenti.

Su Mastodon, Tao ha ipotizzato che la natura scalabile dei sistemi AI li renda più adatti a essere applicati sistematicamente alla coda lunga degli oscuri problemi di Erdős, molti dei quali hanno in realtà soluzioni lineari. In altre parole, ci sono problemi che sembrano difficili solo perché nessuno ha mai avuto il tempo o la pazienza di affrontarli metodicamente.

Non è una resa, ma un riconoscimento, le macchine stanno diventando straordinariamente brave in certi compiti matematici.

La formalizzazione, il segreto del successo

Un altro elemento cruciale in questa storia è la formalizzazione, un processo che rende il ragionamento matematico più facile da verificare ed estendere. La formalizzazione non richiede necessariamente l’uso dell’AI o persino dei computer, ma è un lavoro noioso e ripetitivo. Esattamente il tipo di compito in cui le macchine eccellono.

Lean, l‘assistente alla dimostrazione open source sviluppato da Microsoft Research nel 2013, è diventato lo standard del settore per formalizzare le prove. E strumenti AI come Aristotle di Harmonic sono in grado di automatizzare gran parte di questo lavoro, rendendo possibile tradurre dimostrazioni informali in codice verificabile in pochissimo tempo.

Tudor Achim, fondatore di Harmonic, è meno interessato al numero di problemi risolti e più al fatto che i grandi matematici stiano iniziando a prendere sul serio questi strumenti. Queste persone hanno una reputazione da proteggere, quindi quando dicono di usare Aristotle o ChatGPT, quella è una prova reale.

L’AI deve fare ancora molta strada

Nonostante i progressi impressionanti, siamo ancora lontani da sistemi AI capaci di fare matematica senza l’intervento umano. La maggior parte delle soluzioni richiede verifica, raffinamento, contesto aggiuntivo fornito da esperti umani. L’AI trova strade, ma spesso è un matematico a decidere se quella strada porta davvero da qualche parte.

Tuttavia, il ruolo dei modelli linguistici di grandi dimensioni nella ricerca matematica è ormai innegabile. Non sono più giocattoli o curiosità. Sono strumenti che professori con decenni di esperienza stanno integrando nel loro lavoro, e i risultati parlano da soli.