Il 6 ottobre OpenAI ha pubblicato manoscritti matematici prodotti da un modello interno. Il repository pubblico segnala diversi livelli di verifica e possibili errori. Non è il rilascio di un nuovo modello agli utenti né una raccolta di risultati che Neudyne abbia confermato sul piano matematico.

Una parte del lavoro dispone di formalizzazioni in Lean, che consentono il controllo informatico di enunciati precisi. Questo non equivale a confermare ogni formulazione del manoscritto associato. Esistono istruzioni per compilare la libreria; noi non abbiamo compilato le dimostrazioni. Più del numero di file conta la corrispondenza tra l'affermazione del testo e ciò che l'artefatto di verifica copre davvero.

Il gruppo consultivo indipendente AGMAI chiede spiegazioni comprensibili e responsabilità umana per i contenuti matematici. Consultarlo non è quindi un certificato di correttezza. Immaginiamo un esito più utile di un titolo sulla macchina miracolosa: una matematica riceve un'idea nuova, ne individua un punto debole e sviluppa un metodo affidabile per continuare la ricerca.

Se questi metodi reggessero, potrebbero aiutare a ricavare limiti per algoritmi di ottimizzazione o a preparare componenti software verificati formalmente. È un nostro scenario realistico, non un'applicazione dimostrata di questa raccolta. Prima servono controlli sulle ipotesi, sui collegamenti con la letteratura e sulla dimostrazione stessa. Soltanto dopo si potrà valutarne l'utilità pratica.

La nostra stima editoriale ottimistica è di 4–12 settimane per le prime analisi pubblicate di singoli enunciati, se vi lavoreranno gli specialisti adatti. Non possiamo assegnare un termine analogo all'accettazione dell'intera raccolta o all'impiego nei prodotti. Il vero interesse non è la velocità dell'annuncio, ma la possibilità che un'idea superi controlli al di fuori del suo autore.