Il 1º agosto 2026 OpenAI ha annunciato che un suo modello interno, chiamato Astra, ha risolto dieci problemi rimasti aperti per anni in matematica e informatica teorica, pubblicando per ciascuno una dimostrazione formale verificabile al computer. Non un comunicato di marketing: sul repository GitHub dell'azienda ci sono i file di prova in Lean 4, i "ragionamenti" del modello passo per passo e un manoscritto di 249 pagine datato agosto 2026.
Cosa ha dimostrato Astra, in concreto
I dieci problemi erano tutti aperti da almeno un decennio. Secondo OpenAI, il modello ha prodotto le soluzioni in autonomia e il costo in token per trovarle tutte è stato stimato attorno ai 2.000 dollari alle tariffe delle sue API. Due risultati spiccano su tutti. Il primo smentirebbe la congettura di rigidità di Connes: Astra costruisce infiniti gruppi con proprietà (T), tra loro non isomorfi, che condividono la stessa algebra di von Neumann di gruppo — il che, se confermato, dimostra che la congettura è falsa. Il secondo stabilirebbe l'esistenza di un gruppo non sofico, una questione che resisteva da 27 anni, dall'introduzione del concetto nel 1999.
Perché le prove in Lean 4 cambiano le regole
Quando un'IA "dimostra" un teorema in linguaggio naturale, resta il dubbio: sta ragionando o sta imitando in modo convincente? Lean 4 elimina quel dubbio. È un assistente di dimostrazione: verifica meccanicamente, riga per riga, che ogni passaggio segua dagli assiomi. Un certificato Lean che compila senza errori garantisce che l'enunciato formalizzato è vero. Resta un compito per la comunità matematica: controllare che la formalizzazione corrisponda davvero alla congettura che si intendeva affrontare. Ma è una verifica diversa, e molto più rapida, rispetto al leggere pagine di prova a mano.
OpenAI assume i matematici: il caso Tsimerman
L'annuncio non arriva isolato. Pochi giorni prima, il 31 luglio, si è saputo che Jacob Tsimerman, vincitore della Medaglia Fields 2026 e noto per aver dimostrato la congettura di André-Oort, lascia l'Università di Toronto per unirsi a OpenAI e lavorare sulla sicurezza dei modelli. È il segnale di una strategia: l'azienda sta reclutando matematici di primissimo piano, convinta che i modelli in grado di produrre matematica verificabile siano anche una via per capire e controllare meglio i sistemi più potenti.
Cosa non dimostra ancora questo risultato
Va tenuta la testa fredda. I risultati sono "proposti": andranno digeriti dagli specialisti, che dovranno accertare che gli enunciati Lean coincidano con le congetture nella loro forma consueta e valutare se le costruzioni siano davvero nuove. Non significa che l'IA "faccia matematica" come un ricercatore umano: Astra ha lavorato su problemi ben definiti e formalizzabili, non ha scelto le domande né ha costruito una teoria. Ma la combinazione tra modelli sempre più capaci e verifica automatica sposta un confine. Se anche solo alcune di queste dimostrazioni reggeranno al vaglio, l'IA passerà da strumento che suggerisce idee a strumento che produce conoscenza matematica certificata.
La vicenda si inserisce in una corsa più ampia tra i laboratori a usare l'IA per la ricerca scientifica di frontiera, dopo i risultati mostrati nei mesi scorsi anche in crittografia e biologia. La differenza, stavolta, è che le prove sono lì, aperte, pronte da controllare.
