OpenAI dice di aver risolto le equazioni di Navier-Stokes: cosa ha dimostrato davvero

Chi ha appoggiato una tazza di caffè bollente sul tavolo e ha guardato il vapore salire ha davanti l'oggetto matematico più ostinato della fisica classica. Per i primi centimetri il filo di vapore sale ordinato, quasi rigido. Poi si arriccia, si spezza in vortici che si inseguono e si assorbono, e capire dove sarà una singola spira un secondo dopo diventa impossibile. Le equazioni di Navier-Stokes descrivono quel passaggio, e sono le stesse che governano l'aria sopra l'ala di un aereo, la corrente del Golfo, il sangue dentro un'arteria. Si scrivono in poche righe. Nessuno sa ancora se abbiano sempre soluzione.

L'8 settembre 2026 OpenAI ha reso pubblici un documento matematico e una formalizzazione in Lean di quella che descrive come la risoluzione del problema di Navier-Stokes, uno dei sette Millennium Prize Problems del Clay Mathematics Institute. L'annuncio è arrivato circa dodici ore dopo un altro, di segno diverso, con cui Tristan Buckmaster del Courant Institute della New York University e Levent Alpöge, matematico che lavora per Anthropic, avevano pubblicato tre risultati su equazioni più semplici, ottenuti anch'essi con l'aiuto di modelli linguistici. Prima di qualsiasi altra cosa serve la precisazione importante, perché è quella che quasi tutti i rilanci hanno perso per strada.

Punti chiave

• La rivendicazione di OpenAI riguarda le affermazioni C e D dell'enunciato di Fefferman, quelle che ammettono una forza esterna liscia, mentre A e B, il caso con forza identicamente nulla, restano senza dimostrazione.

• Il regolamento del Clay Mathematics Institute, nella versione del 26 settembre 2018, richiede pubblicazione su una sede con revisione paritaria, almeno due anni di attesa e accettazione generale della comunità prima di qualsiasi esame del premio.

• Dei sette problemi da un milione di dollari annunciati il 24 maggio 2000 a Parigi, uno solo è stato chiuso, e Grigori Perelman rifiutò il premio il primo luglio 2010.

• L'impianto concettuale delle due dimostrazioni risale al programma di Diego Córdoba e Luis Martínez-Zoroa, che nel 2023 avevano ottenuto blowup per Euler con forzante irregolare.

• La formalizzazione in Lean certifica la correttezza deduttiva a partire dalle ipotesi scritte nel file, non la corrispondenza fra quelle ipotesi e la formulazione ufficiale del problema.

• OpenAI ha dichiarato di non voler rivendicare il milione di dollari e ha riconosciuto la priorità di Buckmaster e Alpöge sul caso di Euler forzato.

Che cosa è stato dimostrato e che cosa resta aperto

L'enunciato ufficiale del problema non chiede una cosa sola. Nel testo redatto da Charles Fefferman per il Clay Mathematics Institute vengono elencate quattro affermazioni alternative, e per vincere basta dimostrarne una. Le prime due, indicate con le lettere A e B, chiedono di provare che le soluzioni esistono e restano regolari per sempre, nello spazio tridimensionale infinito oppure nel caso periodico, e in entrambe la forza esterna è posta identicamente uguale a zero. Le altre due, C e D, chiedono il contrario, cioè di esibire un dato iniziale regolare e una forza esterna regolare per cui una soluzione liscia non esiste.

La rivendicazione di OpenAI riguarda C e D. Nel writeup pubblicato dall'azienda il risultato viene descritto come un fluido inizialmente in quiete, sottoposto a una forza liscia, che sviluppa una singolarità in tempo finito mantenendo energia finita per tutta l'evoluzione. La geometria è quella di un vortice che si avvita verso l'interno e si allunga come uno spaghetto, con il nucleo che si assottiglia mentre accelera.

Il punto è che A e B, il caso senza forza esterna, restano esattamente dove erano. La domanda che interessa a un fisico, ovvero se un fluido lasciato a se stesso possa spontaneamente arrivare a velocità infinita, non è stata toccata. Dentro le regole del Clay una prova di C chiude il problema, perché il regolamento accetta una qualsiasi delle quattro alternative. Dentro la fisica dei fluidi la faccenda è più stretta, perché la forza esterna è un ingrediente che il matematico può disegnare come vuole, purché resti regolare, e la difficoltà tecnica sta tutta nel farla restare tale mentre la velocità diverge.

Gli agenti di OpenAI dichiarano anche un secondo risultato, sulle equazioni di Euler, cioè Navier-Stokes senza viscosità. Quello riguarda la versione non forzata, ed è un enunciato che il Clay non premia perché Euler non è nella lista dei sette.

Sette problemi, un milione a testa e regole molto lente

I Millennium Prize Problems sono stati annunciati il 24 maggio 2000 al Collège de France, a Parigi, dal Clay Mathematics Institute, che ha destinato un fondo di sette milioni di dollari, un milione per ciascuno. La scelta è stata fatta dal comitato scientifico dell'istituto consultando specialisti di tutto il mondo, con un criterio esplicito, cioè privilegiare questioni classiche che avevano resistito per decenni. L'istituto ricorda che uno dei sette, l'ipotesi di Riemann, formulata nel 1859, compariva già nell'elenco dei ventitré problemi presentati da David Hilbert a Parigi il 9 agosto 1900.

Di quei sette, uno solo è stato chiuso. La congettura di Poincaré è stata risolta da Grigori Perelman, a cui il premio è stato assegnato il 18 marzo 2010 e che lo ha rifiutato il primo luglio dello stesso anno. All'agenzia Interfax Perelman disse di considerare il proprio contributo non superiore a quello di Richard Hamilton, il matematico che aveva aperto la strada con il flusso di Ricci, e di trovare la decisione dell'istituto ingiusta.

Le regole di assegnazione, nella versione adottata dal consiglio direttivo il 26 settembre 2018, spiegano da sole perché nessuno incasserà nulla a breve. L'istituto non accetta candidature dirette. Prima di poter anche solo esaminare una soluzione devono valere tre condizioni insieme, cioè la pubblicazione su una sede qualificata con revisione paritaria, il passaggio di almeno due anni dalla pubblicazione, e l'accettazione generale da parte della comunità matematica mondiale. Solo dopo il comitato scientifico decide se metterla in esame. OpenAI ha comunque dichiarato di non voler rivendicare il premio per questo risultato.

Perché la viscosità dovrebbe impedire il disastro

Le equazioni applicano la seconda legge di Newton a un fluido trattato come un mezzo continuo, quindi non come un insieme di molecole. È un'idealizzazione, e il fatto che un'idealizzazione possa produrre velocità infinite ha un significato preciso, cioè segnala il punto in cui il modello smette di descrivere il mondo e bisognerebbe passare a seguire le particelle una per una. Nessuna conseguenza pratica immediata per il progetto di un'ala o per una previsione meteorologica, molte conseguenze su quanto poco capiamo della turbolenza.

Nel 1934 Jean Leray dimostrò che soluzioni esistono sempre, in un senso generalizzato che oggi si chiama soluzione debole, ottenuto integrando l'equazione contro una funzione di prova e scaricando le derivate su quest'ultima. Da lì in avanti il programma è stato provare che ogni soluzione debole è in realtà liscia, e il programma si è fermato a metà. Fefferman ricorda che l'unicità delle soluzioni deboli di Navier-Stokes non è nota, e che per Euler è addirittura falsa. Il risultato migliore in direzione della regolarità resta il teorema di regolarità parziale di Caffarelli, Kohn e Nirenberg del 1982, che limita la dimensione dell'insieme singolare e, come scrive lo stesso Fefferman, sembra molto difficile da migliorare.

La viscosità è l'argomento a favore della regolarità. È il termine che diffonde, smussa, redistribuisce energia dalle scale piccole, e per decenni è sembrato abbastanza forte da impedire qualsiasi catastrofe. Diego Córdoba, dell'Instituto de Ciencias Matemáticas di Madrid, ha ricordato a Quanta Magazine che dieci anni fa nessuno credeva a una singolarità per Navier-Stokes, mentre molti la ritenevano plausibile per Euler.

Il ruolo del bordo

Nel 2013 Thomas Hou, del California Institute of Technology, e Guo Luo ottennero un risultato che cambiò il clima, mostrando un blowup per Euler dentro un cilindro con le due metà messe in rotazione opposta. Era il primo argomento serio a favore dell'esistenza di una singolarità, e infatti nei dieci anni successivi le tecniche assistite da calcolatore che Hou e Luo avevano usato sono diventate l'approccio dominante.

Il problema del millennio, però, vive nello spazio infinito senza pareti, e la differenza non è formale. Fefferman ha spiegato a Quanta che con un bordo la singolarità nasce dall'interazione del fluido con la parete, mentre senza bordo è il fluido a fare da solo la cosa strana.

La genealogia dell'idea, che passa da Madrid

La parte della vicenda che rischia di passare inosservata è quella che i protagonisti considerano decisiva, perché nessuna delle due dimostrazioni annunciate questa settimana parte da zero. Luis Martínez-Zoroa, oggi alla CUNEF Universidad, nella tesi di dottorato del 2021 ha messo a punto tecniche analitiche che non usano il calcolatore, in netta controtendenza rispetto al filone dominante fondato sulle simulazioni. Con Diego Córdoba, che era il suo relatore, nel 2023 ha dimostrato che una versione delle equazioni di Euler con una forzante irregolare sviluppa singolarità.

Il meccanismo, in forma essenziale, consiste nel costruire una successione infinita di strati, ognuno dei quali è una soluzione non singolare dell'equazione, e nel combinarli in quella che Martínez-Zoroa chiama una cascata infinita. La soluzione limite contiene la singolarità desiderata. Il prezzo era che, pur restando regolare ogni singolo strato, la loro somma produceva una forzante con proprietà brutte, e il criterio del Clay chiede invece una forzante liscia. Quel dislivello è la ragione per cui il risultato del 2023, pur essendo il vero salto concettuale, non chiudeva il problema del millennio.

Rendere liscia la forzante della soluzione limite era il gradino che mancava, ed è un gradino tecnico costruito sopra un'architettura che che né OpenAI né Buckmaster e Alpöge rivendicano come propria. Tristan Buckmaster, che quel passo lo ha compiuto con Alpöge sulle equazioni di Euler tridimensionali, lo mette per iscritto nella dichiarazione che accompagna la pubblicazione (quella resa pubblica dodici ore prima l'annuncio di OpenAI), dove precisa che il programma non è stato avviato da lui né proposto da un modello linguistico e che il merito dell'idea di base va a Córdoba e Martínez-Zoroa. Nello stesso testo aggiunge, dicendo di ripetere in pubblico quello che aveva già detto in privato ai colleghi, di ritenere che Martínez-Zoroa meriti una medaglia Fields.

La valutazione non è isolata. Fefferman, interpellato da Quanta Magazine, ha indicato i due spagnoli come i veri protagonisti della storia. Córdoba, alla stessa rivista, ha ripetuto una sua battuta ricorrente sul non aver bisogno dell'intelligenza artificiale perché ha Luis, mentre Martínez-Zoroa ha precisato di non essere ostile ai modelli, ma di non averli trovati compatibili con il proprio modo di lavorare, e di doversi ormai adattare. Sulla paternità delle idee le voci che contano dicono la stessa cosa, in un momento in cui tutto il resto della vicenda è contestato. Quello che i due gruppi hanno aggiunto è l'ultimo passo, e in entrambi i casi arriva accompagnato da un certificato prodotto da una macchina.

Che cosa certifica Lean e che cosa no

Entrambi i lavori arrivano con una formalizzazione in Lean, l'assistente di dimostrazione in cui ogni passaggio logico viene controllato dalla macchina. Il valore è reale e va detto con precisione. Lean garantisce che, date le ipotesi scritte nel file, la conclusione scritta nel file segue per deduzione, senza salti, senza passaggi lasciati al lettore. Elimina quasi del tutto la categoria di errore che ha affondato molte dimostrazioni lunghe nella storia recente della matematica. Quello che Lean non garantisce è che l'enunciato formalizzato sia lo stesso enunciato che interessa alla comunità. Il confronto fra la formula scritta nel file e la formulazione del Clay resta un lavoro umano, e non è un dettaglio burocratico.

Un esempio concreto rende l'idea. La formulazione di Fefferman impone alla forzante condizioni di decadimento precise su tutte le derivate, in spazio e in tempo. Se nella formalizzazione la classe di funzioni ammesse per la forzante fosse anche solo un po' più permissiva di quella, il file compilerebbe senza un errore e dimostrerebbe un teorema diverso da quello che il premio richiede. È qui che si concentra ogni dubbio residuo, e su questo aspetto è utile capire come funziona la verifica formale delle dimostrazioni matematiche prima di leggere qualsiasi titolo sul tema.

La vicenda dei crediti, raccontata con le attribuzioni

Su questa parte conviene distinguere i fatti documentati dalle versioni contrapposte. I fatti sono che Buckmaster e Levent Alpöge hanno reso pubblici tre risultati di blowup con forzante liscia, per l'equazione dei mezzi porosi incomprimibili, per Boussinesq e per Euler tridimensionale, tutti verificati in Lean, con la dichiarazione comparsa poco prima della mezzanotte del 7 settembre. Che OpenAI ha pubblicato il proprio risultato la mattina dell'8. Che nel suo comunicato OpenAI riconosce la priorità dell'altro gruppo sul caso di Euler forzato.

Il resto va attribuito. Secondo il racconto di OpenAI, lo sforzo è partito il primo settembre dopo aver sentito voci sulla risoluzione di due problemi del millennio, ha impiegato gruppi di agenti coordinati alimentati da un modello interno, con circa diecimila agenti in parallelo sul gruppo che ha prodotto il risultato, e si è chiuso il 5 settembre, con altre diciassette ore per la formalizzazione. L'azienda scrive che né i ricercatori né gli agenti hanno visto il lavoro dell'altro gruppo prima della pubblicazione, e che nessun dato utente specifico è stato consultato.

Secondo la dichiarazione di Buckmaster, il 3 settembre lui scrisse a un matematico di OpenAI per chiarire che la sua era una collaborazione personale, senza alcun coinvolgimento istituzionale dei rispettivi datori di lavoro. Le due telefonate si tennero il pomeriggio del 6 settembre, con Sébastien Bubeck presente e Alpöge assente. Sempre secondo la sua ricostruzione, nel corso della chiamata la descrizione iniziale di un risultato ottenuto con pochissimo intervento umano si sfaldò, perché emerse che a lavorare al problema c'era un intero gruppo, che i modelli erano stati prima messi su problemi più facili, che il prompt mostratogli era stato a sua volta scritto interrogando Codex, e che era stata usata una quantità enorme di calcolo. Buckmaster scrive di aver chiesto se il modello fosse stato addestrato sulle sue sessioni Codex, in cui aveva riversato tutte le bozze del progetto, e di non aver ricevuto risposta sulla parte relativa all'addestramento.

Nella stessa dichiarazione compaiono i due punti più contestati, ovvero che gli sia stato proposto di firmare da solo un articolo sul risultato di Navier-Stokes riconoscendo il modello interno, e che Bubeck avesse per due volte affermato di volere Alpöge fuori dall'autorialità per la sua affiliazione ad Anthropic. Buckmaster riferisce anche una frase sulla carriera, ricevuta dopo aver detto che avrebbe reso pubblica la vicenda. Nel suo testo precisa di non aver visto la dimostrazione di OpenAI e di non accusare nessuno di nulla, limitandosi a riportare cosa gli è stato detto e cosa gli è stato proposto.

Bubeck ha risposto pubblicamente definendo le accuse false, sostenendo di aver seguito le norme accademiche. In un intervento successivo ha pubblicato messaggi che a suo dire mostrano di aver proposto un annuncio coordinato, ha negato di aver chiesto la rimozione di Alpöge dall'autorialità del lavoro di Alpöge, spiegando che la discussione riguardava la riscrittura della dimostrazione di OpenAI, e si è scusato per la frase sulla carriera, definendola un'uscita infelice detta per frustrazione e ritirata subito. Sam Altman lo ha difeso, dicendo che Bubeck si è comportato con integrità. Su un punto la risposta dell'azienda resta condizionale, perché OpenAI scrive di non poter escludere che dati de-identificati derivanti dall'uso dei suoi prodotti abbiano contribuito a migliorare i modelli.

L'obiezione di Tao, che è la parte più interessante

Il 7 settembre Terence Tao, medaglia Fields nel 2006 e autore nel 2014 di un risultato di blowup per una versione mediata delle equazioni di Navier-Stokes, ha dedicato un post al lavoro di Alpöge e Buckmaster, non a quello di OpenAI, che allora non era ancora pubblico. Ha definito il risultato un progresso sostanziale su tre modelli semplificati, ha ricostruito il meccanismo delle correzioni ad alta frequenza aggiunte a una soluzione di fondo, e ha scritto una frase che vale più di tutta la cronaca. La risoluzione di questi problemi, per Tao, è soltanto un obiettivo di comodo, mentre l'obiettivo primario è sviluppare comprensione matematica. Senza quella comprensione, aggiunge, anche un problema famoso come la regolarità di Navier-Stokes ha un'importanza intrinseca molto inferiore a quella che la stampa divulgativa gli attribuisce.

La conseguenza è ruvida. Una dimostrazione corretta prodotta da un processo opaco vale, dal punto di vista matematico, molto meno di quanto suggerisca il titolo di giornale, perché il valore di un risultato sta nell'idea che gli altri possono assimilare e riusare. Tao ha raccontato di aver capito il nucleo del lavoro grazie a una telefonata di mezz'ora con Buckmaster e, in una nota sui social, ha osservato con ironia quanto gli sia sembrato riposante il ritorno a una modalità di comunicazione non mediata dall'intelligenza artificiale.

Buckmaster arriva a una conclusione vicina per strade diverse. Nella sua dichiarazione scrive di aver progettato di dire, annunciando il lavoro, che i risultati non sono la cosa importante, e che conta invece il fatto che un matematico e un modello possano oggi fare tutto quel lavoro in un mese. La ricaduta riguarda il modo in cui si formano i dottorandi, si assegnano i crediti, si arbitrano gli articoli e si decide a cosa vale la pena dedicare una vita di lavoro. Un revisore a cui arriva un manoscritto di oltre cento pagine generato da un modello e accompagnato da un certificato Lean si trova davanti a un compito nuovo, perché il controllo dei passaggi è già fatto e quello che resta da fare è capire se l'enunciato è quello giusto e se l'argomento insegna qualcosa. Su questo la discussione è appena cominciata, e vale la pena seguirla a quanto sta cambiando nel rapporto fra matematica e modelli linguistici.

Cosa resta da verificare

Due elementi in coda meritano attenzione perché indicano dove guardare nelle prossime settimane. Il primo lo segnala Buckmaster stesso, che dichiara di ritenere di avere anche un blowup per una Navier-Stokes ipodissipativa, cioè con viscosità più debole di quella standard, e di non aver pubblicato quel lavoro perché la verifica in Lean non era conclusa. Lo menziona perché suggerisce una strada verso Euler non forzato. Il secondo è un preprint indipendente di Ganeshram, Duruisseaux e Anandkumar, uscito il 7 settembre, che avanza sull'altro approccio storico, quello che cerca prima un profilo autosimile con strumenti numerici e poi ne dimostra la stabilità. Tao lo ha segnalato come un progresso significativo, precisando che stabilire la stabilità entro la tolleranza dell'errore residuo resta un compito molto difficile.

Restano aperte, alla data di scrittura, la verifica indipendente della corrispondenza fra l'enunciato formalizzato e la formulazione del Clay, la revisione paritaria, e la ricostruzione precisa delle cronologie. La pagina del Clay Mathematics Institute continua a elencare Navier-Stokes fra i problemi non risolti. Ultimo aggiornamento 9 settembre 2026.

Domande frequenti

Le equazioni di Navier-Stokes sono state risolte davvero?

OpenAI ha pubblicato l'8 settembre 2026 una dimostrazione di singolarità in tempo finito con forza esterna liscia, che corrisponde alle alternative C e D dell'enunciato ufficiale. Secondo le regole del Clay basta una delle quattro, quindi la rivendicazione è pertinente, ma mancano ancora revisione paritaria e accettazione della comunità matematica.

Che differenza c'è fra il caso forzato e quello non forzato in Navier-Stokes?

Nel caso forzato il matematico può progettare una forza esterna, purché resti regolare, che spinge il fluido verso la catastrofe. Nel caso non forzato il fluido parte da un dato iniziale liscio e nessuno lo tocca più. La seconda situazione è quella fisicamente interessante e resta completamente aperta.

Chi vince il milione di dollari del Millennium Prize per Navier-Stokes?

Nessuno, almeno per ora. OpenAI ha dichiarato di non voler rivendicare il premio. Il regolamento del Clay Mathematics Institute non ammette candidature dirette e pretende tre condizioni congiunte, cioè pubblicazione con revisione paritaria, almeno due anni trascorsi e accettazione generale nella comunità matematica mondiale.

Cosa garantisce la verifica in Lean di una dimostrazione matematica?

Lean controlla che ogni passaggio logico segua dalle ipotesi scritte nel file, eliminando la possibilità di errori nascosti in una catena di ragionamenti lunga. Non verifica invece che quell'enunciato formale coincida con il problema che i matematici volevano risolvere, e quel confronto resta un lavoro umano da fare a mano.

Perché Córdoba e Martínez-Zoroa sono centrali in questa storia di Navier-Stokes?

Perché l'idea di base delle nuove dimostrazioni è loro. Con tecniche analitiche senza calcolatore hanno costruito cascate infinite di strati che producono una singolarità, arrivando nel 2023 al blowup per Euler con forzante irregolare. Buckmaster attribuisce esplicitamente a loro il merito del programma e indica Martínez-Zoroa per una medaglia Fields.