In sintesi: AlphaProof Nexus di Google DeepMind ha risolto nove problemi matematici irrisolti da decenni, con dimostrazioni formalmente verificabili da macchina.
Mercoledì 21 maggio 2026, un preprint su arXiv ha documentato qualcosa che i matematici non si aspettavano di leggere così presto: un sistema di intelligenza artificiale ha risolto autonomamente nove problemi rimasti aperti per decenni, alcuni da 56 anni, dalla raccolta di quesiti lasciata in eredità dal matematico Paul Erdős. Le dimostrazioni sono formalmente verificate da una macchina, scaricabili da un repository GitHub pubblico, e controllabili da chiunque sappia leggere il linguaggio di prova Lean.
Il sistema si chiama AlphaProof Nexus, è sviluppato da Google DeepMind, e il paper porta la firma di Tsoukalas et al. Non è un benchmark interno. Non è una demo. È ricerca aperta, verificabile, ripetibile.
Nove problemi, cinquantasei anni di attesa
Paul Erdős è stato uno dei matematici più prolifici del Novecento. Ha lasciato centinaia di problemi aperti in combinatoria, teoria dei numeri e teoria dei grafi — molti con una ricompensa in denaro che lui stesso aveva promesso a chi li avesse risolti. Sono problemi semplici da enunciare e brutalmente difficili da dimostrare.
AlphaProof Nexus ne ha risolti nove su 353 tentati, circa il 2,5% del catalogo. Il numero sembra piccolo finché non si considera che due di questi erano rimasti senza risposta per 56 anni. Il sistema ha anche dimostrato 44 delle 492 congetture aperte dell’OEIS — l’Enciclopedia Online delle Successioni di Interi — pari a circa il 9% del totale. Ha risolto una questione aperta da 15 anni sulle funzioni di Hilbert in geometria algebrica, ha migliorato un limite noto nell’ottimizzazione convessa, e ha scoperto un parametro di ottimizzazione che, secondo il paper, non era mai stato identificato prima.
Il costo per problema: poche centinaia di dollari di inferenza computazionale.
Il verificatore che non si fida del modello
I modelli linguistici di grandi dimensioni hanno un problema noto: allucinano. Producono risposte che sembrano corrette ma non lo sono. In matematica questo è fatale: una dimostrazione con un solo passaggio logico sbagliato non vale nulla.
AlphaProof Nexus affronta il problema separando la generazione dalla verifica. Il modello linguistico propone passi dimostrativi scritti in Lean — un linguaggio formale dove ogni affermazione deve essere rigorosamente giustificata prima che il sistema la accetti. Se un passaggio non regge, viene scartato immediatamente. Il modello non può convincere il verificatore: o la logica è corretta o non lo è.
Sopra questo ciclo base, la versione completa del sistema — chiamata “Agent D” nel paper — aggiunge due strati. Il primo è una ricerca evolutiva: il sistema mantiene una popolazione di schemi dimostrativi parziali, classificati con un sistema di punteggio simile all’Elo usato negli scacchi, e li fa evolvere selezionando quelli più promettenti. Il secondo è AlphaProof, il modulo di apprendimento per rinforzo già sviluppato da DeepMind, che impara dai tentativi riusciti e falliti.
Vale la pena notare cosa non funziona: i modelli più piccoli testati nel paper — Gemini 3.0 Flash e Gemini 3.1 Flash-Lite — non hanno risolto nulla. La capacità del modello base conta, ma senza l’architettura agentiva attorno, anche Gemini 3.1 Pro da solo non basta. Secondo l’AI Index 2026, la frontiera dei modelli si sposta sempre più verso sistemi agentici multi-strato proprio per questo motivo.
La frecciata a OpenAI e la differenza che conta
La settimana prima della pubblicazione del paper, OpenAI aveva fatto notizia annunciando che la sua IA aveva risolto un problema matematico di 80 anni legato al catalogo di Erdős. Il matematico Tim Gowers, vincitore della Medaglia Fields, l’aveva definita una pietra miliare per la matematica AI.
Demis Hassabis, CEO di Google DeepMind, ha scelto di non essere diplomatico. In un’intervista ha definito “imbarazzante” la comunicazione di OpenAI, spiegando che il modello aveva trovato riferimenti a problemi già risolti in letteratura, senza costruire dimostrazioni nuove. L’agente di DeepMind, invece, produce dimostrazioni originali.
La differenza non è di grado: è di natura. Una dimostrazione formalmente verificata in Lean è inattaccabile per definizione. Una dimostrazione in linguaggio naturale, per quanto revisionata da esperti umani, può contenere errori sottili che emergono mesi dopo. Il paper di Tsoukalas et al. propone esplicitamente la verifica formale come filtro per decidere quali dimostrazioni meritino revisione umana — non il contrario.
C’è anche un’osservazione che il comunicato stampa non fa: i matematici che hanno lavorato con il sistema riferiscono che persino i tentativi falliti si sono rivelati utili. Gli schemi parziali prodotti — formalmente strutturati, con sotto-obiettivi espliciti — hanno permesso ai ricercatori di capire dove si trovava il vero ostacolo, senza dover riverificare ogni volta l’intero argomento da zero.
Da olimpiadi a ricerca aperta: il salto che cambia tutto
AlphaProof Nexus non nasce dal nulla. Il suo predecessore diretto, AlphaProof, aveva ottenuto prestazioni equivalenti a una medaglia d’argento all’International Mathematical Olympiad del 2024, risolvendo il problema più difficile della competizione — quello risolto completamente solo da 5 dei 609 partecipanti umani.
Ma i problemi olimpici sono progettati per essere risolvibili in poche ore da studenti di talento. I problemi di Erdős non hanno questa garanzia: alcuni sono rimasti aperti per decenni perché nessuno sapeva nemmeno da dove cominciare. Il salto da risolutore olimpionico a dimostratore di ricerca è il vero cambiamento di scala.
David Silver di Google DeepMind ha indicato perché la matematica è un terreno particolarmente fertile per questi sistemi: è completamente digitale, ogni affermazione è verificabile in modo automatico, e i cicli di miglioramento basati sull’esperienza funzionano senza ambiguità. Non serve un giudice umano per dire se una dimostrazione è corretta.
Dove arriva, e dove no
Il sistema è già in uso in ricerche attive su ottica quantistica e teoria dei grafi, secondo il paper. Le applicazioni più immediate riguardano la crittografia — dove la verifica formale di algoritmi è un problema aperto e costoso — e la verifica del software, dove dimostrare formalmente che un programma si comporta come previsto è oggi un processo lento e manuale.
Hassabis ha tenuto a precisare che nessuno di questi risultati avvicina l’IA alla cosiddetta AGI — l’intelligenza artificiale generale, cioè un sistema con capacità cognitive paragonabili a quelle umane in tutti i domini. Risolvere equazioni complesse non equivale a intelligenza originale e creativa: il sistema resta un potente assistente di ricerca, non un genio autonomo.
È una precisazione onesta. Nove problemi su 353 è il 2,5% di un catalogo specifico, in domini matematici precisi. I matematici non stanno per essere sostituiti da un proof engine. Ma il punto non è il numero grezzo di problemi risolti: è che esiste ora un’architettura capace di produrre ragionamento originale verificabile dalla macchina, in aree dove gli esseri umani erano bloccati da decenni.
La domanda che resta è quanto velocemente questo 2,5% possa diventare qualcosa di più grande — e se i problemi che restano aperti lo siano perché sono davvero troppo difficili, o perché nessuno aveva ancora lo strumento giusto.
Perché è importante
AlphaProof Nexus dimostra per la prima volta che un sistema AI può produrre dimostrazioni matematiche originali e formalmente inattaccabili su problemi di ricerca reale, non su benchmark costruiti ad hoc. La verifica automatica in Lean elimina il margine di errore umano e apre una nuova categoria di strumenti per crittografia, verifica del software e matematica pura. Il modello non sostituisce i matematici, ma abbatte il costo di esplorazione in territori dove prima era impossibile anche solo orientarsi.
