Settecentodiciannove manoscritti di matematica, pubblicati su GitHub in un colpo solo e con licenza Apache-2.0. Li ha scritti un modello di OpenAI che nessuno di noi può usare. Una parte della comunità matematica ha risposto con rabbia, e su diversi punti ha ragione. Resta però un fatto che nessuna protesta cancella: produrre dimostrazioni sta diventando economico. Per chi oggi comincia un dottorato la domanda non è più se l’IA farà matematica. È quale lavoro resterà agli umani e chi sarà pronto a farlo.

Cosa ha pubblicato davvero OpenAI

Il 6 ottobre 2026 OpenAI ha aperto il repository openai/math. Il README conta 719 manoscritti in 372 famiglie. Unite.AI e DataCamp parlano di 722, segno che il conteggio cresce con gli aggiornamenti. Everyeye titola invece su “377 soluzioni” e non spiega la differenza. I risultati vengono da un modello interno non rilasciato: gli sono stati posti circa 4.000 problemi, con una media di circa tre ore di ChatGPT Pro thinking per ogni risultato.

Secondo DataCamp il materiale copre una ventina di sotto-discipline e comprende oltre 80 articoli di informatica teorica. Circa il 42% dei risultati principali è formalizzato in Lean, il dimostratore che controlla ogni passaggio in modo meccanico. Sul resto il README è onesto: “Some of the unformalized results could have issues”, cioè alcuni risultati non formalizzati potrebbero contenere errori.

Due titoli vanno ridimensionati. Il lavoro sulla funzione zeta non dimostra l’ipotesi di Riemann: stabilisce una regione senza zeri per Re(s) > 11/12. Il lavoro sulla congettura di Hodge riguarda il caso particolare delle varietà abeliane CM. Il README tratta entrambi come eccezioni alla procedura standard. E il contesto conta: l’8 settembre, ricorda Unite.AI, OpenAI aveva già annunciato una singolarità in tempo finito per Navier–Stokes, formalizzata in Lean.

Perché i matematici sono furiosi (e hanno ragione a metà)

Il 29 settembre l’Advisory Group on Mathematics and AI dell’IAS aveva pubblicato le sue raccomandazioni, dopo oltre 600 risposte dalla comunità. Riguardo a OpenAI la posizione è netta: “we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models”. In sostanza chiede di non usare problemi aperti per testare modelli proprietari. Una settimana dopo sono arrivati i 719 file.

L’Association for Human Mathematics (AHM) è stata ancora più dura: “We reject OpenAI’s assertion that this release advances our subject”. E ancora: “Releasing over 700 files at once is not a demonstration of scholarship”. Secondo Futurism, Terence Tao ha rilanciato la dichiarazione. Everyeye riporta l’accusa di ignorare le normali pratiche di ricerca e il rischio di una “matematica a due velocità”: laboratori privati che producono più in fretta di quanto la comunità riesca a verificare.

Le critiche fondate sono tre. Il modello è chiuso. I prompt e le catene di ragionamento complete non sono state pubblicate, come nota DataCamp. Inoltre alcune dimostrazioni, scrive Futurism, sono quasi incomprensibili per un essere umano.

Il quadro però ha anche l’altra metà. Il materiale è sotto Apache-2.0: chiunque può leggerlo, controllarlo e riusarlo. Il 42% formalizzato in Lean è verificabile da una macchina senza fidarsi di OpenAI. Secondo DataCamp, due ricontrolli indipendenti hanno superato una prima ispezione. Un’azienda che pubblica tutto, errori possibili compresi, non è il peggiore dei mondi possibili. Peggio sarebbe tenere tutto chiuso in un cassetto.

Il nuovo collo di bottiglia è la verifica

DataCamp distingue quattro livelli di verifica: formalizzazione in Lean, controllo umano, peer review e verifica indipendente. Non sono intercambiabili. Lean garantisce che la dimostrazione sia corretta rispetto all’enunciato, ma non garantisce che l’enunciato descriva il problema giusto. E pubblicare su GitHub non equivale a una peer review.

Qui sta il punto. Se generare dimostrazioni costa poco, il valore si sposta su chi sa controllarle, interpretarle e formalizzarle. Le fonti non lo dicono esplicitamente: è una nostra inferenza. Ma i segnali vanno in quella direzione.

Uno di questi segnali viene da Carnegie Mellon. Sidharth Hariharan, dottorando, guida la formalizzazione in Lean della dimostrazione di Viazovska e usa anche strumenti di IA come Claude. A gennaio 2026 Math, Inc. ha dichiarato di aver verificato la dimostrazione in circa due settimane, contro i mesi previsti. La sintesi di Hariharan è la più lucida che si possa leggere oggi: “I think AI is capable of formalizing mathematics but not canonizing it”. L’IA può formalizzare la matematica, ma non decidere cosa entra nel canone. Quel giudizio resta umano.

Alla nuova leva, senza giri di parole

Le frasi che seguono sono dure, e sono opinioni nostre.

Se la tua competenza principale è produrre a mano lemmi tecnici di routine, sei in concorrenza con una macchina che lavora tre ore per risultato. Non è un insulto, è una questione di costi. Tre anni di dottorato spesi su quel tipo di lavoro, senza imparare a verificarlo e a dargli senso, rischiano di valere poco.

Rifiutare Lean per principio è una posizione comoda, non una posizione seria. Il dottorando della CMU non ha aspettato che qualcuno gli desse il permesso.

Il rischio opposto è altrettanto grave. Chi usa il modello per firmare risultati che non capisce non fa ricerca: fa da intermediario. La comunità se ne accorgerà, e farà bene.

La nuova leva ha un vantaggio enorme che la generazione precedente non aveva: strumenti che moltiplicano la capacità di un singolo ricercatore. Sprecarlo per orgoglio o per pigrizia sarebbe l’errore vero.

Cosa puoi fare tu, concretamente

Leggi le notizie per livelli. Davanti a un “l’IA ha dimostrato X”, chiediti tre cose: è formalizzato in Lean? Qualcuno lo ha controllato? È passato da una peer review? Spesso la risposta ridimensiona il titolo.

Apri il repository. È pubblico. Scegli un risultato formalizzato e confronta l’enunciato in Lean con quello scritto in linguaggio naturale. È il modo più rapido per capire dove finisce la garanzia della macchina.

Se studi o fai ricerca, impara le basi di Lean. La formalizzazione è il ponte tra la produzione automatica e la fiducia. Chi sa attraversarlo avrà lavoro.

Usa l’IA per formalizzare e controllare, non per firmare. Ogni risultato che presenti come tuo devi saperlo spiegare.

Porta la regola nel tuo campo. Chi viene da Bitcoin la conosce già: don’t trust, verify. Vale per un teorema, per un contratto e per una transazione.

Conclusione

OpenAI ha scelto un metodo discutibile: modello chiuso, pubblicazione in blocco e scarso rispetto per chi aveva chiesto prudenza. Le critiche dell’AHM e dell’AGMAI meritano ascolto. Il messaggio di fondo però non cambia: le macchine sanno già produrre matematica non banale, e una parte la sanno anche certificare. La disciplina non muore. Cambia il mestiere: meno tempo a scrivere passaggi di routine, più tempo a scegliere i problemi, controllare gli enunciati e decidere cosa conta. Chi si prepara ora per quel lavoro ci arriva in vantaggio. Chi aspetta che passi rischia di restare indietro.

Fonti: