OpenAI pubblica 722 lavori matematici: Lean ne verifica solo una parte

14 ottobre 2026 alle ore 13:00|Autore: Redazione QUASA|5 min di lettura| 1

Il 6 ottobre 2026 OpenAI ha pubblicato su GitHub una raccolta di lavori matematici prodotti con un modello interno, insieme a formalizzazioni in Lean e sintesi del ragionamento. Un censimento della pubblicazione iniziale conta 722 manoscritti in 372 famiglie: 185 risultati principali hanno una verifica formale associata a 162 manoscritti. Il totale dei documenti e quello degli enunciati controllati descrivono dunque aspetti diversi della raccolta.

Il modello che ha prodotto i lavori non è stato reso disponibile al pubblico. OpenAI ha pubblicato i testi e parte delle prove formali per consentirne l’esame, ma la raccolta comprende risultati a stadi diversi di verifica. Da quando è stata aperta, alcuni manoscritti sono stati ritirati o modificati: i numeri della pubblicazione iniziale non descrivono più da soli lo stato del catalogo.

Che cosa contano manoscritti e famiglie

Un manoscritto è un singolo lavoro; una famiglia riunisce testi legati allo stesso filone di risultati. Può includere un risultato principale, argomenti complementari, conseguenze oppure una dimostrazione alternativa. Perciò più documenti possono sviluppare la stessa questione matematica, e contarli come scoperte indipendenti attribuirebbe al totale un significato che non ha.

La raccolta nasce da problemi di ricerca sottoposti al modello durante il suo sviluppo. OpenAI ha organizzato e selezionato gli esiti giudicati abbastanza significativi da pubblicare. Il numero dei manoscritti misura i testi conservati dopo questa selezione, non la quota di problemi risolti fra tutti quelli tentati: un calcolo del genere richiederebbe anche di conoscere e classificare gli insuccessi con criteri comparabili.

La distinzione conta anche per i lavori più ambiziosi. Un’affermazione centrale può avere più manoscritti di supporto, mentre un altro testo può presentare una conseguenza che dipende da quella stessa affermazione. Se emerge un errore nell’argomento di partenza, la correzione può quindi riguardare anche lavori collegati. L’organizzazione in famiglie rende visibili questi rapporti, ma non assegna automaticamente a ogni documento lo stesso grado di controllo.

Che cosa verifica Lean

Lean controlla una prova espressa in un linguaggio formale. Per accettarla, verifica che l’enunciato derivi dalle definizioni, dagli assiomi ammessi e dai passaggi forniti. Nella raccolta, Comparator collega l’enunciato da dimostrare alla soluzione formale e controlla che la prova accettata riguardi proprio quell’enunciato. Il controllo è preciso, ma ha per oggetto la formulazione codificata, non ogni frase del manoscritto scritto in linguaggio naturale.

Questo spiega perché il conteggio dei risultati principali formalizzati differisca da quello dei manoscritti che li ospitano. Un documento può essere associato a più enunciati controllati; altri documenti della stessa famiglia possono non avere una formalizzazione del loro risultato centrale. Anche quando una prova è presente, applicazioni, lemmi o conseguenze discusse nel testo possono restare fuori dal suo perimetro. La presenza di codice Lean, da sola, non equivale quindi alla verifica integrale del lavoro che lo accompagna.

Rimane una valutazione matematica che il verificatore non svolge: stabilire se l’enunciato formalizzato esprima fedelmente il problema di ricerca rivendicato nel testo. Lean può accettare una prova corretta di una versione più circoscritta senza pronunciarsi sulle conclusioni ulteriori del manoscritto. Novità, importanza e rapporto con la letteratura precedente richiedono inoltre il giudizio degli specialisti. Le note che accompagnano le formalizzazioni delimitano quali affermazioni sono state tradotte e quali restano affidate alla dimostrazione in prosa.

I ritiri e il nuovo conteggio del catalogo

La cronologia del repository registra per il 7 ottobre 2026 il ritiro di tre manoscritti, la revisione di altri 14 e l’aggiornamento dei riferimenti in 13 lavori collegati; indica ora 719 manoscritti e 300 risultati principali formalizzati, circa il 42% del catalogo corrente. Il ritiro è seguito alla scoperta di un errore di segno che comprometteva un argomento e la costruzione usata da due lavori dipendenti. Le revisioni comprendono riparazioni di prove, enunciati corretti e ipotesi rese più chiare.

Il conteggio aggiornato delle formalizzazioni e il censimento iniziale delle prove associate ai manoscritti usano versioni e unità di misura diverse. Non si può leggere la loro differenza come un semplice numero di nuove dimostrazioni: il primo dato riguarda i risultati principali nel catalogo corrente, il secondo contava gli enunciati con una configurazione di verifica in un insieme iniziale di documenti. La crescita delle formalizzazioni va quindi interpretata insieme alle modifiche del catalogo e al perimetro preciso di ciascuna prova.

La verifica indipendente dei risultati

Pubblicare manoscritti, codice e versioni precedenti permette ai matematici di esaminare le ipotesi, ricostruire gli argomenti e valutare le dipendenze fra lavori. Questo esame va oltre il controllo automatico di un enunciato: comprende le parti rimaste in linguaggio naturale e il confronto con risultati già conosciuti. Una prova formale può eliminare errori logici nella formulazione che verifica, mentre la valutazione del contributo scientifico riguarda l’intero risultato rivendicato.

I ritiri mostrano una conseguenza concreta di questa distinzione. I testi archiviati documentano che cosa era stato pubblicato inizialmente; quelli rimasti nel catalogo corrente rappresentano le affermazioni ancora sostenute dopo le prime correzioni. OpenAI prevede di aggiungere altre formalizzazioni. Per i risultati ancora privi di una prova formale del loro enunciato centrale, la lettura indipendente dei matematici resta il passaggio decisivo per stabilire quali conclusioni reggano.