OpenAI pubblica 719 manoscritti di matematica da un modello non rilasciato: cosa ha verificato Lean, cosa no, e perché i matematici chiedono le prove

OpenAI pubblica 719 manoscritti di matematica da un modello non rilasciato: cosa ha verificato Lean, cosa no, e perché i matematici chiedono le prove

Il 6 ottobre 2026 OpenAI ha pubblicato Sharing AI progress in mathematics e, la sera stessa, ha aperto un repository GitHub, openai/math, con licenza Apache-2.0. Il repository contiene manoscritti e file Lean prodotti da quello che OpenAI chiama «un modello frontier interno», un modello che non ha rilasciato. La mattina dell'8 ottobre il README elencava 719 manoscritti in 372 famiglie. Al lancio erano 722; tre sono stati ritirati il 7 ottobre. Secondo il README, durante la valutazione al modello sono stati posti circa 4.000 problemi, e circa il 42% dei risultati principali è formalizzato in Lean. Il post di OpenAI dice che in media ogni risultato ha richiesto l'equivalente di circa tre ore di ragionamento di ChatGPT Pro.

Le due voci che fanno i titoli sono una presunta dimostrazione della congettura di Hodge razionale per le varietà abeliane CM, un caso particolare e non la congettura generale, e un presunto semipiano libero da zeri, Re s > 7/8, per ogni funzione L di Dirichlet, compresa la zeta di Riemann. Il repository chiama questo secondo risultato «ipotesi quasi-Riemann». Non è l'ipotesi di Riemann. Sono proprio i due risultati che il README indica come eccezioni alla sua procedura standard, e nessuno di questi manoscritti è passato dalla revisione tra pari. Lean ha controllato una fetta ampia del catalogo, non tutto, e superare un controllo non equivale a capire.

Di seguito: cosa è stato pubblicato, le due affermazioni in parole semplici, cosa chiude Lean, cosa è stato ritirato e cosa dicono i matematici. L'8 ottobre 2026 abbiamo riletto il repository (API GitHub, README, file history e catalogo), il post di OpenAI, il pezzo di Scientific American del 6 ottobre e la dichiarazione dell'Association for Human Mathematics. Le citazioni dall'inglese sono tradotte da noi.

Il post. L'annuncio di OpenAI dice che i risultati sono stati «prodotti da un modello frontier interno» e che l'azienda «sta lavorando per rilasciare in modo responsabile il modello che ha prodotto questi risultati». Promette formalizzazioni in Lean di «molte delle dimostrazioni», dieci sintesi del ragionamento del modello e statistiche sui problemi tentati. Dice anche che OpenAI finanzierà una serie di workshop, conferenze e programmi speciali dedicati alla comprensione dei grandi risultati prodotti dall'IA. Il post non riporta il numero di manoscritti o di famiglie e non nomina né Hodge né la zeta. Quei dettagli stanno nel repository.

Il repository. L'API di GitHub mostra che openai/math è stato creato a tarda sera del 6 ottobre, ora italiana, con licenza Apache-2.0. Il README parla di manoscritti matematici e materiali di supporto alle dimostrazioni prodotti da un modello interno di OpenAI, e spiega che le valutazioni sono state estese dopo che le prestazioni sui benchmark matematici esistenti erano arrivate a saturazione. Al momento della stesura il catalogo conta 719 manoscritti in 372 famiglie. Una famiglia raggruppa un risultato principale con argomenti collegati, conseguenze o dimostrazioni alternative.

Stato della formalizzazione. Il README indica circa il 42% dei risultati principali formalizzato. Il file history fa il conto: 300 su 719. Sul resto il README è franco: non tutti i risultati hanno una formalizzazione Lean, e alcuni di quelli non formalizzati «potrebbero avere problemi»; OpenAI dice che cercherà di correggerli rapidamente.

Procedura. Secondo il README la «grande maggioranza» dei risultati segue la stessa procedura, con due eccezioni: il lavoro sugli zeri della funzione zeta e quello su Hodge per le varietà CM.

Attenzione e orari. La mattina dell'8 ottobre il repository aveva superato le 10.000 stelle su GitHub, secondo l'API di GitHub. È una misura di interesse, non di correttezza. Scientific American riporta che il repository è diventato pubblico alle 18:00 EDT del 6 ottobre, cioè a mezzanotte in Italia.

Hodge, solo il caso CM. In parole semplici, prendendo come contesto il testo divulgativo di Claire Voisin sul blog di Terence Tao del 12 settembre (precede il rilascio e non dice nulla su questa affermazione): la congettura di Hodge sostiene che certe classi di coomologia su una varietà proiettiva complessa liscia, le «classi di Hodge», siano sempre algebriche, cioè provengano da combinazioni di sottovarietà. Il caso generale è uno dei problemi del Millennio del Clay Institute ed è ancora aperto. Nella mappa dei manoscritti la famiglia 032 di OpenAI rivendica la congettura di Hodge razionale per le varietà abeliane CM, una famiglia speciale e molto simmetrica. Il README la colloca fuori dalla procedura standard e, nel catalogo del repository all'8 ottobre, non ha alcuna formalizzazione Lean.

Un semipiano senza zeri, non l'ipotesi di Riemann. L'ipotesi di Riemann dice che tutti gli zeri non banali della funzione zeta stanno esattamente sulla retta Re s = 1/2. Un semipiano libero da zeri dice qualcosa di più debole: non ci sono zeri a destra di un'altra retta verticale. La famiglia 003 di OpenAI afferma che nessuna funzione L di Dirichlet, zeta compresa, ha zeri con Re s > 7/8. Il manoscritto principale è datato 30 settembre e copre anche le funzioni L di Hecke di ordine finito su Q(√-3). Il repository la chiama «ipotesi quasi-Riemann». È un'etichetta sua. L'affermazione lascia intatta tutta la striscia tra 1/2 e 7/8, quindi non è l'ipotesi di Riemann.

Il manoscritto collegato. Un secondo manoscritto della famiglia, datato 5 ottobre, propone un argomento alternativo per un semipiano più debole, Re s > 11/12. Secondo il README quella stesura è stata ritoccata a mano per leggibilità, e il lavoro sugli zeri è fuori dalla procedura standard. La nota Lean del repository sulla famiglia 003 copre il limite 7/8 per la zeta, per le funzioni L di Dirichlet e per il caso di Hecke. Un controllo formale di questo tipo pesa. Resta comunque un'affermazione in un manoscritto che non è passato dalla revisione tra pari.

Cosa dà Lean. Lean è un linguaggio di programmazione in cui un computer controlla che un enunciato formale segua, passo dopo passo, dalle definizioni di una libreria. Scientific American scrive che molti risultati sono già stati verificati in Lean e sono quindi «quasi certamente corretti». Fin qui è giusto. Ma il controllo Lean non dice se l'enunciato formale corrisponde all'affermazione scritta nell'articolo, se il risultato è nuovo o se le idee serviranno a qualcuno. Queste restano domande per le persone. Il README rimanda anche a una procedura Comparator per controllare gli enunciati formali stessi.

La divisione, con i numeri di OpenAI. Circa il 42% dei risultati principali è formalizzato, 300 su 719. Il resto sono dimostrazioni in prosa che, con le parole del README, «potrebbero avere problemi». Le due voci di punta stanno ai lati opposti di questa linea: l'affermazione sul semipiano 7/8 ha una voce Lean, quella su Hodge per le varietà CM no, all'8 ottobre.

Ritiri nel giro di un giorno. Il 7 ottobre il file history ha registrato che un errore di segno invalida un argomento di cancellazione in un manoscritto e in due lavori che ne dipendevano. OpenAI li ha ritirati tutti e tre: «Algebraicity of Weil classes on split abelian eightfolds», «Algebraicity of Kuga–Satake Correspondences for K3 Surfaces» e «The rational Hodge conjecture for products of K3 surfaces». Ha poi rivisto altri 14 manoscritti con correzioni alle dimostrazioni e agli enunciati. Per precisione: il lavoro sulle superfici K3 è un manoscritto su Hodge diverso dall'affermazione sulle varietà CM, che resta nel catalogo. Resta il fatto che un'affermazione vicina a Hodge è stata ritirata circa un giorno dopo il rilascio, e il file history è il registro delle correzioni da seguire.

Un'abitudine per chi legge. Quando un titolo cita una congettura famosa, controlla tre cose: il caso particolare esatto nel titolo usato dal repository, se la famiglia ha una voce Lean e se il file history riporta ritiri o revisioni.

Le ricevute. Andrew Sutherland, del MIT, ha detto a Scientific American: «Finché non rilasceranno il modello e altri non potranno replicare i risultati, credo che qualsiasi affermazione sul risolvere problemi al primo colpo con un singolo agente vada considerata non verificata». E poi: «Dovremmo chiedere le ricevute». Il portavoce di OpenAI aveva detto alla rivista che il modello ha prodotto quasi tutti i risultati in risposta a un unico prompt affidato a un unico agente, e che alcuni potrebbero aver richiesto più tentativi.

Le norme del gruppo consultivo. Secondo Scientific American, il gruppo consultivo indipendente di matematici annunciato il 21 settembre raccomanda che chi pubblica risultati di questo tipo renda pubblici il modello, il prompt esatto e il tempo di calcolo dietro ciascuno. OpenAI pubblica il calcolo medio e alcune statistiche, nessun prompt. Il suo portavoce ha detto che l'azienda prende sul serio le linee guida, ma non è vincolata a rispettarle.

La critica aperta. L'Association for Human Mathematics, in una dichiarazione ripubblicata come guest post sul blog di Terence Tao il 7 ottobre, ha scritto: «Pubblicare oltre 700 file in una volta non è una dimostrazione di erudizione, ma una dimostrazione di potere». E ha invitato matematici e pubblico a valutare questo modello di pubblicazione «con il dovuto scetticismo». Scientific American nota a parte che Tao ha criticato i laboratori frontier per il ritmo «folle» dei loro risultati generati con l'IA.

L'altra voce. Daniel Litt, dell'Università di Toronto, sempre a Scientific American: «Se vogliamo conoscere le risposte a queste domande matematiche, non vedo perché dovremmo chiedere all'azienda di tenerle segrete». E ancora: «Per me sarà una cosa buona per la matematica».

Chi fa i controlli. Il portavoce di OpenAI ha detto alla rivista anche che molti dei nuovi risultati non sono ancora compresi nemmeno dai matematici dell'azienda. Qualcuno deve leggere 719 manoscritti, e gran parte di quella lettura toccherà a matematici che non vengono pagati per farla.

---

A che punto siamo all'8 ottobre 2026. Il repository openai/math di OpenAI (Apache-2.0) elenca 719 manoscritti in 372 famiglie prodotti da un modello non rilasciato, contro i 722 iniziali, dopo tre ritiri il 7 ottobre. Circa il 42% dei risultati principali è formalizzato in Lean. La voce su Hodge è un'affermazione limitata alle varietà abeliane CM, ancora senza voce Lean. Quella sugli zeri è un'affermazione con voce Lean: nessuna funzione L di Dirichlet, zeta compresa, avrebbe zeri con Re s > 7/8. Il repository la chiama ipotesi quasi-Riemann; non è l'ipotesi di Riemann, che riguarda la retta Re s = 1/2. Nessuno dei manoscritti è passato dalla revisione tra pari.

Il conteggio del catalogo è già cambiato una volta. Prima di citare un numero, controlla il README e il file history.