OpenAI ha utilizzato una versione interna di Astra, la prossima famiglia principale di modelli dell’azienda, per ottenere nuovi risultati su dieci problemi aperti di matematica e informatica teorica. I problemi affrontati appartengono ad ambiti differenti, tra cui geometria ad alta dimensionalità, teoria dei codici, complessità dei circuiti aritmetici, teoria dei gruppi, algebre di operatori, complessità quantistica, crittografia basata sui reticoli e combinatoria estremale. In tutti i casi selezionati non erano stati registrati progressi sostanziali sul risultato principale da almeno dieci anni e, per diversi problemi, la situazione di stallo durava da molto più tempo.
Astra non è stato ancora distribuito come prodotto pubblico. OpenAI lo ha descritto per la prima volta come la propria prossima grande famiglia di modelli, senza indicare una data di lancio. La versione impiegata per la ricerca ha generato gli argomenti matematici alla base delle soluzioni, mentre i ricercatori hanno utilizzato lo stesso modello per trasformare tali argomenti in manoscritti scientifici. In una fase successiva, Astra ha riscritto ogni dimostrazione nel sistema formale Lean, producendo certificati verificabili meccanicamente.
Il processo ha quindi combinato tre livelli distinti. Il modello ha innanzitutto individuato le idee matematiche e costruito i nuovi argomenti. I ricercatori hanno poi organizzato i risultati nella forma richiesta da una pubblicazione accademica, verificando i passaggi e lavorando alla presentazione dei contenuti. Infine, le dimostrazioni sono state formalizzate in Lean, in modo da sottoporle a un controllo automatico della coerenza logica. OpenAI ha pubblicato anche una ricostruzione del percorso seguito dal modello per ciascun risultato. Il primo avanzamento riguarda il problema dell’impacchettamento di sfere in dimensioni elevate. L’obiettivo consiste nello stabilire con quale densità sia possibile collocare sfere identiche in uno spazio senza sovrapporle. Astra ha prodotto nuovi limiti superiori per la densità dell’impacchettamento, avvicinandoli alla soglia di Cohn-Elkies, uno dei riferimenti principali per lo studio matematico del problema. Il secondo risultato interessa i codici binari e sferici. I codici binari sono insiemi di sequenze formate da zero e uno progettati per mantenere una distanza minima tra le diverse parole di codice, mentre quelli sferici distribuiscono punti sulla superficie di una sfera ad alta dimensionalità. Il modello ha ricavato limiti superiori esponenzialmente migliori per il numero massimo di codici binari che possono rispettare una distanza minima prefissata, estendendo il metodo anche ai codici sferici in dimensioni elevate.
Un terzo risultato riguarda l’esistenza dei gruppi non sofic. I gruppi sofic possono essere approssimati attraverso strutture finite e costituiscono una classe molto ampia nella teoria dei gruppi. Per lungo tempo non era stato possibile stabilire se esistessero gruppi esterni a questa classe. Astra ha costruito un esempio che dimostra l’esistenza di gruppi non sofic, fornendo una risposta a una questione centrale rimasta aperta nel settore. Il modello ha inoltre prodotto un controesempio alla congettura di rigidità di Connes. La congettura sosteneva, in una particolare formulazione, che determinati gruppi potessero essere identificati in modo univoco attraverso le rispettive algebre di von Neumann. La dimostrazione generata da Astra mostra invece che questa corrispondenza non vale in tutti i casi, invalidando la congettura nella sua forma generale. Nel campo della complessità dei circuiti aritmetici, Astra ha ricavato nuovi limiti inferiori per il calcolo del permanente di una matrice. Il permanente è una funzione simile al determinante, ma priva dell’alternanza dei segni, ed è considerato molto più difficile da calcolare. I nuovi risultati stabiliscono limiti sulla dimensione minima dei circuiti e delle formule aritmetiche necessari per eseguire questo calcolo, includendo un limite inferiore dell’ordine di n elevato alla quarta diviso il logaritmo di n per le formule aritmetiche.
Un altro avanzamento riguarda la ripetizione parallela nei giochi quantistici. Nella teoria della complessità, i teoremi di ripetizione parallela descrivono come diminuisca la probabilità di successo quando uno stesso gioco viene eseguito più volte contemporaneamente. Astra ha formulato un teorema di ripetizione parallela esponenziale valido per giochi quantistici generali con due partecipanti, estendendo al contesto quantistico un principio già centrale nella teoria classica della complessità. Il settimo risultato riguarda il problema del vettore più vicino, noto come Closest Vector Problem o CVP. Dato un reticolo e un punto esterno, il problema richiede di individuare il punto del reticolo più vicino. La sua difficoltà computazionale è alla base di diversi sistemi di crittografia post-quantistica. Astra ha dimostrato la difficoltà dell’approssimazione del CVP entro fattori polinomiali, rafforzando la comprensione teorica della sicurezza dei problemi basati sui reticoli.
Il modello ha inoltre risolto la congettura sul volume di Ehrhart. Il problema consiste nel determinare, in ogni dimensione, il massimo volume possibile di un corpo convesso il cui baricentro rappresenti l’unico punto del reticolo presente al suo interno. Il risultato definisce il valore estremo consentito e completa una questione che collega geometria convessa e teoria discreta dei reticoli. Nel campo della teoria di Ramsey, Astra ha ottenuto un nuovo limite inferiore superesponenziale per i numeri di Ramsey triangolari multicolore. Questi numeri indicano la dimensione minima che una struttura deve raggiungere affinché, colorandone gli elementi con un determinato numero di colori, compaia inevitabilmente una configurazione monocromatica. Il nuovo limite risolve il problema numero 183 dell’elenco di Paul Erdős. L’ultimo gruppo di risultati interessa la teoria estremale dei grafi. Astra ha risolto due congetture relative alla compattezza e alla degenerazione, corrispondenti ai problemi 146 e 180 di Erdős. La teoria estremale studia quante connessioni possa contenere un grafo senza che compaiano determinate sottostrutture proibite. Le nuove dimostrazioni chiariscono le condizioni alle quali specifiche proprietà locali e globali dei grafi possono essere garantite.
OpenAI ha stimato che il numero complessivo di token necessario per individuare le dieci soluzioni corrisponderebbe a un costo di circa 2.000 dollari applicando le tariffe API di GPT-5.6 Sol. L’importo riguarda la fase di ricerca delle soluzioni e non rappresenta necessariamente il costo totale dell’intero progetto, che ha incluso il lavoro dei ricercatori, la preparazione dei manoscritti, la verifica delle dimostrazioni e la formalizzazione in Lean. Il dato viene utilizzato per mostrare la quantità relativamente contenuta di calcolo necessaria per ottenere i risultati. Noam Brown, responsabile delle attività di ricerca avanzata di OpenAI, ha precisato che su ciascun problema non sono state impiegate quantità particolarmente elevate di calcolo durante l’inferenza. Ciò lascia aperta la possibilità di aumentare ulteriormente il test-time compute, permettendo ai futuri modelli di esplorare più ipotesi, mantenere attivi più percorsi di ragionamento e dedicare tempi maggiori alla verifica delle soluzioni. Le capacità attribuite ad Astra comprendono anche un sistema di collaborazione tra più agenti. In questa configurazione, differenti istanze del modello lavorano sullo stesso problema per periodi prolungati, suddividendo il progetto in attività più piccole, proponendo alternative, criticando i risultati prodotti dagli altri agenti e correggendo progressivamente gli errori. L’approccio è destinato alle attività che non possono essere completate con una singola risposta, come la ricerca scientifica, la matematica avanzata e i progetti tecnici articolati.
Sam Altman avrebbe mostrato privatamente alcune di queste funzioni durante incontri con responsabili politici e rappresentanti delle autorità di regolamentazione a Washington. Le dimostrazioni si sarebbero concentrate sulla capacità di gruppi di agenti di collaborare a lungo su problemi complessi. OpenAI non ha tuttavia comunicato se la versione commerciale di Astra comprenderà fin dal lancio la stessa architettura utilizzata negli esperimenti matematici. L’azienda ha specificato che gli argomenti matematici sono stati generati dal sistema e non dai ricercatori umani. Il contributo umano ha riguardato la preparazione dei manoscritti, il controllo dei risultati, il supporto alla formalizzazione e l’assunzione di responsabilità sulla correttezza delle pubblicazioni. OpenAI ritiene pertanto improprio attribuire esclusivamente agli autori umani dimostrazioni concepite interamente dal modello, poiché una simile presentazione non descriverebbe correttamente il processo con cui sono stati ottenuti i risultati.
La pubblicazione delle dimostrazioni formalizzate non elimina la necessità della verifica accademica indipendente. Lean può controllare che una dimostrazione segua correttamente le regole logiche e gli assiomi formalizzati nel sistema, ma la comunità scientifica deve comunque valutare l’importanza dei risultati, la correttezza della loro interpretazione, la validità delle formalizzazioni iniziali e le eventuali conseguenze per le discipline coinvolte. Il matematico Thomas Bloom dell’Università di Manchester ha definito i risultati particolarmente rilevanti, indicando il nuovo limite sui numeri di Ramsey multicolore come uno degli avanzamenti più significativi. Altri ricercatori hanno mantenuto una posizione più prudente, osservando che tutte le dimostrazioni devono essere esaminate in modo indipendente e attraversare i normali processi di revisione scientifica prima di essere considerate definitivamente acquisite. Noam Brown ha inoltre chiarito che Astra non ha risolto uno dei sette problemi del Millennio. I dieci risultati riguardano comunque questioni aperte considerate importanti nei rispettivi campi e rimaste prive di miglioramenti decisivi per almeno un decennio. La distinzione serve a evitare che il valore scientifico del lavoro venga confuso con la soluzione dei problemi matematici più noti al pubblico.
Prima di questi risultati, OpenAI aveva già comunicato la confutazione generata dall’intelligenza artificiale della congettura delle distanze unitarie di Erdős. Anche quel risultato era emerso durante la valutazione di un modello non ancora distribuito e aveva successivamente stimolato ulteriori lavori nel campo della matematica e dell’informatica teorica. La serie di dieci problemi amplia quindi una linea di ricerca nella quale i modelli vengono valutati non soltanto attraverso benchmark con risposte note, ma anche tramite problemi scientifici aperti. L’impiego di Lean costituisce una parte centrale della procedura. Una dimostrazione matematica tradizionale è scritta per essere letta e interpretata da altri ricercatori e può contenere passaggi lasciati impliciti. Una dimostrazione formale deve invece rappresentare ogni passaggio in un linguaggio controllato, specificando definizioni, ipotesi e regole di inferenza. Il verificatore controlla automaticamente che la conclusione discenda dalle premesse senza salti logici non giustificati. La formalizzazione può quindi ridurre il rischio che un risultato prodotto dall’intelligenza artificiale contenga errori nascosti dietro una spiegazione linguisticamente convincente. Non garantisce però automaticamente che il teorema formalizzato corrisponda esattamente alla domanda matematica originaria. Per questo motivo, la verifica meccanica deve essere affiancata dal controllo degli esperti, che devono assicurarsi che le definizioni inserite nel sistema rappresentino correttamente il problema studiato.
OpenAI ha collegato il progetto alla propria iniziativa per offrire gratuitamente i modelli più avanzati di ChatGPT a 100.000 scienziati e matematici. L’obiettivo dichiarato è rendere più ampio l’accesso agli strumenti di ricerca assistita, evitando che capacità di questo tipo rimangano disponibili soltanto alle organizzazioni dotate delle maggiori risorse informatiche ed economiche. La società ha riconosciuto anche le questioni aperte relative all’impatto dell’intelligenza artificiale sulla matematica, sull’attribuzione dei risultati e sul ruolo degli autori umani. La capacità di produrre nuove dimostrazioni rende necessario stabilire modalità trasparenti per indicare il contributo dei modelli, distinguere la generazione delle idee dal lavoro di verifica e assegnare la responsabilità scientifica delle pubblicazioni.
Astra viene quindi presentato come un modello orientato non soltanto alla risposta immediata, ma al lavoro prolungato su problemi che richiedono esplorazione, collaborazione tra agenti, uso di strumenti formali e successive revisioni. La data di disponibilità non è stata annunciata e non è stato specificato quali funzioni della versione interna saranno incluse nel prodotto finale. I dieci risultati matematici rappresentano per ora una dimostrazione delle capacità raggiunte durante lo sviluppo e restano sottoposti all’esame della comunità scientifica.