In un articolo pubblicato il 19 ottobre, il Daily Californian ha riferito le posizioni divergenti dei matematici di UC Berkeley Richard Borcherds e Robin Huang sull’IA nella ricerca matematica. Il loro confronto arriva dopo una critica tecnica, pubblicata il 6 ottobre, che individua discrepanze tra alcune parti della prova di Navier-Stokes annunciata da OpenAI e la relativa formalizzazione in Lean. Gli autori della critica non sostengono che la dimostrazione in linguaggio naturale sia errata.
Due visioni dell’IA nella matematica
Borcherds, professore di matematica a UC Berkeley e vincitore della Medaglia Fields nel 1998, ritiene che, se la tendenza attuale proseguirà, l’IA potrebbe superare i matematici umani nella ricerca entro pochi anni. Huang, dottoranda all’ultimo anno, ha posto l’accento sui rischi per la formazione: secondo lei, chi delega all’IA i compiti di matematica può arrivare impreparato agli esami. Ha anche sollevato dubbi sugli standard e sugli incentivi della comunità matematica.
NeoTeo aveva già raccontato la pubblicazione dei risultati matematici ottenuti da un modello interno di OpenAI. Qui il punto centrale è la differenza tra controllare una dimostrazione formalizzata e verificare che essa corrisponda davvero al testo scritto.
Che cosa sostiene OpenAI sul problema di Navier-Stokes
Nell’annuncio dell’8 settembre 2026, OpenAI ha presentato un risultato che, secondo l’azienda, produce una singolarità in tempo finito nelle equazioni di Navier-Stokes per un fluido incomprimibile tridimensionale sottoposto a una forza esterna liscia. OpenAI sostiene che il risultato affronti le parti C e D della formulazione del problema del Clay.
L’azienda ha riferito che il gruppo di agenti impiegato per questo problema arrivava a circa 10.000 agenti concorrenti e ha indicato 2,7 milioni di messaggi e circa 130 miliardi di token in uscita. Queste cifre descrivono la scala del lavoro riportata da OpenAI.
La discrepanza tra la prova scritta e Lean
Il 6 ottobre A. Bastounis, F. Circelli e A. C. Hansen hanno pubblicato un’analisi della formalizzazione in Lean. Tra gli esempi, confrontano la stima della Lemma 8.6 nel testo in linguaggio naturale con quella citata nella versione Lean: la prima coinvolge quattro derivate aggiuntive, la seconda cinque.
| Versione della stima | Derivate aggiuntive indicate |
| Testo in linguaggio naturale | 4 |
| Stima citata nella formalizzazione Lean | 5 |
Gli autori segnalano anche differenze nella stima del flusso di pressione: quella descritta nel testo usa un termine in B_R, mentre la stima Lean dipende anche da A_R. Dicono che le due espressioni sono difficili da confrontare direttamente.
Che cosa controlla una dimostrazione in Lean
Lean è un assistente per le dimostrazioni formali: controlla la prova e l’enunciato matematico così come sono codificati nel sistema. La compilazione, da sola, non stabilisce che l’enunciato e i passaggi codificati corrispondano fedelmente alla dimostrazione in linguaggio naturale. È questa corrispondenza, nei casi esaminati, il problema sollevato da Bastounis, Circelli e Hansen.
