Google Deepmind ha messo a punto AlphaProof Nexus, un framework che ha risolto autonomamente nove dei 353 problemi aperti di Erdős che ha tentato. Due di questi erano rimasti senza risposta per 56 anni. Il costo? Poche centinaia di dollari a problema.
Non è magia. È un sistema che combina la generazione di prove guidata da LLM con la verifica automatica. Il modello linguistico — in questo caso Gemini 3.1 Pro — genera passi di dimostrazione in Lean, un linguaggio di programmazione formale usato per la verifica matematica. Ogni passo viene controllato dal compilatore, e se qualcosa non torna, i messaggi di errore alimentano il tentativo successivo. Tradotto: il modello non deve portare avanti da solo tutta la catena logica, ha una rete di sicurezza simbolica che compensa le ben note debolezze dei LLM quando si tratta di ragionamento.
Quattro agenti, un risultato sorprendente
Il sistema si articola in quattro varianti di agente, con complessità crescente. Il più semplice, Agent (A), fa girare sotto-agenti indipendenti basati su Gemini 3.1 Pro in ciclo: il modello genera passi, il compilatore Lean li verifica, gli errori tornano indietro per il prossimo tentativo.
Agent (B) aggiunge query ad AlphaProof, il sistema di Google basato su reinforcement learning per la matematica olimpica, che può riempire segmenti mancanti nelle dimostrazioni. Agent (C) introduce una componente evolutiva: i sotto-agenti condividono una popolazione comune di schizzi di prova, valutati per plausibilità e novità da agenti di rating costruiti su Gemini 3.0 Flash, poi classificati con un sistema Elo. Agent (D), quello completo, combina tutte queste capacità.
Per i problemi di Erdős è stato usato Agent (D). Ma — sorpresa — un’analisi post-hoc ha rivelato che anche il più semplice Agent (A), quello che usa solo LLM e feedback del compilatore, poteva risolvere tutti e nove i problemi di Erdős risolti. Costava di più sui più difficili, questo sì, ma ci arrivava.
I ricercatori attribuiscono questo successo a due fattori: il rapido miglioramento dei modelli linguistici di base e ‘il potere del feedback del compilatore nel radicare il ragionamento del LLM’. L’agente completo ha ancora un vantaggio sui task più tosti, per ora. Ma quel vantaggio potrebbe ridursi man mano che i LLM migliorano. I ricercatori parlano di ‘uno spostamento in corso da sistemi addestrati specializzati verso semplici cicli agentici, man mano che i LLM diventano più capaci’.
Utile anche senza una prova completa
I successi del sistema si concentrano in aree come combinatoria, ottimizzazione convessa e teoria dei numeri, dove la libreria matematica di Lean — Mathlib — è matura e i problemi si scompongono in sotto-obiettivi gestibili. La maggior parte dei problemi di Erdős è rimasta fuori portata, ‘per non parlare dei problemi che richiedono nuova teoria estesa’, scrivono i ricercatori. Gli agenti ereditano anche l’inaffidabilità dei modelli linguistici sottostanti.
Eppure vedono valore anche oltre i problemi risolti. I matematici che hanno lavorato con il sistema hanno riferito che persino i tentativi di prova falliti hanno approfondito la loro comprensione di un problema. Come scrivono gli autori: ‘la ricerca formale di prove guidata dall’IA può servire non solo a risolvere problemi ma ad approfondire la comprensione umana’.
Siccome gli schizzi erano formali, gli esperti potevano concentrarsi sui sotto-obiettivi non risolti invece di ricontrollare l’intero argomento da zero. Gli agenti si sono anche dimostrati efficaci nel catturare formalizzazioni errate nella letteratura. ‘La verifica formale può servire da filtro per determinare quali prove meritano revisione umana’, scrivono.
Il sistema è già utilizzato in ricerche in corso su ottica quantistica e teoria dei grafi, secondo il paper. Tutte le prove Lean e alcune prove in linguaggio naturale sono disponibili su GitHub.
I problemi di Erdős diventano il benchmark per l’IA matematica
OpenAI ha recentemente usato un modello di ragionamento proprietario per confutare la congettura della distanza unitaria di Erdős. Il medaglista Fields Tim Gowers l’ha definita ‘una pietra miliare nella matematica IA’. Prima di allora, GPT-5.2 Pro aveva aiutato a risolvere il problema di Erdős #281, con Terence Tao che ha definito il caso ‘forse l’istanza più inequivocabile’ di un LLM che risolve un problema matematico aperto. Successivamente, GPT-5.4 ha risolto un altro problema di Erdős.
In un certo senso, quei risultati sono più impressionanti dell’approccio di Deepmind. Il modello linguistico doveva portare avanti l’intera catena logica attraverso il linguaggio naturale, senza un compilatore Lean che controllasse ogni passo. AlphaProof Nexus è più sistematico e scalabile, ma sta affrontando un obiettivo diverso: costruire uno strumento IA affidabile per la ricerca matematica quotidiana. OpenAI potrebbe integrare Lean nel proprio scaffold, certo, ma il punto lì è più testare la capacità grezza del LLM.
Tao in passato ha messo in guardia dal leggere troppo nei titoli. Il tasso di successo effettivo dell’IA sui problemi di Erdős si attesta solo all’uno-due percento, concentrato sui compiti più facili. Il sistema di Google ha risolto solo nove problemi su 353. Si allinea quasi esattamente con la soglia del due percento di Tao.
Diciamo che i titoli pompano, i numeri ridimensionano. Ma anche il due percento, se costa poche centinaia di dollari e gira su hardware normale, non è male come punto di partenza.
