Problemi matematici che nemmeno gli esperti sanno risolvere? Ci pensa l'AI
Una nuova intelligenza artificiale specializzata nella matematica è riuscita a dimostrare congetture che per anni avevano messo in difficoltà i ricercatori.
Per decenni abbiamo pensato che certe dimostrazioni fossero un terreno esclusivo della mente umana. Poi è arrivata un’AI che risolve problemi matematici in modo autonomo, trovando collegamenti che nessuno aveva mai visto. Non è fantascienza, ma una storia vera giunta dal mondo della ricerca e che sta cambiando il modo in cui guardiamo alla matematica.
Quando un problema resta senza risposta per anni
Cinque anni fa, i matematici Dawei Chen e Quentin Gendron stavano lavorando a un teorema di geometria algebrica. Il loro ragionamento, però, si bloccò su una formula della teoria dei numeri che non riuscivano a dimostrare. Il risultato? Trasformare il teorema in una congettura, cioè un’ipotesi plausibile ma non verificata.
Come spesso accade, la questione rimase aperta. Nemmeno i colleghi più esperti riuscivano a sciogliere quel nodo. Chen provò persino a usare ChatGPT, sperando in un’intuizione, ma senza successo. La svolta arrivò per caso, durante una conferenza a Washington, quando raccontò il problema a Ken Ono, matematico noto e oggi parte della startup Axiom.
La mattina seguente, Ono tornò con una dimostrazione completa. Non l’aveva scritta lui, ma AxiomProver, un sistema di intelligenza artificiale matematica progettato per ragionare in modo formale sui teoremi.
Cos’è AxiomProver e perché è diverso dagli altri modelli
AxiomProver non è un semplice chatbot che riformula testi o cerca soluzioni in rete. È un sistema che combina modelli linguistici di grandi dimensioni con un motore logico capace di costruire e verificare dimostrazioni usando il linguaggio matematico Lean.
Questo significa che non si limita a “suggerire” una risposta: controlla ogni passaggio e verifica che sia formalmente corretto. Nel caso di Chen e Gendron, l’AI ha trovato un collegamento con un fenomeno numerico studiato già nel XIX secolo, individuando una strada che nessuno aveva mai considerato. La dimostrazione è stata poi pubblicata su arXiv, l’archivio pubblico di articoli scientifici.
Ken Ono ha raccontato che il sistema «ha trovato qualcosa che era sfuggito a tutti gli esseri umani». Un’affermazione forte, ma sostenuta dai fatti.
L’AI che risolve teoremi (e non solo uno)
La congettura di Chen non è un caso isolato. Axiom ha dichiarato che il suo sistema ha già prodotto diverse dimostrazioni di problemi rimasti irrisolti per anni. Una riguarda la cosiddetta congettura di Fel, legata alle “sizigie”, strutture algebriche complesse. In questo caso, AxiomProver non ha colmato una lacuna, ma ha costruito una dimostrazione completamente nuova.
Ancora più sorprendente è il legame con Srinivasa Ramanujan: alcune formule richiamate dall’AI erano apparse nei suoi taccuini oltre cento anni fa. Un’altra dimostrazione si basa su strumenti sviluppati per l’Ultimo teorema di Fermat, una delle sfide più celebri della matematica moderna.
Qui non siamo davanti a un assistente passivo, ma a una vera AI che risolve teoremi in modo autosufficiente, vagliando ogni passaggio.
Un nuovo modo di fare ricerca matematica
Secondo Carina Hong, amministratrice delegata di Axiom, la matematica è il banco di prova ideale per l’intelligenza artificiale. Se un sistema riesce a muoversi in un campo così rigoroso, in seguito può essere adattato ad altri contesti. Le stesse tecniche, per esempio, potrebbero aiutare a verificare la sicurezza del software o a individuare vulnerabilità informatiche.
Scott Kominers, professore alla Harvard Business School, ha definito “sorprendente” non solo il risultato, ma anche l’eleganza delle dimostrazioni prodotte dall’AI. Un giudizio che pesa, considerando che conosce sia la tecnologia sia i problemi risolti.
Come cambia il ruolo dei matematici
AxiomProver non sostituisce gli studiosi, ma li affianca. Ono parla di un nuovo paradigma: l’AI come partner di ricerca, capace di suggerire strade inattese e di rendere più rapido il processo di verifica. Chen, che ha visto risolta una sua congettura, è ottimista: «I matematici non hanno dimenticato le tabelline dopo l’invenzione della calcolatrice».
Oggi, con un’AI che risolve problemi matematici, non stiamo delegando il pensiero alle macchine. Stiamo ampliando gli strumenti con cui esplorare ciò che, fino a ieri, sembrava irraggiungibile. E la matematica, ancora una volta, mostra dove può arrivare l’ingegno umano quando decide di collaborare con le sue creazioni.
