Il 6 ottobre 2026 OpenAI ha pubblicato su GitHub il repository openai/math, con 722 manoscritti di matematica prodotti da un modello interno non rilasciato e raggruppati in 372 famiglie di risultati. È lo stesso modello che a settembre aveva prodotto la dimostrazione su Navier-Stokes.

Al modello sono stati posti circa 4.000 problemi. In media un risultato ha richiesto l’equivalente di tre ore di ragionamento di ChatGPT Pro. Per 235 famiglie su 372 c’è una formalizzazione in Lean, almeno del risultato principale, il linguaggio che permette a un computer di verificare una dimostrazione passo per passo.

Che cosa contiene

Fra i risultati dichiarati, quelli che hanno fatto più rumore sono questi.

  • La Unique Games Conjecture di Subhash Khot, centrale in informatica teorica. Ne seguirebbe che non si può approssimare Max-Cut meglio dell’algoritmo di Goemans e Williamson, né Vertex Cover meglio di un fattore due, a meno che P sia uguale a NP.
  • L’ipotesi quasi-Riemann. La funzione zeta e tutte le funzioni L di Dirichlet non hanno zeri con parte reale maggiore di 7/8. L’ipotesi di Riemann chiede 1/2, quindi non è il problema del millennio, ma era proprio aperta la questione di un semipiano libero da zeri di questo tipo.
  • L’isomorfismo dei fattori dei gruppi liberi, una questione aperta da decenni nelle algebre di von Neumann.
  • Un controesempio alla congettura del divisore dello zero di Kaplansky, dopo che nel 2021 Giles Gardam aveva già trovato quello alla congettura dell’unità.
  • L’irrazionalità della costante di Catalan e il valore esatto dell’esponente di irrazionalità di π.

Altri risultati importanti, come la formula di Birch e Swinnerton-Dyer per tutte le curve ellittiche su ℚ con corango di Selmer 0 o 1 o i controesempi alla congettura di Baum-Connes, per ora non hanno la formalizzazione. OpenAI stessa scrive che alcuni risultati non formalizzati potrebbero contenere errori.

Come si controlla

Per i risultati formalizzati il controllo non dipende da OpenAI. Il repository include le sfide per Comparator, uno strumento della comunità Lean che verifica che il teorema dimostrato coincida con un enunciato di riferimento e che la dimostrazione usi solo i tre assiomi standard. Il controllo si può quindi rifare in modo indipendente su una macchina Linux con Lean e gli strumenti indicati nel repository.

Resta aperta una domanda che Lean non risolve: l’enunciato formale dice davvero quello che dice il titolo? Per la zeta l’enunciato è una riga, la funzione non si annulla quando la parte reale supera 7/8, ed è difficile sbagliarlo. Per risultati più strutturati la fedeltà della traduzione va letta da persone competenti, e su 722 manoscritti questo lavoro richiederà mesi.

OpenAI dice di aver consultato il gruppo consultivo dell’Institute for Advanced Study, che il 29 settembre aveva pubblicato le sue raccomandazioni. Sulla trasparenza le ha seguite in parte: riassunti del ragionamento per dieci famiglie, il calcolo medio e il numero di problemi posti, ma non il nome del modello né i prompt.

Le sfide per Comparator rispondono invece alla richiesta di formalizzare. Il gruppo chiede anche archivi non controllati dai laboratori, e per ora il repository è di OpenAI, che dice di valutare soluzioni gestite dalla comunità.

Il 6 ottobre il gruppo ha precisato che il suo ruolo non va letto come un avallo del processo, e che giudicare quanto le raccomandazioni siano state rispettate spetta alla comunità matematica.

Cosa ne penso

Per la matematica intesa come produzione di dimostrazioni una fase è finita. Fino a ieri la risorsa scarsa era trovare la dimostrazione. Oggi è verificare che l’enunciato sia quello giusto, capire perché il risultato è vero e decidere quali problemi vale la pena porre. È lo spostamento che le medaglie Fields firmatarie della dichiarazione dell’11 settembre chiedono di governare, perché la velocità dei risultati non vada a scapito della loro comprensione.

Per il resto del mondo la risposta è più prudente. Le conseguenze dirette di questi teoremi sono reali ma lente. Se gli zeri della zeta stanno sotto 7/8, l’errore nel teorema dei numeri primi scende a x elevato a 7/8 più epsilon, un miglioramento enorme per la teoria dei numeri.

Sulla crittografia l’effetto atteso è limitato: questi teoremi stabiliscono proprietà e limiti, non forniscono algoritmi di attacco, e RSA si basa sulla difficoltà di fattorizzare. La Unique Games Conjecture fissa limiti a quanto bene si possono approssimare certi problemi di ottimizzazione, e non accelera gli algoritmi esistenti: dice fin dove possono arrivare.

Quello che cambia il mondo è il metodo. Un modello a cui vengono posti circa quattromila problemi e che ne chiude alcune centinaia, con prove controllabili da una macchina, è lo stesso tipo di sistema che il paper di Cambridge sull’esplosione di intelligenza vede applicato alla ricerca sull’AI.

La matematica è il primo campo in cui si vede bene, perché ha un verificatore formale. Negli altri campi il verificatore è il laboratorio, ed è più lento.

La mia risposta alla domanda del titolo è che si è chiuso il tempo in cui la difficoltà di produrre un risultato ne garantiva anche la scarsità. Da qui in avanti il valore si sposta via via verso chi sa porre le domande e verificare le risposte.

Limiti

Al momento della scrittura non ho trovato conferme pubbliche dei risultati principali da parte di matematici esterni.

I manoscritti senza formalizzazione vanno considerati non verificati, e almeno un risultato, la regione libera da zeri con parte reale maggiore di 11/12, è stato rivisto da persone per la leggibilità. OpenAI dichiara inoltre che il lavoro sulla regione libera da zeri della zeta e quello sulla congettura di Hodge per le varietà abeliane CM non hanno seguito la procedura standard.

Il modello non è disponibile, quindi il processo non si può riprodurre dall’esterno. Gli enunciati di riferimento per Comparator li ha scritti OpenAI, e la loro corrispondenza con le congetture originali va controllata caso per caso.

Immagine di copertina: la prima pagina della memoria di Bernhard Riemann Ueber die Anzahl der Primzahlen unter einer gegebenen Grösse*, nel resoconto dell’Accademia delle scienze di Berlino del novembre 1859. È il testo in cui compare l’ipotesi di Riemann — pubblico dominio — https://commons.wikimedia.org/wiki/File:RiemannPrim1859.djvu*