OpenAI sostiene di aver risolto il problema di esistenza e regolarità delle equazioni di Navier-Stokes, uno dei sette Millennium Prize Problems del Clay Mathematics Institute. Ma l’annuncio dell’8 settembre 2026 è arrivato insieme a una disputa sulla priorità scientifica con Tristan Buckmaster, matematico della New York University, e Levent Alpöge, matematico che lavora per Anthropic.
La risposta alla domanda più immediata è questa: al 9 settembre 2026 il problema non può ancora essere considerato ufficialmente chiuso. OpenAI ha pubblicato una dimostrazione e una formalizzazione in Lean che, secondo l’azienda, soddisfano una delle formulazioni ammesse del problema del Millennio. Buckmaster e Alpöge hanno pubblicato risultati molto vicini per altre equazioni dei fluidi, ma non una soluzione completa di Navier-Stokes. La prova di OpenAI deve ancora essere verificata indipendentemente e non è stata riconosciuta dal Clay Mathematics Institute.
Che cosa ha annunciato OpenAI su Navier-Stokes
Nella pubblicazione ufficiale dedicata a Navier-Stokes, OpenAI afferma che un proprio sistema interno di ricerca matematica ha costruito una dimostrazione per una delle formulazioni previste dal problema del Millennio. Il risultato mostra che le equazioni tridimensionali incomprimibili possono sviluppare una singolarità in tempo finito in presenza di una forza esterna liscia opportunamente costruita.
OpenAI racconta di aver avviato il test sui Problemi del Millennio il 1° settembre, dopo aver sentito voci secondo cui altri ricercatori avrebbero ottenuto risultati importanti. Gli agenti avrebbero raggiunto la costruzione decisiva il 5 settembre, circa 88 ore dopo l’avvio. La formalizzazione e la verifica in Lean avrebbero richiesto altre 17 ore.
Il sistema usato non è il normale ChatGPT. OpenAI parla di un modello interno più capace di GPT-6 Astra e di gruppi coordinati fino a circa 10.000 agenti contemporanei. Per il tentativo Navier-Stokes l’azienda dichiara circa 2,7 milioni di messaggi e 130 miliardi di token di output.
Perché il risultato può valere come soluzione del problema del Millennio
Qui c’è un dettaglio che molti titoli stanno semplificando. Il problema del Millennio non chiede soltanto di dimostrare che le soluzioni di Navier-Stokes restano sempre regolari. La formulazione ufficiale consente anche la strada opposta: costruire condizioni iniziali e una forza esterna sufficientemente regolari per cui non esista una soluzione liscia globale.
È proprio questa la strada rivendicata da OpenAI. Se la dimostrazione soddisfa tutte le condizioni matematiche richieste, mostrare una rottura in tempo finito con forcing liscio sarebbe sufficiente a rispondere al problema nella forma prevista dal Clay Mathematics Institute.
Questo non significa che un fluido reale debba raggiungere velocità infinite. Una singolarità è un comportamento del modello matematico: indica che, nelle condizioni costruite dalla prova, una quantità perde regolarità in tempo finito. È una questione sulla struttura delle equazioni, non una previsione secondo cui acqua o aria possano letteralmente accelerare senza limite.
Da dove nasce la disputa con Buckmaster e Alpöge
Tristan Buckmaster e Levent Alpöge lavoravano da circa un anno su una strategia collegata alla formazione di singolarità nelle equazioni dei fluidi. Alpöge è dipendente di Anthropic, ma il lavoro descritto dai due ricercatori non viene presentato come un progetto ufficiale dell’azienda. La coppia ha usato sia Claude sia Codex come strumenti di ricerca.
Il 15 agosto i due avrebbero raggiunto un passaggio importante e in seguito hanno completato risultati di blow-up con forcing liscio per tre sistemi correlati: Euler tridimensionale, Boussinesq bidimensionale e incompressible porous media. Questi risultati sono importanti, ma non equivalgono alla soluzione completa del problema di Navier-Stokes.
Nella sua dichiarazione pubblica, Buckmaster sostiene che il percorso scelto dal sistema di OpenAI fosse insolitamente vicino alla linea di ricerca che lui e Alpöge stavano seguendo. La sua contestazione non riguarda soltanto chi abbia scritto per primo una dimostrazione, ma anche come OpenAI sia arrivata a scegliere quella specifica strada matematica.
L’accusa più delicata: OpenAI poteva conoscere il lavoro privato?
Buckmaster afferma di aver chiesto a OpenAI se le sessioni dei ricercatori con Codex potessero aver contribuito al sistema interno che poi ha prodotto la prova. È un punto centrale perché i due matematici avevano usato strumenti OpenAI durante il lavoro e non avevano ancora pubblicato integralmente i risultati quando la corsa alla soluzione è partita.
OpenAI nega che i propri ricercatori o agenti abbiano avuto accesso al lavoro specifico di Buckmaster e Alpöge. Nella ricostruzione ufficiale l’azienda afferma che non sono stati consultati prompt, dimostrazioni o dati utente specifici per indirizzare il sistema verso la soluzione.
C’è però una precisazione significativa nella stessa posizione di OpenAI: l’azienda dice di non poter escludere completamente che dati de-identificati derivati dall’uso dei suoi prodotti possano avere contribuito in passato al miglioramento generale dei modelli. Questo non dimostra che il lavoro privato dei due ricercatori sia stato usato per risolvere Navier-Stokes, ma rende la questione dell’attribuzione più delicata di una normale disputa accademica.
La controversia sull’autorialità e il ruolo di Anthropic
Secondo Buckmaster, durante i contatti successivi OpenAI avrebbe proposto una pubblicazione coordinata e, in una delle ipotesi discusse, avrebbe chiesto che Alpöge non figurasse come autore del lavoro Navier-Stokes. Buckmaster collega questa richiesta al fatto che il collega lavora per Anthropic e riferisce anche frasi che ha interpretato come pressioni sulla propria carriera.
Si tratta di accuse formulate da Buckmaster e contestate da OpenAI. OpenAI sostiene invece di aver cercato una soluzione che riconoscesse la priorità del lavoro umano precedente e afferma che la propria prova è stata ottenuta indipendentemente. Il punto importante, per chi legge, è non trasformare una disputa ancora aperta in un fatto già accertato.
Chi ha risolto Navier-Stokes, allora?
Al momento bisogna separare tre piani.
- OpenAI rivendica una soluzione completa di una formulazione ammessa del problema di Navier-Stokes e ha pubblicato sia il testo della prova sia una formalizzazione in Lean.
- Buckmaster e Alpöge hanno pubblicato risultati correlati che sviluppano una strategia di blow-up con forcing liscio, ma non hanno presentato una soluzione completa del problema di Navier-Stokes.
- Il Clay Mathematics Institute non ha ancora riconosciuto ufficialmente il problema come risolto e la comunità matematica non ha ancora completato una verifica indipendente della dimostrazione di OpenAI.
Per questo, scrivere oggi che “OpenAI ha vinto il milione” o che “Anthropic ha risolto Navier-Stokes” sarebbe prematuro. La formulazione più corretta è che OpenAI ha pubblicato una soluzione candidata estremamente rilevante, mentre una disputa sulla priorità e sulla provenienza delle idee resta aperta.
Che cosa dimostra Lean e che cosa non dimostra
Lean è un proof assistant: traduce definizioni e passaggi logici in una forma che un computer può controllare meccanicamente. Una formalizzazione accettata dal kernel di Lean offre una garanzia molto forte sulla coerenza dei passaggi codificati.
Non sostituisce però il controllo scientifico sul significato della formalizzazione. I matematici devono verificare che le definizioni usate corrispondano esattamente al problema del Clay, che le ipotesi siano quelle ammesse e che non ci siano discrepanze tra il testo informale e la prova formalizzata.
È la stessa distinzione che abbiamo già evidenziato parlando di turbolenza e modelli numerici complessi: una verifica computazionale può essere molto forte senza trasformare automaticamente una costruzione matematica in un risultato scientifico già assimilato dalla comunità.
Perché questa storia conta anche oltre la matematica
Se la prova verrà confermata, il risultato sarebbe importante non solo per Navier-Stokes. Mostrerebbe che sistemi AI coordinati possono esplorare strategie matematiche, costruire dimostrazioni molto lunghe e formalizzarle in un proof assistant a un livello finora associato a gruppi di specialisti.
Il caso apre però una seconda questione: cosa succede quando gli scienziati usano modelli commerciali per sviluppare idee non ancora pubblicate e il fornitore del modello sta lavorando sullo stesso problema? La disputa tra OpenAI, Buckmaster e Alpöge mostra che privacy dei dati, attribuzione, priorità scientifica e trasparenza dei sistemi AI stanno diventando parte del metodo di ricerca, non semplici temi contrattuali.
Il confronto con GPT-6 Astra aiuta anche a capire la scala dell’esperimento: il risultato non nasce da una singola risposta di un chatbot, ma da un’infrastruttura specializzata con migliaia di agenti, enormi quantità di calcolo e una fase separata di formalizzazione.
Cosa bisogna aspettare adesso
Il prossimo passaggio non sarà un altro annuncio aziendale, ma la verifica da parte di matematici indipendenti. Dovranno controllare la corrispondenza tra la prova, la formalizzazione Lean e le condizioni previste dal problema del Millennio.
Solo dopo questo processo si potrà stabilire se Navier-Stokes sia stato effettivamente risolto nella forma richiesta. La disputa sull’attribuzione seguirà invece un percorso separato: la correttezza matematica della prova e la questione su chi debba ricevere il merito sono due problemi distinti, entrambi ancora aperti al controllo pubblico.
