Una versione interna di Astra, il prossimo modello principale di OpenAI, ha prodotto dieci nuovi risultati su problemi aperti di matematica e informatica teorica. Gli argomenti matematici sono stati generati dal sistema, mentre i ricercatori di OpenAI hanno curato la preparazione delle prove con l’assistenza dello stesso modello. Astra ha poi formalizzato le dimostrazioni in Lean, rendendole verificabili meccanicamente.
Le questioni affrontate appartengono a discipline altamente specialistiche, dalla geometria in alte dimensioni alla complessità quantistica, dalla teoria dei gruppi alla crittografia basata sui reticoli. Alcuni problemi erano rimasti senza progressi sostanziali per decenni.
Per chi non lavora in questi campi, l’importanza dell’annuncio di OpenAI non risiede però nei dettagli delle singole dimostrazioni. Il punto è il passaggio dall’intelligenza artificiale che recupera e rielabora conoscenza esistente a un sistema capace di contribuire alla produzione di conoscenza nuova.
Dai problemi con soluzione nota alla ricerca originale
Negli ultimi anni i modelli di AI hanno raggiunto risultati elevati nelle competizioni matematiche e nei benchmark universitari. Queste prove misurano la capacità di risolvere esercizi difficili per i quali esiste già una risposta, spesso insieme a un vasto patrimonio di problemi analoghi utilizzabili durante l’addestramento.
La ricerca introduce un ostacolo differente: la soluzione non è conosciuta. Occorre individuare una direzione promettente, combinare strumenti provenienti da aree diverse, abbandonare i tentativi falliti e costruire un risultato che aggiunga qualcosa alla letteratura.
OpenAI attribuisce ad Astra proprio questo tipo di lavoro e ha pubblicato le dieci prove complete. I risultati includono nuovi limiti teorici, controesempi a congetture e soluzioni a questioni aperte da lungo tempo.
Tra questi compaiono il primo miglioramento generale dal 1978 per un problema di impacchettamento di sfere in alte dimensioni, la costruzione di un gruppo non sofico, la confutazione della congettura di rigidità di Connes e nuovi risultati sulla difficoltà computazionale di problemi collegati anche alla crittografia post-quantistica.
L’annuncio segue la confutazione di una congettura di Paul Erdős rimasta aperta per circa ottant’anni. In quel caso la soluzione generata da un modello di OpenAI era stata verificata da matematici indipendenti e accolta come un risultato significativo per la matematica assistita dall’AI. Con Astra cambia soprattutto la scala: dieci avanzamenti in discipline differenti, anziché una singola scoperta.
La verifica formale delle dimostrazioni con Lean
La formalizzazione delle dimostrazioni in Lean è centrale per valutare i risultati. Un modello linguistico può infatti produrre una prova apparentemente rigorosa anche quando contiene errori o passaggi mancanti.
Lean è un linguaggio di programmazione open source e un proof assistant, cioè un sistema progettato per scrivere e controllare dimostrazioni matematiche formali. In una prova tradizionale alcuni passaggi considerati evidenti possono essere lasciati impliciti. In Lean, definizioni, ipotesi e inferenze devono essere espresse con la precisione richiesta da un programma.
Il sistema confronta ogni passaggio con le regole della logica e con i risultati già formalizzati. Può inoltre utilizzare Mathlib, una libreria sviluppata dalla comunità che contiene oltre un milione di righe di matematica verificata, dall’algebra alla probabilità. Se un passaggio non deriva correttamente dalle premesse, Lean rifiuta la prova.
Il controllo finale è affidato a un componente relativamente piccolo chiamato kernel. Anche se gli strumenti automatici impiegati per costruire una dimostrazione commettessero un errore, non potrebbero costringere il kernel ad accettare un passaggio logicamente invalido.
I certificati delle dieci prove di Astra sono disponibili su GitHub. Altri ricercatori possono scaricarli, compilare il progetto e verificare che Lean accetti le dimostrazioni. Non devono quindi fidarsi soltanto della prosa prodotta dal modello o delle affermazioni di OpenAI.
La formalizzazione certifica la correttezza logica rispetto alle definizioni, alle ipotesi e agli enunciati codificati. Agli specialisti rimane il compito di controllare che questi rappresentino fedelmente i problemi originali e di valutare novità, importanza e conseguenze dei risultati.
Lean non stabilisce, per esempio, se una scoperta sia destinata a modificare un’intera disciplina o a rimanere un avanzamento più circoscritto. Questo giudizio dipende dal confronto con la letteratura e dal lavoro successivo della comunità matematica.
Il costo marginale della ricerca automatizzata
OpenAI stima che la quantità complessiva di token necessaria per trovare le dieci soluzioni costerebbe circa 2.000 dollari applicando le tariffe API di Sol. La cifra suggerisce che, una volta sviluppato il modello, il costo marginale per esplorare problemi scientifici possa diventare sorprendentemente basso.
Non è il costo complessivo di Astra. Non comprende l’addestramento, gli anni di ricerca e sviluppo, l’infrastruttura, il lavoro dei matematici e gli esperimenti svolti durante la costruzione del sistema.
L’aspetto rilevante è la possibilità di parallelizzare la ricerca. Un laboratorio potrebbe assegnare migliaia di problemi o ipotesi a istanze diverse dello stesso modello, scartare i percorsi falliti e sottoporre agli scienziati le soluzioni più promettenti.
In questa prospettiva l’AI non riduce soltanto il tempo necessario a svolgere un calcolo. Amplia il numero di direzioni che possono essere esplorate contemporaneamente e consente di combinare conoscenze provenienti da specializzazioni che raramente convivono nello stesso gruppo di ricerca.
Autonomia, selezione dei risultati e riproducibilità
La pubblicazione permette di esaminare i dieci risultati, ma non offre ancora tutti gli elementi necessari per misurare le capacità complessive di Astra. OpenAI non indica quanti problemi siano stati sottoposti al modello, quanti tentativi non abbiano prodotto risultati o quali criteri siano stati utilizzati per selezionare i dieci casi. Resta da precisare anche il grado di autonomia: l’azienda attribuisce al sistema la generazione degli argomenti matematici, ma non descrive nel dettaglio l’eventuale prompting iterativo, lo steering dei ricercatori o il numero di interazioni necessarie.
Tra gli studiosi che hanno invitato a valutare l’annuncio attraverso il metodo scientifico c’è Walter Quattrociocchi, professore ordinario di Informatica alla Sapienza Università di Roma, noto anche per avere introdotto il concetto di epistemia, l’illusione di conoscenza prodotta quando la plausibilità sostituisce la verifica. Quattrociocchi considera i risultati potenzialmente molto importanti, ma indica alcuni elementi necessari per misurare la capacità di Astra: il numero complessivo dei tentativi e il tasso di fallimento; la quantità di prompting, steering e intervento dei matematici; la possibilità di ripetere l’esperimento con lo stesso modello; i criteri utilizzati per selezionare i problemi; il diverso peso scientifico delle dieci prove. La formalizzazione permette di controllare i risultati finali, ma non ricostruisce il processo che li ha generati: ”La verifica in Lean certifica la correttezza della dimostrazione finale, ma non risponde automaticamente alla domanda su dove e come emerga la scoperta matematica”. Sono questioni che non ridimensionano l’annuncio, ma distinguono la validità delle prove dalla valutazione dell’autonomia e della generalità del sistema.
I limiti dei benchmark sul ragionamento
Il risultato di Astra si inserisce in un dibattito scientifico più ampio sulle capacità di ragionamento dei modelli linguistici. Le ricerche disponibili non restituiscono una contrapposizione semplice tra sistemi che ragionano e sistemi che si limitano a riprodurre correlazioni.
Nel 2025 i ricercatori di Apple hanno studiato i Large Reasoning Models in ambienti nei quali la complessità poteva essere controllata. The Illusion of Thinking ha rilevato buone prestazioni sui problemi intermedi e un rapido deterioramento oltre una certa soglia.
Il lavoro ha ricevuto repliche che ne hanno contestato parte dell’impostazione sperimentale. Rethinking the Illusion of Thinking ha confermato alcuni limiti, ma ha anche mostrato che una parte del collasso dipendeva dalla costruzione dei problemi. È un esempio di come risultati, critiche e nuovi test modifichino progressivamente la comprensione di questi sistemi.
Anche il benchmark SOCRATES, progettato per ridurre le scorciatoie statistiche nei test di ragionamento, ha rilevato capacità reali ma fortemente variabili secondo il tipo di relazione richiesta.
Astra mostra che un modello può generare nuova matematica all’interno di problemi già formulati. Rimane da capire fino a che punto questa capacità si estenda alla formulazione di nuove domande, all’introduzione di principi esplicativi e alla costruzione di teorie.
Il vaglio della comunità matematica
La comunità scientifica non ha ancora avuto il tempo di valutare complessivamente le dieci prove. L’annuncio risale al 1° agosto e ciascun risultato richiede competenze molto specifiche.
Le prime letture sono comunque avvenute durante la preparazione delle dimostrazioni. Per il lavoro sulla congettura di Connes, OpenAI cita i commenti di Sorin Popa, membro della National Academy of Sciences statunitense e tra le figure più autorevoli nello studio delle algebre di operatori, e la lettura di Cyril Houdayer, professore all’École normale supérieure e specialista di algebre di von Neumann e rigidità. La prova sui gruppi non sofici ha invece ricevuto osservazioni da ricercatori che lavorano sulla teoria dei gruppi e sulle loro approssimazioni finite. Sono controlli specialistici pertinenti, ma non equivalgono a una revisione indipendente dell’intera raccolta.
OpenAI ha pubblicato anche dieci ricostruzioni dei percorsi seguiti. Non sono trascrizioni integrali del ragionamento interno di Astra, ma narrazioni elaborate successivamente a partire dalle tracce originali e dalle prove finali. Aiutano a comprendere tentativi e cambi di direzione, senza consentire di riprodurre integralmente l’esperimento.
Saranno le verifiche, le estensioni e i lavori successivi a stabilire quali risultati cambieranno realmente il rispettivo campo. Questo processo può richiedere mesi o anni e non rappresenta un ridimensionamento, ma il normale funzionamento della ricerca scientifica.
Verso una nuova organizzazione della ricerca
Astra indica una nuova possibile divisione del lavoro. Un modello può esplorare rapidamente molte direzioni, combinare tecniche provenienti da una letteratura più vasta di quella assimilabile da un singolo individuo e produrre dimostrazioni formalmente controllabili.
Agli scienziati rimangono la formulazione delle domande, la valutazione della rilevanza, il controllo delle premesse, l’interpretazione dei risultati e la costruzione di nuove teorie.
Il salto non consiste nell’avere una macchina che ragiona esattamente come un essere umano. Consiste nell’avere un nuovo strumento per la ricerca teorica: scalabile, parallelizzabile e capace di produrre risultati originali, inserito in un processo nel quale verifica formale e giudizio della comunità restano indispensabili.
