OpenAI: un modello di intelligenza artificiale avrebbe risolto Navier-Stokes

Un modello di OpenAI sembra aver affrontato Navier-Stokes, ma tra vortici, singolarità e formalizzazione in Lean restano dubbi su metodo, paternità e verifica: la matematica umana conserva un ruolo decisivo.

OpenAI ha annunciato il 9 settembre 2026 che un modello interno, non ancora disponibile al pubblico, avrebbe risolto il problema dellesistenza e della regolarit delle equazioni di Navier-Stokes. Il lavoro sarebbe stato completato in circa 88 ore, con il coinvolgimento di un numero massimo di 10.000 agenti artificiali e costi di calcolo stimati in milioni di dollari. Lazienda ha parlato di una possibile dimostrazione di singolarit. Questo, per, non equivale ancora a una soluzione riconosciuta dal Clay Mathematics Institute o dalla comunit matematica.

La distinzione pesa. OpenAI afferma di avere prodotto una prova teorica accompagnata da una formalizzazione in Lean, il linguaggio impiegato per controllare automaticamente i passaggi logici. Prima di poter parlare di soluzione accettata, la matematica richiede per una valutazione indipendente: il testo deve essere leggibile, verificabile da specialisti e sottoposto alla procedura prevista per uno dei sette Problemi del Millennio.

Che cosa ha annunciato OpenAI

Il progetto cominciato dopo laddestramento, avviato alla fine di agosto 2026, di un modello pi capace rispetto ai sistemi resi pubblici fino a quel momento. OpenAI non lo ha presentato come un prodotto per gli utenti. Nelle descrizioni dellazienda si tratta di un sistema interno, progettato anche per coordinare agenti specializzati.

Il lavoro matematico sarebbe partito il primo settembre 2026. Gli agenti sono stati applicati ai Problemi del Millennio ancora aperti e ad altri quesiti collegati. Allinizio si sono concentrati sulle equazioni di Eulero, una versione semplificata di Navier-Stokes nella quale la viscosit viene trascurata.

Circa 100 agenti avrebbero lavorato per quasi 50 ore, ottenendo progressi che sarebbero poi serviti alle fasi successive. Per Navier-Stokes il gruppo stato ampliato fino a circa 10.000 copie del modello. Operavano in parallelo: formulavano ipotesi, eseguivano codice, confrontavano gli esiti e passavano agli altri gruppi le idee considerate pi promettenti.

La soluzione sarebbe arrivata il 5 settembre 2026, dopo circa 88 ore di lavoro continuo. Il resoconto parla di 2,7 milioni di messaggi scambiati e di circa 130 miliardi di token prodotti sul problema.

Sbastien Bubeck, responsabile del gruppo matematico di OpenAI, ha stimato in diversi milioni di dollari la spesa complessiva per il calcolo. Mark Chen, responsabile della ricerca dellazienda, ha descritto il risultato come un traguardo per la ricerca sullintelligenza artificiale. Secondo Chen, il costo sarebbe stato circa mille volte superiore a quello di precedenti risultati matematici interni.

Il problema matematico ancora aperto

Le equazioni di Navier-Stokes furono sviluppate nellOttocento a partire dai lavori dellingegnere francese Claude-Louis Navier e del matematico e fisico irlandese George Gabriel Stokes. Rappresentano il fluido come un mezzo continuo e applicano alla sua dinamica principi legati alla seconda legge di Newton.

Detto in modo semplice, collegano grandezze come velocit, pressione, densit e viscosit alla posizione e al tempo. Servono a modellare lacqua, laria e altri fluidi. Le applicazioni comprendono la progettazione degli aerei, le previsioni meteorologiche, lo studio del flusso sanguigno e lanalisi di processi industriali.

Lutilit pratica delle equazioni non significa che ogni loro propriet matematica sia gi stata dimostrata. La domanda posta dal Clay Mathematics Institute riguarda il caso tridimensionale di un fluido incomprimibile. Dati iniziali regolari e una forza esterna regolare garantiscono che la soluzione rimanga liscia per ogni istante, oppure il sistema pu sviluppare una singolarit in un tempo finito?

Una soluzione regolare non contiene valori destinati a diventare improvvisamente illimitati. Una singolarit sarebbe invece un punto nel quale una quantit, per esempio la velocit, cresce senza limite secondo il modello matematico. In una situazione del genere la descrizione continua del fluido smetterebbe di rappresentare una condizione fisica reale: un fluido materiale non pu raggiungere una velocit infinita.

Il quesito non consiste nel calcolare il movimento di un liquido in una situazione quotidiana. Chiede se le equazioni ammettano sempre una soluzione regolare oppure se la loro struttura possa produrre unesplosione, indicata spesso con il termine inglese blow-up. Una simulazione numerica, anche molto dettagliata, non pu quindi dimostrare da sola un enunciato generale.

Il vortice che dovrebbe produrre la singolarit

La costruzione attribuita a OpenAI parte da un fluido inizialmente fermo. Una forza esterna liscia, dunque regolare secondo i requisiti matematici del problema, mette in movimento il sistema. Si forma un vortice che si avvolge verso linterno, si allunga e concentra il moto in una regione sempre pi piccola.

Stando alla descrizione resa pubblica, la velocit cresce senza limite mentre lenergia rimane finita. Limmagine quella di una spirale che si stringe e si prolunga, senza violare i vincoli richiesti dalla formulazione matematica. La tesi sarebbe dunque lesistenza di condizioni iniziali e forze esterne regolari capaci di condurre Navier-Stokes a una singolarit.

La precisazione serve a delimitare il risultato. La forza esterna costruita appositamente per ottenere il fenomeno. OpenAI non ha sostenuto che laria intorno a un aereo, lacqua di un fiume o il fluido di una turbina sviluppino spontaneamente la stessa instabilit.

Se corretta, la dimostrazione risponderebbe alla domanda matematica nella forma prevista dal premio. Non descriverebbe, invece, un evento osservabile nella vita quotidiana.

Perch Navier-Stokes un Problema del Millennio

Alla fine del Novecento il Clay Mathematics Institute, organizzazione dedicata alla ricerca matematica, selezion sette problemi considerati tra i pi difficili e influenti. Lelenco fu presentato nel 2000 e riprendeva la tradizione della lista di problemi proposta da David Hilbert nel 1900.

Per ciascun problema previsto un premio di un milione di dollari. Il riconoscimento economico, per, dipende da condizioni precise: la soluzione deve essere pubblicata in una sede qualificata, devono trascorrere almeno due anni e la comunit matematica internazionale deve arrivare a unaccettazione generale. Il Clay Institute continua a classificare Navier-Stokes come non risolto.

Tra i sette problemi, lunico riconosciuto ufficialmente come risolto la congettura di Poincar. Grigori Perelman ne forn la dimostrazione tra il 2002 e il 2003; il riconoscimento formale da parte del Clay Institute arriv nel 2010. Il matematico russo rifiut il premio da un milione di dollari e nel 2006 aveva gi rifiutato la medaglia Fields.

OpenAI ha dichiarato che non reclamerebbe il milione di dollari anche se la prova di Navier-Stokes fosse convalidata. La rinuncia al denaro non cambia i criteri scientifici: il premio pu essere rifiutato, mentre la dimostrazione deve comunque essere controllata.

La formalizzazione in Lean: che cosa dimostra

OpenAI ha dichiarato di avere tradotto la dimostrazione in Lean e di averla fatta controllare da un altro modello in circa 17 ore. Lean un proof assistant, cio un sistema che permette di rappresentare definizioni e passaggi matematici in una forma verificabile da un computer.

Una formalizzazione riduce il rischio di alcuni errori logici e consente di controllare che le istruzioni inserite rispettino le regole del sistema. Non dimostra per, da sola, che ci che stato formalizzato coincida esattamente con lenunciato richiesto dal Clay Institute.

Restano da esaminare le ipotesi adottate, la scelta degli spazi matematici, la regolarit della forza esterna e il passaggio che porta alla singolarit. Anche la corrispondenza tra il problema ufficiale e la proposizione verificata deve essere accertata.

Controllo formale e comprensione matematica non sono la stessa cosa. Un verificatore pu confermare una catena di istruzioni formalizzate; gli specialisti devono ancora capire se quella catena dimostri davvero la proposizione in discussione. Devono anche escludere che siano state introdotte ipotesi pi forti di quelle ammesse o che siano state dimostrate proposizioni differenti.

In una prova lunga e tecnica, la leggibilit non un dettaglio. I ricercatori devono poter ricostruire lidea, confrontarla con la formulazione ufficiale e individuare i passaggi che richiedono nuovi lemmi o verifiche indipendenti.

Il metodo umano dietro lapproccio del forcing

La strategia indicata nella dimostrazione si collega al lavoro dei matematici Diego Crdoba, dellIstituto di scienze matematiche di Madrid, e Luis Martnez-Zoroa, dellUniversit CUNEF di Madrid. Il loro contributo riguarda un termine della formulazione: la forza esterna che mette in moto il fluido.

Molti approcci tendono a eliminare quel termine, ritenendolo irrilevante per la domanda studiata. Crdoba e Martnez-Zoroa hanno invece esaminato la possibilit di usarlo in modo controllato. La tecnica, chiamata forcing, costruisce una sequenza di strati regolari e li combina in una cascata capace di contenere il comportamento singolare.

Il lavoro era stato sviluppato nella tesi di dottorato di Martnez-Zoroa, discussa nel 2021, con Crdoba come relatore. Nel 2023 i due avevano ottenuto un risultato su una versione delle equazioni di Eulero con una forza esterna non liscia.

La difficolt successiva consisteva nel conservare insieme la singolarit e una forza esterna regolare. questo il passaggio che rende il collegamento con il lavoro precedente particolarmente rilevante.

La paternit delle idee, per, non coincide automaticamente con chi produce per primo una prova completa. Un sistema artificiale pu avere trovato una combinazione nuova di strumenti, mentre il percorso concettuale pu dipendere da risultati umani precedenti, pubblici e riconoscibili.

Le accuse di Buckmaster e Alpge

La disputa pi delicata riguarda Tristan Buckmaster, professore di matematica alla New York University, e Levent Alpge, matematico che lavora per Anthropic. I due collaboravano da circa un anno su problemi collegati a Navier-Stokes e utilizzavano anche modelli di intelligenza artificiale.

Tra il 15 e il 22 agosto 2026 avrebbero ottenuto una dimostrazione relativa alle equazioni di Eulero, verificata in Lean prima del 22 agosto. Il testo esplicativo prodotto dai modelli non era ancora facilmente leggibile. I ricercatori lo stavano riscrivendo per renderlo comprensibile alla comunit.

Buckmaster sostiene che le informazioni sul loro lavoro siano arrivate a OpenAI allinizio di settembre 2026. Secondo la sua ricostruzione, il primo prompt utile per la dimostrazione di Navier-Stokes sarebbe stato inviato soltanto negli ultimi giorni, dopo la diffusione di quelle informazioni.

Per il matematico significativo che il sistema abbia seguito una direzione legata al forcing, cio una scelta elaborata dai due ricercatori nel loro progetto. La somiglianza, da sola, non dimostra per come le informazioni siano state ottenute.

Buckmaster ha posto anche una domanda sulle sessioni private svolte con Codex, un modello di OpenAI usato durante la ricerca. Ha chiesto se quelle conversazioni fossero state consultate oppure incluse nei dati di addestramento.

Il ricercatore afferma di non avere ricevuto una risposta completa sulla distinzione tra accesso diretto alle conversazioni e possibile uso, in forma anonima e aggregata, dei dati per migliorare i modelli.

La replica di OpenAI sulla paternit

OpenAI nega di avere usato i prompt o le dimostrazioni dei due matematici per indirizzare i propri agenti. Lazienda sostiene che n i ricercatori n i sistemi artificiali abbiano visto il loro lavoro prima della pubblicazione. Afferma inoltre che nessun dato utente specifico sia stato consultato per risolvere il problema.

La posizione dellazienda contiene per una precisazione. Non sarebbe possibile escludere in assoluto che conversazioni rese anonime e mescolate ad altri dati siano finite nei processi generali di addestramento o di miglioramento dei modelli.

OpenAI sostiene comunque che le dimostrazioni siano diverse. Anche i risultati sulle equazioni di Eulero non coinciderebbero: quello attribuito al sistema dellazienda sarebbe senza forza esterna, mentre il lavoro di Buckmaster e Alpge riguarderebbe una configurazione con forza esterna.

Secondo la versione di OpenAI, il contatto con i due matematici avvenuto il 6 settembre 2026, quando il lavoro era gi terminato. Lazienda avrebbe proposto una pubblicazione simultanea e il riconoscimento della loro priorit sul risultato relativo a Eulero con forza esterna.

Bubeck ha definito false e provocatorie le accuse rivolte al gruppo. Ha respinto lipotesi che i prompt privati abbiano guidato la prova.

Le due ricostruzioni non sono state risolte da una verifica indipendente. Occorre quindi distinguere laccusa di appropriazione del lavoro, che resta attribuita ai ricercatori, dalla negazione di OpenAI. N la tempistica dellannuncio n la somiglianza di un metodo stabiliscono, da sole, che vi sia stato accesso a dati privati.

Perch il riconoscimento umano resta centrale

La controversia non riguarda soltanto lordine degli autori. Coinvolge la provenienza delle idee, il modo in cui i modelli trattano i dati e le regole con cui la ricerca attribuisce il merito.

Roberto Natalini, direttore dellIstituto per le Applicazioni del Calcolo del Consiglio nazionale delle ricerche, ha avvertito che il timore di vedere intuizioni assorbite dai sistemi artificiali potrebbe ridurre la condivisione dei risultati prima della pubblicazione.

Una circolazione pi limitata delle idee danneggerebbe un meccanismo tradizionale della matematica: mettere rapidamente a confronto metodi, errori e progressi. La possibilit di discutere un risultato prima della sua pubblicazione ha infatti un peso concreto nel lavoro dei ricercatori.

Charles Fefferman, il matematico di Princeton che ha scritto la descrizione ufficiale del problema per il Clay Institute, ha mostrato interesse per il risultato. Ha per indicato Crdoba e Martnez-Zoroa come figure decisive per lidea del forcing.

Anche Martnez-Zoroa ha riconosciuto il valore della dimostrazione annunciata, osservando nello stesso tempo che sarebbe stato preferibile arrivarci direttamente con il proprio gruppo.

Una prova generata da agenti non cancella automaticamente i contributi precedenti. La valutazione dovr chiarire quali passaggi siano originali, quali dipendano da risultati gi noti e quale apporto abbiano avuto i ricercatori nella formulazione della strategia e nel controllo del risultato.

Che cosa cambia per le simulazioni dei fluidi

La conferma della prova non renderebbe automaticamente pi precise le previsioni meteorologiche e non ridurrebbe subito i consumi degli aerei. Le applicazioni industriali usano gi metodi numerici per approssimare le equazioni; il problema del Clay Institute, invece, teorico.

Una dimostrazione convalidata potrebbe per offrire un caso severo per mettere alla prova la computational fluid dynamics. I simulatori dividono lo spazio in una griglia e devono rappresentare vortici e strutture sempre pi piccole. Quando una configurazione concentra il moto in regioni che si restringono, il calcolo deve aumentare la risoluzione oppure accettare una perdita di dettaglio.

La configurazione proposta potrebbe servire a valutare il momento in cui un algoritmo numerico smette di seguire correttamente il fenomeno, il modo in cui distribuire la risoluzione e laffidabilit di un risultato in condizioni estreme.

Le possibili ricadute riguardano aerospazio, energia, turbine, processi chimici e dispositivi medici. Restano per programmi di ricerca, non effetti gi dimostrati dalla prova annunciata.

Il modello agentico come laboratorio parallelo

Laspetto tecnologico pi rilevante riguarda lorganizzazione del lavoro. OpenAI non ha affidato il problema a una singola risposta, ma a molte copie di un modello in grado di usare strumenti, eseguire codice e comunicare con gli altri agenti.

I gruppi hanno seguito strategie differenti, abbandonato le ipotesi deboli e trasferito le intuizioni pi utili a nuovi agenti. Il sistema assomiglia cos a un programma di ricerca distribuito, anche se la qualit del risultato dipende da come vengono selezionati e controllati i tentativi.

Gli esseri umani stabiliscono la domanda, i criteri di successo e la quantit di risorse. Gli agenti producono in parallelo un numero molto pi elevato di tentativi. Il vantaggio, quindi, non dipende soltanto dalla capacit del singolo modello, ma anche dalla selezione dei risultati e dal sistema che li verifica.

Lo stesso schema pu essere applicato a problemi meno estremi: progettare componenti, analizzare le cause di un guasto, generare patch software, confrontare configurazioni industriali o valutare ipotesi su processi chimici.

In ciascuno di questi casi il metodo funziona soltanto se il risultato pu essere misurato attraverso test, simulazioni o vincoli verificabili. Senza un criterio esterno, la quantit di tentativi non dice quanto valga la risposta finale.

La verifica decide il valore della promessa

Il caso Navier-Stokes mostra perch lautonomia degli agenti abbia bisogno di un arbitro esterno. In matematica questo ruolo pu essere svolto da una formalizzazione; nel software da una suite di test o da un compilatore; nellingegneria da un simulatore vincolato dalle leggi fisiche.

Senza controllo indipendente, migliaia di agenti producono soprattutto migliaia di testi da esaminare. Con un verificatore possibile eliminare rapidamente molte proposte e concentrare il lavoro umano su quelle che superano i controlli automatici.

Il numero di agenti, preso da solo, non misura il progresso. Servono ipotesi di qualit, conversazioni tracciabili, esperimenti riproducibili e una ricostruzione affidabile del percorso che ha portato alla conclusione.

La risposta alla domanda del titolo

OpenAI ha annunciato una possibile dimostrazione di singolarit per le equazioni tridimensionali di Navier-Stokes, ottenuta con un sistema agentico e formalizzata in Lean. Il risultato non per ancora una soluzione riconosciuta: la prova deve essere resa pubblica, esaminata da specialisti e confrontata con la formulazione ufficiale del Clay Mathematics Institute.

La verifica dovr stabilire se le ipotesi siano ammesse, se ogni passaggio sia corretto e se la configurazione con forza esterna regolare dimostri davvero lesistenza della singolarit richiesta dal problema. Anche lattribuzione dei contributi umani e leventuale uso di lavori precedenti restano da chiarire.

Fino al completamento di questo percorso, la definizione pi accurata risultato preliminare da verificare. Il caso mostra il potenziale dei sistemi agentici nella ricerca matematica, ma conferma anche che il valore di una prova dipende dal controllo indipendente, non dal numero di agenti o dalla quantit di calcolo impiegata.