Il 7 ottobre OpenAI ha ritirato tre manoscritti matematici dopo che un errore di segno aveva invalidato un argomento e una costruzione usata in due lavori dipendenti. La cronologia del repository registra anche revisioni a 14 manoscritti e aggiornamenti bibliografici in altri 13. L’azienda aveva annunciato la pubblicazione dei risultati il 6 ottobre.

OpenAI ritira tre manoscritti dopo un errore

L’errore riguardava un argomento sulla cancellazione della traccia di stabilizzazione e una costruzione impiegata da due manoscritti dipendenti. Nella cronologia del repository, OpenAI registra il ritiro dei tre lavori il 7 ottobre.

La pubblicazione era stata annunciata il 6 ottobre: i risultati provenivano da un modello interno di frontiera. OpenAI afferma che la valutazione ha sottoposto al modello circa 4.000 problemi matematici aperti.

Che cosa contiene il repository matematico di OpenAI

Il catalogo del repository conta 719 manoscritti in 372 famiglie di risultati. I due numeri indicano unità diverse: una famiglia riunisce lavori collegati e può comprendere un risultato principale, argomenti complementari, conseguenze o dimostrazioni alternative.

OpenAI stima che il calcolo impiegato per un risultato medio equivalesse a circa tre ore della modalità Thinking di ChatGPT Pro. Si tratta di una stima dell’azienda riferita alla quantità di calcolo, non di una misura della durata di ciascuna dimostrazione.

Che cosa significa formalizzare un risultato in Lean

OpenAI indica che 300 dei 719 risultati principali, circa il 42%, sono formalizzati in Lean. Una formalizzazione traduce la prova in una forma che il software può controllare; Lean è un assistente di dimostrazione usato per verificare formalmente i passaggi.

La formalizzazione riguarda la prova codificata e non misura, da sola, la rilevanza matematica del risultato. Perciò il dato del 42% non equivale a una valutazione complessiva di tutti i manoscritti.

A che punto è la verifica dei risultati

OpenAI descrive la raccolta come composta da risultati a diversi livelli di verifica e avverte che alcuni di quelli senza formalizzazione Lean potrebbero contenere problemi. La quota formalizzata e i ritiri registrati nella cronologia restituiscono così due aspetti distinti della pubblicazione: una parte dei risultati è espressa in una forma verificabile dal computer, mentre la raccolta comprende anche manoscritti corretti o ritirati.