OpenAI ha pubblicato 722 manoscritti matematici prodotti da un modello interno non ancora rilasciato, descrivendo il lavoro come il risultato di un processo basato in gran parte su un singolo prompt assegnato a un singolo agente. Gli articoli sono organizzati in 372 famiglie di risultati correlati, ma i matematici affermano che le affermazioni non potranno essere valutate pienamente finché il modello, i prompt e ulteriori prove non saranno resi disponibili.

Il rilascio arriva mentre i laboratori di IA utilizzano sempre più la matematica come campo di prova per il ragionamento dei modelli all'avanguardia, e si configura come un primo test su come la ricerca generata dall'IA dovrebbe essere pubblicata, verificata e divulgata.

Un portavoce diAI ha dichiarato che quasi tutto proveniva da un singolo prompt assegnato a un singolo agente IA, sebbene alcuni risultati abbiano potuto richiedere più tentativi. L'azienda ha affermato di aver presentato al modello circa 4.000 problemi e di aver selezionato gli output ritenuti abbastanza significativi da pubblicare.

Andrew Sutherland, matematico del MIT, ha dichiarato a Scientific American che l'affermazione sul one-shot andrebbe trattata con cautela. "Finché non rilasceranno il modello e la gente non potrà replicare i loro risultati, penso che qualsiasi affermazione sulla risoluzione one-shot di problemi con un singolo agente andrebbe trattata come non verificata", ha detto Sutherland. "Dovremmo chiedere le prove."

La cifra di 722 rappresenta manoscritti e non problemi risolti. Una famiglia di risultati può contenere un teorema principale insieme ad argomenti accessori, conseguenze o dimostrazioni alternative. OpenAI ha dichiarato che il risultato medio ha utilizzato l'equivalente di circa tre ore di calcolo di thinking di ChatGPT Pro. Questo differisce dalla rivendicazione sulla Navier-Stokes del mese scorso, che ha coinvolto 10.000 agenti coordinati al lavoro per 88 ore.

OpenAI ha rilasciato sintesi di ragionamento abbreviate per 10 risultati. Tuttavia, un catalogo di formalizzazione nel repository GitHub mostra che solo 162 dei 722 manoscritti includono attualmente un risultato principale verificato da computer. Ciò equivale a circa il 22% della collezione e significa che il risultato è stato tradotto in Lean, un software che verifica meccanicamente ogni passaggio logico. Lean è diventato lo standard operativo per le dimostrazioni verificate da macchina in matematica, ed è per questo che i circa 560 manoscritti non ancora formalizzati rappresentano la principale questione aperta della collezione.

OpenAI ha dichiarato che non tutti i manoscritti hanno formalizzazioni Lean e ha avvertito che "uni dei risultati non formalizzati potrebbero avere problemi". Una verifica Lean riuscita conferma solo che la dimostrazione discende dall'enunciato così come scritto in Lean. Non dimostra che l'enunciato corrisponda al problema originale, né che il risultato sia nuovo o importante. Queste domande richiedono ancora la revisione dei matematici.

I ricercatori hanno già sollevato preoccupazioni riguardo al materiale e al modo in cui è stato rilasciato. Dmitry Rybin ha scritto su X:

I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math? Somehow the model found that any K-coloring <=> "weakly measurable" K-coloring, which seems out of nowhere 1/2 pic.twitter.com/W13ScT3nel — Dmitry Rybin (@DmitryRybin1) October 7, 2026

Keith Adler ha scritto su X:

The openai/math repo has Issues turned off and has never accepted a pull request. That's disappointing. If you publish 722 manuscripts and ask for Lean formalisations, you need somewhere for people to send them. I'm formalising OpenAI's Saxl's Conjecture proof in Lean 4 against… — Keith Adler (@keithadler) October 7, 2026

Anche l'Institute for Advanced Study di Princeton, nel New Jersey, ha messo in dubbio le implicazioni del lavoro matematico generato dall'IA. "Ora è il caso che l'IA possa produrre argomenti matematici in situazioni in cui l'essere umano che l'ha sollecitata non è in grado di comprenderli, verificarli o risponderne", ha dichiarato l'istituto in una dichiarazione. "Riteniamo che la comprensione umana della matematica rimanga di importanza fondamentale. Come, in questa nuova era, possiamo lavorare verso un nuovo paradigma che includa la comprensione umana della matematica come parte di una produzione accademica responsabile?"

Il professor Abhishek Saha ha espresso un giudizio più positivo, scrivendo: "È un giorno molto importante per la matematica". Ha affermato che la maggior parte dei risultati rientrava in categorie come "progressi eccezionali all'interno di un programma esistente" e "scoperte sorprendenti". Secondo la sua valutazione, la collezione contiene problemi interessanti ma non risultati paragonabili ai problemi del millennio, le sette questioni da 1 milione di dollari del Clay Mathematics Institute. Ha identificato l'Ipotesi Quasi-Riemann come l'unico dei 722 risultati a raggiungere quel livello di rilevanza.

Saha ha scritto su X:

Some further thoughts on the 372 results released by OpenAI today, across 722 manuscripts. If I were to classify theorems that mathematicians prove and publish according to their groundbreaking nature, I would (very roughly) divide them into four categories: A) Non-breakthrough… — Abhishek Saha (@ObhishekSaha) October 7, 2026

Il rilascio non ha inoltre soddisfatto le raccomandazioni emesse da un gruppo consultivo dell'Institute for Advanced Study il 29 settembre. Il gruppo aveva raccomandato di divulgare il nome del modello, i prompt, una sintesi della catena di ragamento, il tempo impiegato e il costo di calcolo per ogni risultato. OpenAI ha fornito cifre medie di calcolo e 10 sintesi di ragionamento, ma non i prompt. L'azienda ha dichiarato di continuare a lavorare per rilasciare il modello in modo responsabile.

Daniel Litt, matematico dell'Università di Toronto, ha assunto la posizione opposta, sostenendo che non vi era motivo di chiedere a OpenAI di mantenere segrete le risposte a queste questioni matematiche.

Anthropic ha adottato un approccio diverso il mese scorso, pubblicando su GitHub tutte le 13 milioni di righe di una dimostrazione verificata in Lean dell'Ultimo Teorema di Fermat. Quel lavoro ha formalizzato un teorema pubblicato da Andrew Wiles nel 1995, piuttosto che presentare nuovi risultati matematici. I due rilasci illustrano una divisione nelle strategie di divulgazione nel settore: da un lato una dimostrazione completa e verificata da macchina di un teorema noto, dall'altro un ampio lotto di nuove affermazioni con verifica formale parziale.

OpenAI ha dichiarato che aggiungerà le formalizzazioni Lean man mano che le otterrà. Per ora, 162 dei 722 manoscritti ne hanno una. La posizione degli altri dipende ora da ciò che i ricercatori dicono di volere di più: il rilascio del modello, i prompt sottostanti e le formalizzazioni indipendenti dei manoscritti rimanenti.