Navier-Stokes, l’intelligenza artificiale e una prova che deve ancora convincere i matematici

Un milione di dollari per ciascuno di sette problemi matematici tra i più profondi del nostro tempo. È la sfida lanciata nel 2000 dal Clay Mathematics Institute con i Millennium Prize Problems. Finora soltanto uno, la congettura di Poincaré, è stato risolto e riconosciuto ufficialmente. Tra i sei ancora aperti figura il problema dell’esistenza e regolarità delle soluzioni delle equazioni di Navier-Stokes, fondamentali per descrivere il moto dei fluidi.

Il 9 settembre, OpenAI ha comunicato che un proprio sistema di intelligenza artificiale abbia prodotto una dimostrazione capace di chiudere il problema. L’azienda ha pubblicato un testo matematico e una formalizzazione in Lean, un software che controlla la correttezza logica di una dimostrazione. È un annuncio potenzialmente storico, ma non ancora un verdetto: una prova formalizzata può escludere molti errori logici, purché enunciati e formalizzazione siano corretti, ma non sostituisce l’esame della comunità matematica. E le regole del Clay Mathematics Institute sono esplicite: una soluzione deve apparire in una sede scientifica qualificata, devono trascorrere almeno due anni dalla pubblicazione e il risultato deve ottenere un’accettazione generale prima che l’Istituto possa prenderlo in considerazione.

La cautela è tanto più necessaria perché all’annuncio si accompagna una controversia sulla genesi della prova e sull’attribuzione del lavoro. Al centro della vicenda ci sono Tristan Buckmaster, matematico della New York University, e Levent Alpöge, matematico che lavora per Anthropic. I loro risultati e quello rivendicato da OpenAI sono collegati, ma non coincidono.

Ma facciamo un passo indietro: che cosa sono le equazioni di Navier-Stokes? Sono uno dei più importanti strumenti della fisica matematica. Descrivono il comportamento dei fluidi, cioè dei liquidi e dei gas e ci aiutano a capire come si formano i vortici nell’acqua, perché un aereo riesce a volare, come si muovono le correnti oceaniche o come il sangue scorre nelle arterie. 

Il principio su cui si basano è semplice: anche una piccola porzione di fluido obbedisce alla seconda legge di Newton e il suo movimento cambia in risposta alle forze che agiscono su di essa. In tre dimensioni, la formula vettoriale del moto corrisponde a tre equazioni, una per ciascuna direzione dello spazio. A queste si aggiunge l’equazione di continuità, che garantisce la conservazione della massa. 

Le equazioni di Navier-Stokes formano dunque un sistema matematico che tiene conto della velocità e dell’accelerazione del fluido, della pressione, della viscosità – cioè dell’attrito interno – e di forze esterne come la gravità.

La loro storia inizia nel Settecento, quando Leonhard Euler formula un modello per fluidi ideali, privi di viscosità. Nel 1822 Claude-Louis Navier introduce l’effetto dell’attrito interno; alcuni decenni dopo George Gabriel Stokes sviluppa il modello nella forma che oggi conosciamo. Da allora, queste equazioni sono diventate fondamentali in meteorologia, aeronautica, oceanografia, medicina e ingegneria. Eppure, nascondono ancora un grande mistero: nel caso tridimensionale non sappiamo dimostrare che, partendo da condizioni iniziali regolari, le soluzioni rimangono sempre regolari. Non è noto, cioè, se velocità e vortici possano crescere senza limite in un tempo finito, creando una singolarità, oppure se ciò sia impossibile. Questa incertezza non impedisce di usarle: grazie ai computer possiamo ottenere ottime soluzioni approssimate in moltissimi casi concreta. 

Una dimostrazione matematica generale, però, continua a mancare e il problema dell’esistenza e della regolarità delle loro soluzioni è ancora uno dei sette Problemi del Millennio scelti dal Clay Mathematics Institute. 

In una dichiarazione pubblica, Buckmaster ha annunciato con Alpöge tre risultati di blow-up in tempo finito con forzante liscia: uno per le equazioni dei mezzi porosi incomprimibili, uno per il sistema di Boussinesq e uno per le equazioni di Eulero tridimensionali incomprimibili (in questo contesto, blow-up significa che una soluzione inizialmente regolare sviluppa una singolarità dopo un intervallo di tempo finito).

Questi risultati sono importanti e riguardano sistemi strettamente legati alla dinamica dei fluidi, ma non risolvono di per sé il problema del Millennio sulle equazioni di Navier-Stokes. Buckmaster e Alpöge affermano inoltre di avere ottenuto un blow-up per una versione ipodissipativa di Navier-Stokes, nella quale la dissipazione è più debole rispetto alle equazioni classiche. Al momento della dichiarazione, tuttavia, la verifica in Lean non era terminata e gli autori non disponevano ancora di un manoscritto presentabile.

Secondo Buckmaster, il programma di ricerca non è nato da un modello linguistico. Il punto di partenza è il lavoro di Diego Córdoba e Luis Martínez-Zoroa sui blow-up prodotti da forzanti poco regolari. Buckmaster e Alpöge dichiarano di aver esteso quella strategia a forzanti lisce e ad altri sistemi, ricorrendo ampiamente a modelli di Anthropic e OpenAI per sviluppare, controllare e formalizzare le dimostrazioni. Nella sua ricostruzione, il progresso decisivo sulle equazioni di Boussinesq ed Eulero sarebbe avvenuto il 15 agosto, con la verifica formale del risultato su Euler completata il 22 agosto.

La rivendicazione di OpenAI è diversa e più ambiziosa. L’azienda afferma che un proprio sistema interno abbia invece costruito un controesempio per le equazioni classiche di Navier-Stokes tridimensionali con una forza esterna liscia, mostrando la formazione di una singolarità in tempo finito. Se la prova superasse l’esame degli specialisti, sarebbe dunque sufficiente a risolvere il problema.

OpenAI riferisce di aver impiegato un sistema composto da circa 10000 agenti, ai quali sono state assegnate diverse varianti del quesito. Secondo il resoconto pubblicato dall’azienda, la ricerca avrebbe richiesto circa 88 ore e la formalizzazione in Lean altre 17. L’azienda sostiene che il modello responsabile del risultato sia un sistema interno più avanzato di GPT-6 Astra e dichiara di non voler concorrere per il premio da un milione di dollari.

La vicinanza temporale tra le due linee di ricerca ha innescato uno scontro. Buckmaster racconta che, dopo la diffusione di indiscrezioni sui risultati ottenuti con Alpöge, OpenAI gli avrebbe comunicato di possedere una prova di blow-up per Navier-Stokes con forzante liscia. Il matematico sostiene che, durante successive conversazioni, sarebbe emerso un contributo umano e organizzativo più ampio di quanto inizialmente lasciato intendere: un gruppo di ricerca avrebbe selezionato problemi intermedi, orientato gli agenti e impiegato una quantità eccezionale di calcolo.

Buckmaster riferisce inoltre che Sébastien Bubeck, ricercatore di OpenAI, avrebbe proposto una pubblicazione coordinata e, in una delle ipotesi discusse, un articolo sul risultato Navier–Stokes firmato dal solo Buckmaster, escludendo Alpöge perché dipendente di Anthropic. Racconta anche di aver ricevuto risposte intimidatorie quando prospettò di rendere pubblica la vicenda. Sono affermazioni contenute nella dichiarazione del matematico e devono essere presentate come tali, non come fatti stabiliti da una verifica indipendente.

Il punto più sensibile riguarda i dati. Buckmaster e Alpöge avevano caricato bozze e materiali del progetto nelle sessioni di Codex. Buckmaster afferma di aver chiesto se il nuovo sistema avesse avuto accesso a quelle conversazioni o fosse stato addestrato su di esse senza ricevere, sul momento, una risposta soddisfacente. OpenAI replica che né i ricercatori né gli agenti avrebbero consultato il loro lavoro prima della pubblicazione. L’azienda aggiunge però di non poter escludere del tutto che dati de-identificati derivati dall’uso dei suoi prodotti abbiano contribuito indirettamente al miglioramento dei modelli.

Questa ammissione non dimostra che le idee dei due matematici siano state impiegate per ottenere la nuova prova. Evidenzia tuttavia un problema destinato a diventare centrale: quando uno scienziato affida a un sistema commerciale bozze, calcoli e intuizioni non pubblicate, quali garanzie ha sulla riservatezza, sull’addestramento dei modelli e sulla priorità intellettuale? Le consuete regole accademiche sull’attribuzione si adattano con difficoltà a strumenti che possono assistere migliaia di ricercatori e, nello stesso tempo, migliorare grazie ai dati generati dal loro utilizzo.

Al momento (10 settembre 2026) esiste una dimostrazione pubblica rivendicata da OpenAI, accompagnata da una formalizzazione in Lean. Questo la rende esaminabile e le conferisce un peso ben diverso da quello di un semplice annuncio promozionale. Non significa però che il problema sia già ufficialmente risolto. Gli specialisti devono controllare che la costruzione soddisfi esattamente le ipotesi formulate dal Clay Mathematics Institute, che non vi siano discrepanze tra il testo e il codice formale e che gli assiomi e le definizioni adottati in Lean rappresentino correttamente il problema matematico.

È prematuro anche parlare di ricadute industriali immediate. Le equazioni di Navier-Stokes sono indispensabili in aerodinamica, meteorologia, ingegneria e fisiologia, ma la soluzione del problema di regolarità è anzitutto un risultato di matematica pura: non produce automaticamente simulatori più veloci, previsioni meteorologiche migliori o nuovi progetti di turbine. Il suo impatto applicativo dipenderà dalle tecniche introdotte dalla prova e dalla possibilità di trasferirle al calcolo scientifico.

Il significato più immediato potrebbe trovarsi altrove. Se il risultato sarà confermato, avremo una delle dimostrazioni più impressionanti della capacità dei sistemi di intelligenza artificiale di contribuire alla ricerca matematica di frontiera. Ma la vicenda mostra anche che “l’AI ha risolto il problema” è una formula troppo semplice. Dietro la prova compaiono idee sviluppate in anni di lavoro umano, scelte di ricercatori, infrastrutture di calcolo, strumenti di verifica formale e migliaia di processi coordinati.

Buckmaster ha evocato la vittoria di Deep Blue sul campione di scacchi Garry Kasparov nel 1997. Il paragone coglie la portata simbolica dell’evento, ma la matematica non è una partita con un risultato immediatamente leggibile sulla scacchiera. Una nuova dimostrazione deve essere compresa, controllata e inserita nella storia delle idee da cui discende. Prima di proclamare un vincitore, che sia umano o artificiale, occorre sapere se la prova è corretta e ricostruire con precisione chi, o che cosa, l’ha resa possibile.