L’AI ha risolto problemi aperti. Ma ha capito la matematica?

Da un mese a questa parte, sui social e sulle riviste specializzate circola una notizia che sta scatenando entusiasmo e allarme in egual misura: i Large Language Model hanno iniziato a risolvere problemi matematici aperti da decenni. Congetture che resistevano da anni sono state smentite, e Google e OpenAI hanno pubblicato risultati che sembrano annunciare una nuova era per la matematica assistita dall’intelligenza artificiale.

Ma quanto è reale tutto questo? Come siamo arrivati fin qui, e cosa ne pensano davvero i matematici? In questo articolo ripercorro la storia recente di questo trend e provo a fare un po’ di chiarezza distinguendo l’hype dal reale avanzamento scientifico, aggiungendo anche qualche riflessione personale da chi lavora ogni giorno con questi strumenti.

La matematica ha sempre avuto una caratteristica che la rendeva, fino a poco tempo fa, un terreno relativamente sicuro rispetto all’avanzata dell’intelligenza artificiale: la sua natura estremamente formale. Al contrario della scrittura creativa o della programmazione, dove esiste una certa tolleranza all’ambiguità, in matematica una dimostrazione è corretta oppure non lo è. Non ci sono mezze misure. Per anni questo ha fatto pensare a molti che la matematica pura sarebbe stata una delle ultime roccaforti dell’intelligenza umana. Gli eventi degli ultimi mesi stanno mettendo in discussione anche questa convinzione.

Dal disastro aritmetico al Reinforcement Learning

Per capire la portata di questo cambiamento, bisogna tornare indietro di appena tre anni. Nel 2023, le prime versioni di ChatGPT erano sorprendentemente fragili sulla matematica: bastavano somme relativamente semplici per far cadere il modello in errore. Chi ha usato quei primi LLM lo ricorda bene, ed è uno dei motivi per cui, ancora oggi, molti utenti trattano con scetticismo le capacità matematiche di questi sistemi.

La svolta arriva con una tecnica di addestramento chiamata Reinforcement Learning from Verifiable Rewards, spesso abbreviata in RLVR. L’idea, in parole semplici, è allenare i modelli su migliaia di problemi per cui conosciamo già la soluzione corretta, premiandoli quando ci arrivano. Questo approccio ha funzionato benissimo sia per il codice — non è un caso che gli LLM siano diventati ottimi programmatori — sia per una parte della matematica.

Grazie a questi miglioramenti nella fase di addestramento, a giugno 2025 sia OpenAI sia Google DeepMind annunciano di aver risolto problemi di livello da medaglia d’oro alle Olimpiadi Internazionali di Matematica. È un traguardo importante, ma è solo l’inizio di quello che accade nei mesi successivi.

Il salto di qualità: LLM più proof assistant

A maggio 2026 la storia si fa più interessante. Alcuni ricercatori iniziano a dichiarare di aver risolto problemi aperti lasciati da Paul Erdős, il leggendario matematico ungherese noto per aver formulato centinaia di congetture, molte delle quali ancora senza soluzione. Tra questi ricercatori c’è Google, che pubblica un paper considerato fondazionale su questo tema, disponibile su arXiv. Il punto centrale del lavoro di Google è l’interazione tra un LLM e Lean, un cosiddetto proof assistant.

Lean funziona un po’ come il compilatore di un linguaggio di programmazione: non risolve il problema al posto tuo, ma verifica se la soluzione che gli proponi ha senso dal punto di vista logico-formale. È lo stesso principio dei verifiable rewards visto prima, applicato però non in fase di addestramento ma direttamente in fase di inferenza. Nella pratica, il sistema funziona in modo agentico: l’LLM genera diverse possibili dimostrazioni, e Lean scarta quelle che non “compilano”, cioè che non sono formalmente valide.

Questo permette al modello di esplorare solo le strade più promettenti. Il risultato è notevole: usando questa combinazione, il sistema di Google risolve nove problemi di Erdős su 353 analizzati, e dimostra 44 congetture su 492 tratte dalla OEIS, l’Online Encyclopedia of Integer Sequences, con un costo di inferenza di poche centinaia di dollari a problema. Un dettaglio cruciale emerso dagli esperimenti del paper: usare da solo un sistema specializzato come AlphaProof non basta a risolvere questi problemi. È la combinazione tra il ragionamento in linguaggio naturale dell’LLM e la verifica formale di Lean a fare la differenza. Inoltre, sostituire il modello con una versione meno capace fa crollare i risultati.

Da sviluppatore, questo schema mi è familiare: è esattamente la stessa logica che uso ogni giorno quando lascio che un modello generi codice e mi fido solo se i test automatici passano, non se “sembra” corretto. Vedere lo stesso pattern riemergere in un ambito così distante dal software, mi convince che il vero collo di bottiglia dell’AI generativa non è mai stato soltanto il ragionamento. Il problema è l’assenza di un giudice affidabile. Ogni volta che riusciamo a costruire quel giudice, il progresso accelera in modo quasi improvviso.

Il tweet che ha aperto le porte: la congettura giacobiana

A luglio 2026 succede qualcosa che accelera ulteriormente il dibattito. Un dipendente di Anthropic, durante la finale dei Mondiali, chiede a un modello di trovare un controesempio alla famosa congettura giacobiana, un problema aperto in matematica da decenni. Il modello lo trova, e il ricercatore lo pubblica su X.

Vale la pena soffermarsi su cosa renda la congettura giacobiana un caso particolarmente indicativo. Si tratta di un problema di geometria algebrica formulato per la prima volta nel 1939, che riguarda le condizioni sotto cui una particolare classe di trasformazioni polinomiali multivariate ammette un inverso altrettanto polinomiale.

È un problema tecnico, lontano dall’intuizione comune, ma proprio per questo emblematico: se un modello linguistico può trovare un controesempio a una congettura di questo tipo, aperta da oltre ottant’anni, significa che è in grado di navigare spazi di ricerca estremamente vasti e specialistici, ben oltre quanto un essere umano potrebbe fare manualmente in tempi ragionevoli. La particolarità di questo caso è che un controesempio si può verificare quasi immediatamente: basta controllare che soddisfi le condizioni del problema.

La community matematica lo conferma in tempi rapidi, e la notizia si diffonde. Da quel momento, decine di altre persone iniziano a “cacciare” problemi matematici più o meno oscuri usando gli LLM, postando i risultati sui social. Qui però nasce un problema strutturale: se per un controesempio la verifica è immediata, per molti altri tipi di risultati non lo è affatto. Serve un esperto per valutare la rilevanza, l’originalità e la correttezza di una dimostrazione complessa, e questo richiede tempo, competenza e, soprattutto, tanta pazienza.

Il primo agosto 2026, OpenAI alza ulteriormente la posta pubblicando un paper di 250 pagine che descrive dieci avanzamenti in matematica e informatica ottenuti con l’assistenza di un modello interno, non ancora pubblico. Il documento è scritto da esseri umani che raccontano il processo di ragionamento del modello, ma resta il fatto che si parla di un sistema proprietario, non verificabile da terzi in modo indipendente. Il tema della democratizzazione dell’accesso merita un approfondimento a parte.

Quando un’azienda rivendica un progresso matematico ottenuto con un modello interno non ancora disponibile al pubblico, si crea una situazione paradossale: la comunità scientifica non può replicare il risultato né verificarlo in modo indipendente. Questo crea un problema epistemologico prima ancora che etico: come si fa scienza quando lo strumento principale della scoperta è una scatola nera proprietaria?

È una domanda che riguarda anche altri campi, dalla biologia computazionale alla fisica delle particelle, ma che in matematica assume un peso particolare perché il valore della disciplina si fonda storicamente sulla verificabilità pubblica e condivisa delle dimostrazioni.

La Leiden Declaration: l’allarme di migliaia di matematici

Di fronte a questa accelerazione, la comunità matematica non è rimasta a guardare. Il 2 giugno 2026, sedici ricercatori provenienti da quindici università hanno pubblicato la Leiden Declaration on Artificial Intelligence and Mathematics, un documento nato da un workshop tenuto nel settembre 2025 al Lorentz Center dell’Università di Leiden.

La dichiarazione è stata sottoscritta da oltre 3.000 ricercatori ed esperti, tra cui nomi di primo piano come Terence Tao e il vincitore della Fields Medal Peter Scholze, ed è stata formalmente approvata dall’International Mathematical Union. Il documento individua cinque rischi principali legati all’uso dell’AI in matematica.

• Argomentazioni plausibili ma sbagliate: gli LLM possono produrre dimostrazioni che sembrano corrette ma non lo sono, indistinguibili a un primo sguardo da quelle valide. Il problema è che oggi produrre questi contenuti costa molto meno che verificarli, creando un vero e proprio collo di bottiglia per il sistema di peer review, con il rischio concreto di sommergere i ricercatori di contenuti da controllare.
• Attribuzione mancante: i modelli si appoggiano a letteratura matematica esistente senza necessariamente citarla nei risultati finali, e spesso sono addestrati su materiale protetto da copyright senza consenso.
• Incentivi distorti e dipendenza tecnologica: chi ha accesso a modelli proprietari avanzati ottiene un vantaggio competitivo, penalizzando i ricercatori senza quelle risorse e minando la democratizzazione della ricerca.
• Annunci via comunicato stampa: i risultati vengono spesso pubblicizzati attraverso blog e post sui social prima di qualsiasi valutazione da parte della comunità scientifica, seguendo logiche di marketing più che di rigore accademico.
• Perdita di autonomia della ricerca: c’è il rischio che i problemi scelti dai ricercatori vengano orientati verso ciò che è automatizzabile dagli LLM, abbandonando strade di ricerca più profonde ma meno immediate.

La Leiden Declaration non chiede di bandire l’intelligenza artificiale dalla matematica, ma di stabilire regole chiare: dichiarare sempre l’uso di strumenti AI nei paper, mantenere la responsabilità umana sulla correttezza dei risultati, continuare a pubblicare tramite peer review e non tramite comunicati stampa, e proteggere l’indipendenza della ricerca dalle grandi aziende tecnologiche.

Non tutti i problemi matematici sono uguali

Uno degli aspetti più interessanti, e sottovalutati nel dibattito pubblico, è che la matematica non è un blocco monolitico di difficoltà uniforme. Per capire davvero cosa stanno facendo gli LLM, è utile una tassonomia in quattro livelli.

Il primo livello è quello che potremmo chiamare sieving, o setacciatura: problemi molto ristretti, dove la risposta è già congetturata e gli strumenti per risolverla esistono già. Manca solo il lavoro lungo e meccanico di combinarli. Attaccare questi problemi chiude una domanda ma non ne apre altre, e non ha un impatto sistemico sulla matematica. Secondo diverse analisi, buona parte dei risultati recenti, con la possibile eccezione dell’ultimo lavoro di OpenAI ancora da valutare, ricade proprio in questa categoria.

Il secondo livello è il bridging, cioè costruire ponti tra aree diverse della matematica, riutilizzando strumenti sviluppati in un campo per risolvere problemi in un altro. Qui gli LLM mostrano capacità sorprendenti, complice la loro attitudine a maneggiare enormi quantità di dati e connessioni che sarebbero difficili da individuare per un singolo essere umano. Per rendere più concreta questa tassonomia, pensiamo a un esempio pratico. Immaginiamo un problema di teoria dei numeri per cui esiste già una tecnica dimostrativa nota, applicata con successo su varianti simili del problema in passato. Un LLM che riesce a individuare quale tecnica applicare, adattarla al caso specifico e verificarla con l’aiuto di un proof assistant come Lean, sta compiendo un lavoro di sieving: prezioso, ma incrementale. Diverso è il caso in cui lo stesso modello nota che una tecnica sviluppata per risolvere problemi di teoria dei grafi può essere trapiantata, con opportuni adattamenti, in un problema di combinatoria additiva che a prima vista non ha nulla a che fare con i grafi. Qui si parla di bridging, ed è un tipo di intuizione che richiede di avere una visione d’insieme su aree della matematica molto distanti tra loro, cosa in cui gli LLM, addestrati su enormi quantità di letteratura scientifica eterogenea, sembrano avere un vantaggio naturale rispetto a un singolo essere umano specializzato in un solo campo.

I livelli tre e quattro restano invece completamente fuori dalla portata attuale dei modelli. Il terzo riguarda l’invenzione di interi nuovi settori della matematica: costruire da zero la machinery necessaria e usarla per risolvere problemi via via più complessi, facendo crescere intere branche della disciplina.

Il quarto livello è forse il più affascinante: riguarda la capacità di formulare le domande giuste da porre a un modello.Questo tipo di creatività e intuizione resta, per ora, un’esclusiva umana. Vale la pena ricordare anche il concetto di intelligenza frattale: l’intelligenza artificiale non è uniformemente brava o scarsa, ma ha una struttura frastagliata che si ripete a ogni livello di zoom. È molto capace in certi sottoproblemi e scarsa in altri, e se ci si concentra sui sottoproblemi in cui eccelle, si ritrova la stessa struttura irregolare, anche a un livello più fine. È un’immagine che aiuta a spiegare perché gli LLM sembrino contemporaneamente geniali e limitati, spesso sullo stesso argomento.

Nella mia esperienza quotidiana con questi modelli, applicati a problemi di NLP o di ingegneria del software, riconosco benissimo questa irregolarità: lo stesso modello che risolve in un colpo un bug complesso di concorrenza può poi incastrarsi su un refactoring banale, semplicemente perché quel tipo specifico di pattern era sottorappresentato nei dati di addestramento.

Una riflessione finale: dove va l’umanità nella matematica

C’è infine un aspetto più filosofico che vale la pena toccare. Alcuni matematici hanno un rapporto pragmatico con questi strumenti: li usano per le parti più noiose o meccaniche del lavoro, mantenendo per sé il compito di generare idee e formulare le domande giuste. Altri, invece, esprimono un disagio più profondo, chiedendosi dove sia finita l’umanità nella matematica, un’obiezione che ricorda molto quella già sollevata da artisti e scrittori riguardo a immagini, video e testi generati dall’AI.È un parallelo che dice molto sul momento storico che stiamo vivendo: stiamo imparando, un settore alla volta, a convivere con sistemi che ragionano in modo diverso da noi, capaci di eccellere in compiti specifici pur restando privi della creatività necessaria per aprire nuove strade.

La matematica, dopo il software development, è solo uno dei campi a fare i conti con questa trasformazione, e probabilmente non sarà l’ultimo. Per chi si occupa di intelligenza artificiale e non solo di matematica pura, questa vicenda offre alcuni spunti trasferibili ad altri ambiti.

Primo: la combinazione tra un modello generativo e uno strumento di verifica formale, esterno e affidabile, sembra essere una ricetta vincente ogni volta che il dominio applicativo lo consente. Lo abbiamo visto con il codice, dove i test automatici fungono da verificatore, e lo stiamo vedendo ora con Lean in matematica.

Secondo: più un compito è facilmente verificabile in modo automatico, più velocemente un LLM riuscirà a padroneggiarlo, mentre i compiti che richiedono giudizio umano esperto per essere valutati resteranno indietro più a lungo, indipendentemente da quanto siano importanti.

Terzo, e forse più importante: la velocità con cui arrivano questi annunci supera sistematicamente la velocità con cui la comunità scientifica può valutarli con attenzione.

Questo squilibrio, se non affrontato con strumenti come la Leiden Declaration, rischia di normalizzare un modo di fare scienza guidato più dal marketing che dal metodo.

Se dovessi scommettere su dove guarderà questa storia in un paio d’anni, punterei sul fatto che il vero salto di qualità non arriverà da un modello linguistico più grande in senso assoluto, ma da un ecosistema di verificatori formali sempre più ricchi, uno per ogni dominio in cui riusciremo a codificare cosa significhi “corretto” in modo non ambiguo. È lo stesso motivo per cui, come sviluppatore, tendo a fidarmi di più di una pipeline CI/CD ben scritta che di un singolo modello per quanto sofisticato: la fiducia in questi sistemi non nascerà mai dalla loro bravura isolata, ma dalla qualità dell’infrastruttura di controllo che li circonda. Quello che emerge, mettendo insieme la storia tecnica e le preoccupazioni della comunità scientifica, è un quadro più sfumato di quanto i titoli sensazionalistici lascino intendere.

Gli LLM hanno fatto passi da gigante nel setacciare problemi noti e nel collegare aree diverse della matematica, ma restano lontani dall’inventare nuova matematica in senso profondo. La vera domanda, sollevata con forza dalla Leiden Declaration, non è tanto quanto sono bravi questi modelli, ma chi controlla, verifica e si assume la responsabilità di quello che producono, una questione che riguarda tutti, non solo chi fa ricerca matematica."

- Matteo