AlphaProof Nexus di Google DeepMind risolve 53 problemi matematici aperti

Se usi ChatGPT per ragionare su un problema e poi ti chiedi se la risposta sia davvero giusta, la nuova ricerca di Google DeepMind ti riguarda da vicino: mostra come un’intelligenza artificiale possa non solo proporre una soluzione, ma sottoporla a un controllo rigoroso. In matematica la differenza è decisiva. Un ragionamento convincente non basta: ogni passaggio deve reggere.

AlphaProof Nexus ha prodotto dimostrazioni per nove problemi attribuiti al matematico Paul Erdős e per 44 congetture dell’On-Line Encyclopedia of Integer Sequences (OEIS), un archivio di successioni numeriche. Due dei problemi di Erdős erano aperti da 56 anni. I risultati sono descritti in uno studio pubblicato su Science l’8 ottobre 2026, dopo la revisione da parte di altri esperti, detta peer review.

La notizia arriva mentre si discute di come rendere pubbliche le scoperte matematiche ottenute con l’AI. La questione non è soltanto quante dimostrazioni una macchina riesca a scrivere. È anche chi le controlla, chi se ne assume la responsabilità e come altri ricercatori possono comprenderle.

I problemi di Erdős prendono il nome da Paul Erdős, matematico noto per aver formulato numerose domande ancora oggetto di ricerca. Una congettura è un’affermazione che sembra vera, ma per la quale manca una dimostrazione generale: osservare che funziona in mille esempi non significa aver provato che funzionerà sempre.

Secondo lo studio dei ricercatori, la versione più completa di AlphaProof Nexus ha risolto nove dei 353 problemi di Erdős sottoposti al sistema. Ha inoltre dimostrato 44 delle 492 congetture OEIS considerate nell’esperimento. Nello stesso lavoro gli autori descrivono progressi in geometria algebrica, ottimizzazione e su un problema tratto da una raccolta del matematico Ben Green: non sono però risultati da sommare indistintamente ai due gruppi principali.

Il denominatore conta quanto il numeratore. I 353 problemi di Erdős erano quelli disponibili in una raccolta di enunciati formalizzati, cioè già tradotti in una forma leggibile dal software. Per OEIS, invece, i ricercatori sono partiti da 2.649 congetture aperte e ne hanno fatte selezionare 500 a Gemini anche in base alla loro idoneità alla dimostrazione automatica; otto sono state poi escluse per incompatibilità tecniche. Il risultato di 44 su 492 non va quindi interpretato come la probabilità che l’AI risolva una qualsiasi congettura matematica.

Al centro del progetto c’è Gemini 3.1 Pro, usato come Large Language Model (LLM), cioè un modello linguistico capace di generare e rielaborare testo e codice. In questo caso non scrive soltanto spiegazioni in italiano o inglese: prepara bozze di dimostrazione in Lean, un linguaggio con cui gli argomenti matematici possono essere espressi in forma controllabile da un computer.

Il ciclo di lavoro somiglia a quello di chi corregge un programma: l’AI propone un passaggio, Lean lo esamina e restituisce eventuali errori; il sistema usa quelle indicazioni per riprovare. La configurazione più elaborata fa lavorare più agenti — componenti che portano avanti tentativi distinti — e può affidare sottoproblemi ad AlphaProof, uno strumento specializzato. Conserva e confronta anche bozze promettenti, invece di ripartire sempre da zero.

C’è un risultato meno vistoso dei 53 problemi, ma importante per capire la tecnologia: nello studio, anche una versione più semplice, basata sull’alternanza tra tentativi del modello e controlli di Lean, è riuscita a riprodurre le nove soluzioni ai problemi di Erdős. Per i casi più difficili ha però richiesto una spesa di calcolo maggiore. Questo suggerisce che il controllo continuo e la capacità del modello contino almeno quanto la complessità dell’architettura; non significa che ogni problema sia facile da risolvere con un sistema minimale.

Se Lean accetta una dimostrazione, verifica che i passaggi seguano logicamente dalle premesse formulate nel programma. Resta però una domanda precedente: le premesse e l’enunciato inseriti nel software corrispondono davvero al problema che volevamo risolvere? Un controllore impeccabile può certificare la soluzione di una domanda diversa da quella che il ricercatore aveva in mente. È il motivo per cui la traduzione del problema in linguaggio formale merita un esame umano.

C’è poi la distanza tra validità e comprensione. Una dimostrazione può essere corretta ma difficile da spiegare, oppure offrire poche intuizioni utili ad affrontare altre domande. Il gruppo consultivo su matematica e intelligenza artificiale dell’Institute for Advanced Study insiste proprio su questo punto: gli autori devono capire gli argomenti che pubblicano, verificarli e assumersene la responsabilità.

Google DeepMind ha reso disponibili in un archivio pubblico le dimostrazioni in Lean e una selezione di spiegazioni in linguaggio naturale. Lo studio era già apparso come preprint, cioè una versione diffusa prima della pubblicazione su rivista, nel maggio 2026. Il passaggio successivo su Science non cancella la necessità di esame da parte della comunità, ma aggiunge un livello di valutazione editoriale a materiale che può essere ispezionato.

Il 6 ottobre 2026 OpenAI ha annunciato la pubblicazione su GitHub di un ampio insieme di risultati matematici prodotti da un proprio modello interno. L’azienda afferma di aver condiviso anche dimostrazioni formalizzate in Lean per molti risultati e informazioni sul processo seguito. Un archivio pubblico rende possibile l’analisi da parte di altri, ma caricare un manoscritto su GitHub non equivale a farlo revisionare da una rivista. È una distinzione di percorso editoriale, non una prova automatica che un’azienda abbia ragione e l’altra torto sui contenuti matematici.

Il 7 ottobre l’Association for Human Mathematics ha criticato la pubblicazione simultanea di oltre 700 documenti e ha invitato i matematici a interrompere le collaborazioni con OpenAI. La dichiarazione è stata ospitata come contributo dell’associazione sul blog di Terence Tao: attribuirla personalmente a Tao sarebbe impreciso. La preoccupazione espressa dal gruppo è che una quantità così grande di lavori trasferisca sulla comunità il compito di controllarli e comprenderli.

OpenAI, da parte sua, scrive di aver consultato un gruppo consultivo indipendente, di voler migliorare citazioni e chiarezza dei lavori e di prevedere iniziative a sostegno della loro comprensione. Quel gruppo consultivo, nelle proprie raccomandazioni del 29 settembre, chiede però anche alle aziende di smettere di testare problemi matematici avanzati su modelli proprietari non accessibili alla comunità. La discussione, dunque, va oltre il confronto fra due piattaforme di pubblicazione: riguarda le regole con cui l’AI entra nella ricerca.

La prima cautela riguarda la difficoltà. «Problema aperto» significa che mancava una soluzione riconosciuta, non che tutti i problemi aperti siano ugualmente importanti o ardui. Il fatto che due domande siano rimaste senza risposta per 56 anni è notevole, ma da solo non misura la portata teorica di ciascuna dimostrazione. Anche per questo è utile che specialisti del settore possano leggerle, confrontarle con lavori precedenti e discuterne le idee.

La seconda cautela riguarda i costi. Gli autori stimano alcune centinaia di dollari di calcolo per problema risolto nel gruppo Erdős. Specificano però che quel valore non comprende l’intero investimento necessario a esplorare tutti i 353 candidati e individuare quelli trattabili. Non è quindi il prezzo complessivo di una scoperta matematica, né un confronto sensato con il lavoro di un ricercatore umano.

Infine, AlphaProof Nexus è un sistema costruito per un ambiente di ricerca preciso: riceve problemi già espressi in una forma su cui i suoi strumenti possono lavorare. Non bisogna confondere questa capacità con quella di un chatbot generico a cui si chiede, in una normale conversazione, di risolvere qualsiasi grande enigma della matematica. La lezione più concreta è più circoscritta e più interessante: un modello che propone idee, affiancato da strumenti che le controllano, può contribuire alla ricerca reale.

Notizie simili diventeranno probabilmente più frequenti. Per distinguere un risultato promettente da un annuncio prematuro, non serve saper leggere una dimostrazione in Lean: basta chiedersi quale sia il problema originale, che cosa sia stato effettivamente controllato e quale percorso pubblico abbia seguito il lavoro. Sono domande simili a quelle che faremmo davanti a una nuova scoperta medica: il comunicato è soltanto l’inizio della verifica.

AlphaProof Nexus segna un risultato concreto: ha affrontato problemi di ricerca aperti, ha prodotto prove controllabili dal computer e ha portato il proprio metodo davanti ai revisori di una rivista scientifica. Non dimostra che la matematica possa fare a meno dei matematici. Mostra, piuttosto, quanto possa diventare potente un processo in cui l’AI cerca nuove strade, gli strumenti formali ne controllano la logica e le persone continuano a decidere che cosa è stato davvero scoperto e perché conta.