Nel panorama dell'intelligenza artificiale applicata alle scienze formali, sta avvenendo qualcosa che fino a pochissimo tempo fa sembrava fantascienza accademica: i sistemi AI stanno dimostrando capacità matematiche che sfidano i confini tradizionali tra ragionamento umano e computazione automatica. Non si tratta di semplici calcoli o di risoluzione di equazioni elementari, ma di affrontare problemi di ricerca autentici, produrre dimostrazioni formali complesse e verificare lavori premiati con la Medaglia Fields, il riconoscimento più prestigioso della matematica mondiale. La velocità di questo progresso ha colto di sorpresa persino i matematici più attenti all'evoluzione tecnologica, ridisegnando in pochi mesi le proiezioni che sembravano solide appena un anno fa.
Il segnale più eloquente di questo cambio di paradigma viene da Daniel Litt, matematico dell'Università di Toronto, che nel marzo 2025 aveva scommesso con un collega che le probabilità di un'AI capace di produrre ricerca matematica ai livelli dei migliori accademici entro il 2030 fossero solo del 25 per cento. A distanza di un anno, Litt ha pubblicamente dichiarato sul suo blog di aspettarsi di perdere quella scommessa. "Fino a qualche anno fa questi strumenti erano sostanzialmente inutili persino per problemi di matematica delle scuole superiori, e ora riescono a volte a risolvere problemi che compaiono realmente nella vita di ricerca di un matematico", ha spiegato.
Questa traiettoria di miglioramento accelerato si era già manifestata nel 2024, quando sistemi sviluppati da OpenAI e Google DeepMind avevano ottenuto prestazioni equivalenti alla medaglia d'oro alle Olimpiadi Internazionali di Matematica, una competizione d'élite per studenti delle scuole superiori che molti esperti consideravano fuori portata per qualsiasi AI. A gennaio, matematici hanno iniziato a utilizzare strumenti analoghi per affrontare problemi formulati decenni fa dal matematico ungherese Paul Erdős e rimasti irrisolti. L'accelerazione non accenna a fermarsi, e la comunità accademica si trova ora a fare i conti con implicazioni che vanno ben oltre la curiosità scientifica.
A febbraio, Nikhil Srivastava dell'Università della California a Berkeley e i suoi collaboratori hanno lanciato il progetto First Proof, con l'obiettivo esplicito di costruire un benchmark più realistico per misurare le capacità matematiche dei sistemi AI. Il progetto ha raccolto 10 problemi emersi direttamente dall'attività quotidiana di ricerca dei partecipanti, spaziando tra campi matematici profondamente diversi. "Erano problemi naturalmente emersi nella nostra ricerca di tutti i giorni", ha precisato Srivastava. "Non erano impossibili, ma neanche routine. C'era davvero un ampio spettro di difficoltà."
Le risposte non si sono fatte attendere. I team di OpenAI e Google DeepMind hanno sottoposto i propri modelli alla prova: OpenAI ha dichiarato di aver risolto correttamente 5 problemi su 10, secondo valutazioni di esperti esterni, mentre Google DeepMind ha ottenuto un punteggio di 6 su 10. "Le cose sono cambiate così in fretta", ha commentato Thang Luong di Google DeepMind. "Ora l'AI è diventata un collaboratore serio, capace di produrre vero lavoro di ricerca o, come nel caso di First Proof, di proporre soluzioni in autonomia."
Lo strumento utilizzato da Google si chiama Aletheia e combina una versione computazionalmente intensiva del modello Gemini con un algoritmo di verifica progettato per identificare errori nelle soluzioni candidate. Il sistema è in grado di generare miglioramenti iterativi in modo autonomo fino a convergere su una risposta. Google non ha divulgato il numero di iterazioni necessarie per ciascun problema, rendendo difficile una valutazione comparativa precisa, ma i risultati hanno comunque impressionato la comunità matematica. Sul problema numero 8, in un'area di nicchia della geometria, cinque dei sette esperti consultati da Google hanno concordato sulla correttezza della soluzione proposta. Ivan Smith dell'Università di Cambridge, esterno al progetto, ha osservato che l'approccio adottato dal sistema mostra una direzione sensata. "Se fosse uno studente di dottorato a tornare con queste riflessioni, sarebbe incoraggiante e aumenterebbe la fiducia nel fatto che il risultato sia effettivamente corretto", ha dichiarato.
Un nodo critico che emerge con forza da questa fase di sviluppo è la questione della verifica: i sistemi AI rischiano di generare dimostrazioni più velocemente di quanto i matematici umani riescano a controllarle. È qui che entra in gioco un secondo filone di innovazione, quello della formalizzazione automatica delle dimostrazioni, ovvero la traduzione di prove scritte in linguaggio naturale in codice verificabile da un computer. La startup Math, Inc. ha recentemente annunciato che il suo strumento Gauss ha formalizzato e verificato automaticamente la dimostrazione premiata con la Medaglia Fields 2022 della matematica ucraina Maryna Viazovska, relativa al problema dell'impacchettamento ottimale di sfere nello spazio.
Il percorso che ha portato a questo risultato merita attenzione per capire le dinamiche di collaborazione tra ricercatori umani e sistemi AI. Un gruppo di matematici, tra cui Bhavik Mehta dell'Imperial College London, aveva avviato autonomamente a fine 2024 un progetto per tradurre manualmente il lavoro di Viazovska in codice formale, partendo dalla soluzione in otto dimensioni. Math, Inc. aveva inizialmente offerto supporto a questo gruppo, ma ha poi annunciato di aver già completato una dimostrazione formale completa, seguita da una versione più generale per 24 dimensioni. Mehta e i suoi colleghi avevano sviluppato le definizioni matematiche fondamentali e la struttura di base del lavoro: senza questo contributo, il sistema AI non avrebbe potuto completare le sue dimostrazioni. "Avevamo costruito tutti i pezzi, ma non avevamo scritto il manuale di istruzioni per assemblarli", ha chiarito Chris Birkbeck dell'Università dell'East Anglia.
Il risultato finale è una dimostrazione di circa 200.000 righe di codice, pari a circa il 10 per cento dell'intera matematica formalizzata esistente. La verbosità è significativa: probabilmente un matematico umano avrebbe prodotto codice dieci volte più compatto per lo stesso risultato. Ma Johan Commelin dell'Università di Utrecht sottolinea il valore storico dell'impresa: "È un grande risultato. Si tratta di un lavoro premiato con la Medaglia Fields, e viene auto-formalizzato."
L'impatto più profondo di questi sviluppi potrebbe riguardare non tanto la produzione di nuova matematica quanto la struttura stessa della peer review. Commelin immagina un futuro in cui strumenti di formalizzazione automatica verifichino in tempo reale i paper scientifici alla ricerca di errori, trasformando radicalmente il processo di revisione tra pari. Questo scenario pone interrogativi seri sulla sostenibilità del modello attuale, ma anche sulle responsabilità epistemiche: chi risponde di una dimostrazione generata da un LLM e verificata automaticamente?
Non tutti i matematici accolgono con favore la prospettiva di delegare sempre più lavoro alle macchine. Anna Marie Bohmann della Vanderbilt University avverte che usare AI per risolvere i tipi di problemi affrontati in First Proof può produrre dimostrazioni concrete, ma elimina quella che lei chiama l'"opportunità di apprendimento". "La fatica di creare e formulare nuove idee, di affrontare problemi inediti, è uno dei principali modi in cui sia gli studenti sia i professionisti consolidano la propria conoscenza matematica." Tony Feng, membro del team Aletheia di Google DeepMind, condivide questa cautela e ammette di essere riluttante a usare lo strumento per il proprio lavoro: "Spesso sento che dovrei fare i miei compiti da solo, costruire la mia intuizione attraverso il processo."
Mehta aggiunge un ulteriore livello di complessità: anche formalizzare una dimostrazione può generare intuizioni matematiche preziose, e lui e i suoi colleghi dovranno ora districare le 200.000 righe di codice prodotte da Gauss per estrarre elementi potenzialmente utili per altri progetti. La densità opaca delle dimostrazioni generate da AI diventa essa stessa un problema di comprensibilità scientifica, un aspetto che la comunità matematica dovrà affrontare sistematicamente.
La prospettiva storica offerta da Commelin rimane però la più equilibrata: per secoli i calcoli manuali erano una componente centrale dell'attività matematica, poi sono stati completamente automatizzati, e la disciplina non solo è sopravvissuta ma si è espansa. "Credo che accadrà qualcosa di simile: cambieremo radicalmente quello che facciamo, ma tra 10 o 20 anni riconosceremo ancora come matematica quello che faremo, in uno stile nuovo." La domanda aperta, e non banale, è quale sarà la distribuzione del lavoro cognitivo tra ricercatori umani e sistemi AI in quel futuro, e come si formeranno le nuove generazioni di matematici in un ecosistema in cui molte delle sfide tradizionali vengono progressivamente assorbite dalla computazione automatica.