Le AI trasformano la matematica, se le convinci

La società statunitense OpenAI ha da poco annunciato che un proprio sistema di intelligenza artificiale è riuscito a dimostrare una congettura matematica rimasta irrisolta per quasi cinquant’anni. Il risultato, che dovrà essere confermato e validato, si aggiunge a una lunga serie di annunci sui progressi in campo matematico delle AI, il cui impiego sta rivoluzionando il settore, consentendo di avere dimostrazioni in pochi giorni, a volte ore, rispetto agli anni di lavoro richiesti un tempo. Le potenzialità sono enormi, ma non è sempre semplice distinguere tra i veri progressi e gli annunci altisonanti delle aziende che sviluppano le AI.

La congettura risolta da GPT 5.6 Sol riguarda un particolare tipo di struttura matematica chiamata grafo, che non ha niente a che vedere con i grafici cartesiani che siamo abituati a studiare a scuola. Il modello di OpenAI è riuscito a trovare una dimostrazione che vale per tutti i casi previsti dalla congettura.

Il modello lo ha fatto in un’ora, dopo che per decenni molti matematici si erano scervellati sul problema. Ma non è stata solo questione di rapidità, ma di metodo, ed è questo l’aspetto che in generale sta incuriosendo di più gli esperti di AI e i matematici stessi. Per ottenere i migliori risultati, i modelli devono essere guidati e soprattutto incoraggiati a raggiungere l’obiettivo.

Quando si chiede a una AI di risolvere un problema matematico famoso e ancora irrisolto, il modello tende a scoraggiarsi perché nella sterminata serie di informazioni usate per il suo addestramento ci sono segni evidenti sulla difficoltà del compito assegnato. È probabile che il modello abbia assimilato dati sui lavori di grandi matematici che hanno fallito nel trovare il risultato, di conseguenza assume che sia impossibile trovare una soluzione e si arrende subito, oppure inventa una scusa o produce qualche allucinazione (cioè inventa di sana pianta la risposta).

Nel caso del recente problema posto a GPT 5.6 Sol gli ingegneri informatici di OpenAI hanno provato a seguire un approccio simile a quello usato da un insegnante a scuola, modulando severità e riscontri incoraggianti. Hanno quindi detto al modello che non si sarebbe potuto arrendere liquidando il problema come irrisolvibile, solo perché altri matematici avevano fallito. Ma hanno anche dato istruzioni più nette, chiedendo al modello di passare almeno 8 ore sul problema, prima di rinunciare.

Come in altri esperimenti simili condotti negli ultimi mesi e che hanno mostrato le capacità delle AI in matematica, quelli di OpenAI non hanno usato un singolo chatbot, ma hanno realizzato un’architettura più complessa. Hanno fatto in modo che il compito venisse delegato a 64 agenti, cioè sistemi con un certo livello di autonomia nello svolgere delle attività assegnate e coordinate dal modello. Gli agenti hanno lavorato in contemporanea proponendo passaggi matematici e controllandosi a vicenda, correggendo eventuali errori logici.

In questo modo il modello ha trovato una dimostrazione sorprendentemente breve, senza l’introduzione di concetti matematici rivoluzionari o mai sviluppati prima. L’AI ha usato metodi che gli umani avevano provato in passato e li ha combinati insieme, trovando infine la soluzione più logica alla questione che dovrà essere ora confermata dai matematici.

Il caso dei grafi è solo l’ultimo di una lunga serie di notizie sui progressi raggiunti dalle AI in matematica. La scorsa primavera nell’ambiente si era discusso molto del risultato ottenuto da Liam Price, un inglese senza formazione universitaria in matematica, che usando semplicemente ChatGPT era riuscito a risolvere un problema matematico rimasto insoluto per sessant’anni. Era il problema #1196 proposto nel 1966 da Paul Erdős, uno dei matematici più prolifici e geniali del Novecento.

Di recente il premio Nobel per la Fisica, Giorgio Parisi, ha raccontato con il fisico Francesco Zamponi di avere utilizzato il chatbot Claude per metterlo alla prova con uno dei fenomeni legati allo studio dei sistemi complessi (quelli con tanti sottosistemi che interagiscono tra loro e che possono essere descritti in modo analitico con la matematica).

Claude ha fornito una soluzione, lavorando con la supervisione dei due fisici che hanno corretto le incongruenze che produceva il modello, guidandolo quando andava fuori tema o rischiava di perdersi qualcosa. Alla fine il modello ha proposto una specifica funzione che è stata poi la chiave per chiudere la dimostrazione, un passaggio che Parisi e Zamponi non avevano valutato.

In molti casi le AI non sono quindi la soluzione al problema, ma uno strumento aggiuntivo per i matematici per valutare nuove idee, mettere insieme approcci seguiti da altri in precedenza e sperimentarli per il loro lavoro. Secondo molti di loro, in questo i modelli sono imbattibili perché hanno una conoscenza sterminata, dovuta all’enorme quantità di dati su cui si sono allenati.

I modelli si stanno dimostrando utili sia nelle congetture, sia nelle dimostrazioni. Le prime sono ipotesi o supposizioni che i matematici producono quando notano uno schema ripetitivo o delle regolarità nei numeri, intuendo che quel fenomeno potrebbe valere sempre. Una dimostrazione deve mostrare che la congettura è vera in ogni singolo caso possibile e senza eccezioni. Quando la congettura è dimostrata diventa spesso un teorema, una solida base per verificare altre congetture, per esempio.

Le AI si stanno rivelando molto abili nel trovare le dimostrazioni, usando la loro grande potenza di calcolo e la capacità di associare concetti distanti tra loro, in modo da costruire una sequenza logica. Spesso seguono i lavori già svolti da matematici, che si erano però fermati prima di arrivare a una soluzione, aggiungendo approcci meno convenzionali.

In matematica si seguono spesso schemi definiti: se per esempio un’equazione diventa troppo complicata, piena di eccezioni o di passaggi artificiosi, si tende a considerarla poco elegante e quindi meno promettente, preferendo cercare una strada diversa. A volte questo pregiudizio estetico diventa un freno per i matematici, mentre molti modelli AI sembrano dare meno peso a questi aspetti e tentano comunque di portare avanti la dimostrazione. Molto dipende da come viene accompagnato il loro ragionamento, correggendo e spronando come hanno raccontato Parisi e Zamponi.

Le dimostrazioni devono comunque essere verificate e tra gli strumenti più usati c’è Lean, un software che negli ultimi anni ha cambiato profondamente il modo di fare matematica. È un sistema di verifica formale che consente di controllare le dimostrazioni come se fossero codice informatico. Se un passaggio logico non è chiaro o non è corretto, Lean segnala un errore di compilazione e indica il punto in cui la logica non funziona più.

Il sistema richiede di inserire ogni singolo dettaglio, cosa che non fa un matematico quando lavora su carta (spesso omette i dettagli più ovvi, per fare prima). Per non dover scrivere sempre tutto da capo, i matematici possono usare Mathlib, una sorta di biblioteca digitale di matematica già formalizzata, con definizioni e risultati intermedi già verificati da altri. In questo modo possono costruire i nuovi teoremi partendo da una base solida e verificata.

Lean sta cambiando per molti il modo di fare matematica perché sta trasformando sempre di più la disciplina in un lavoro collettivo, molto più di quanto fosse un tempo quando i gruppi di matematici lavoravano spesso per conto proprio, prima di confrontarsi sui risultati. È la messa in pratica di maggior successo del Polymath Project, un’idea proposta nel 2009 dal matematico britannico Timothy Gowers proprio per incentivare la collaborazione tra matematici. L’iniziativa serviva a dimostrare che se un problema viene scomposto in diverse parti, su cui lavorano più gruppi, si può arrivare più facilmente a una soluzione.

Secondo alcuni matematici, le AI fanno qualcosa di simile, tenendo insieme non solo le conoscenze che hanno maturato durante il loro allenamento su quantità sterminate di dati, ma anche attraverso fonti specifiche e specializzate come Mathlib e Lean. Le AI specializzate in campo matematico sono spesso addestrate con questi sistemi, creando un ciclo in cui il modello apprende un ragionamento matematico ricevendo continuamente correzioni dal software, che verifica la sequenza logica dei passaggi.

Terence Tao, uno dei più importanti matematici viventi e vincitore della Medaglia Fields – spesso definita “il Nobel della Matematica” (il Nobel non la comprende tra le discipline considerate), in questi anni è diventato tra i più convinti promotori dell’impiego dell’AI nel suo campo di studio. In un’intervista sul sito di Nature ha detto che la fase della negazione nell’elaborazione del lutto legato alle AI in matematica è ormai svanita: i modelli iniziano a rendersi più utili di quanto potesse apparire anche solo un paio di anni fa (nonostante chi li produceva cercasse di promuoverli come già altamente avanzati).

Secondo Tao, le AI sono ideali per lavorare sulla matematica, perché non possono produrre errori che non possono essere verificati. Al tempo stesso, Tao ricorda che per ora il processo di controllo tramite i sistemi di verifica formale è inevitabile, e che quindi i modelli non sono affidabili a sufficienza per essere usati da soli. Dice che in tempi brevi il modo di fare matematica cambierà: invece di studiare un problema per volta, strumenti sempre più raffinati consentiranno di risolvere migliaia di problemi contemporaneamente, con risultati che potranno essere usati per studi statistici utili ad arrivare alla soluzione delle congetture più complesse.

Non tutti condividono l’entusiasmo di Tao, anche se i risultati recenti offerti dalle AI stanno portando a ripensamenti anche tra i più scettici. La critica che viene mossa più spesso è che le AI ottengono risultati grazie a una perseveranza “meccanica” e non grazie all’intuizione creativa, che ha distinto alcune delle soluzioni matematiche più eleganti. Un’altra preoccupazione è legata alle allucinazioni, anche se in realtà i modelli sono diventati via via più precisi e riescono a tenersi meglio sotto controllo, proprio per evitare risposte campate in aria.

Come sa bene chi li usa di frequente, i modelli di intelligenza artificiale tendono a fornire raramente le fonti su cui hanno basato le loro risposte, semplicemente perché attingono a una enorme quantità di informazioni difficilmente riconducibile a un’unica fonte (salvo non si tratti di richieste estremamente precise e puntuali). Per la matematica statunitense Melanie Wood è un problema di «negligenza professionale»: se un matematico presentasse idee altrui come proprie senza citarle, sarebbe duramente criticato e sanzionato dalla comunità accademica.

Oltre all’etica professionale, ci sono anche questioni più pratiche. Come per altre discipline scientifiche, la matematica richiede un costante allenamento fatto non solo di studio, ma anche di pratica e calcolo. È in questo modo che si mantiene allenato il proprio “muscolo mentale”, fino dai primi anni in cui si studia la materia in ambito accademico. La preoccupazione di molti matematici, compreso Tao, è che un uso precoce delle AI porti i meno esperti ad allenarsi di meno, costruendo basi meno solide per i loro studi successivi. Per questo si sta discutendo di come integrare l’impiego delle AI nei percorsi di studio, trovando il giusto equilibrio per evitare di mettere a rischio la formazione di nuovi ricercatori.

Trovare quell’equilibrio non è però semplice, considerato che gli strumenti di AI sono facilmente accessibili e ormai onnipresenti su computer e smartphone. Joel David Hamkins, un matematico dell’University of Notre Dame (Indiana, Stati Uniti) ha detto a Quanta di avere smesso di assegnare esercizi a casa ai propri studenti, perché aveva notato che erano quasi tutti scritti con le AI.

Le società che sviluppano questi sistemi hanno del resto un grande interesse nel diffonderli il più possibile, vista la necessità di generare ricavi per rientrare dai grandi investimenti per il loro sviluppo. E queste società possono spendere l’equivalente di centinaia di migliaia di euro su un singolo progetto, una cosa improponibile per molti gruppi di ricerca e per le università. Maryna Viazovska, vincitrice della Medaglia Fields e tra le più importanti matematiche al mondo, ne sa qualcosa.

Per oltre due anni Viazovska aveva lavorato con un gruppo di matematici alla formalizzazione di una propria celebre dimostrazione, usando proprio Lean per verificarne l’assoluta correttezza. Mentre era quasi arrivata alla fine della mole gigantesca di istruzioni da dare al sistema di verifica, scoprì che la startup statunitense Math aveva usato il proprio sistema di intelligenza artificiale Gauss per completare lo stesso compito. Ci aveva messo appena cinque giorni e l’operazione era costata a Math circa 100mila dollari in potenza di calcolo. Erano stati “gaussati”, come avrebbe detto in seguito Viazovska, accusando le aziende come Math di avere violato l’etichetta accademica, trasformando la ricerca in una sorta di corsa agli armamenti per il calcolo.