OpenAI sostiene di aver trovato una soluzione al problema di esistenza e regolarità delle equazioni di Navier-Stokes in tre dimensioni, uno dei Millennium Prize Problems. La parte importante, però, è capire cosa significa esattamente: il risultato pubblicato l’8 settembre 2026 descrive una soluzione liscia che, sotto una forza esterna liscia, sviluppa una singolarità in tempo finito. OpenAI ha anche prodotto una formalizzazione in Lean, ma questo non equivale ancora all’accettazione indipendente del risultato da parte della comunità matematica o del Clay Mathematics Institute.
È quindi corretto parlare di una rivendicazione matematica molto rilevante e formalmente verificata nel sistema descritto da OpenAI, non di un premio già assegnato o di un caso definitivamente chiuso. La distinzione è fondamentale, perché qui non si discute solo della capacità di un modello AI di produrre una dimostrazione, ma della validità di una prova su uno dei problemi più difficili della matematica moderna.
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 il caso tridimensionale incomprimibile. Il sistema ha lavorato in parallelo con circa 10.000 agenti e ha prodotto sia un testo matematico sia una formalizzazione verificabile con Lean.
Secondo OpenAI, il lavoro è iniziato il 1° settembre e il nucleo della soluzione è emerso il 5 settembre, dopo circa 88 ore. La formalizzazione e la verifica in Lean hanno richiesto altre 17 ore. L’azienda indica circa 2,7 milioni di messaggi e circa 130 miliardi di token di output per il solo tentativo dedicato a Navier-Stokes.
Il punto decisivo: una singolarità in tempo finito
Le equazioni di Navier-Stokes descrivono il moto dei fluidi, dall’acqua nell’oceano all’aria attorno a un’ala. In tre dimensioni sappiamo che funzionano molto bene come modello fisico, ma resta una domanda matematica profonda: partendo da condizioni iniziali regolari, la soluzione resta sempre regolare oppure può diventare infinita in un tempo finito?
Il risultato proposto da OpenAI segue la seconda strada. La costruzione parte da un fluido inizialmente fermo e introduce una forza esterna liscia e a energia finita. Il meccanismo descritto genera un vortice che si concentra verso l’interno mentre viene stirato lungo il proprio asse. Nel modello, la velocità cresce senza limite in un tempo finito pur mantenendo finita l’energia totale.
È un dettaglio essenziale. Non significa che un bicchiere d’acqua o una corrente d’aria reale debbano produrre velocità infinite. Una singolarità matematica indica invece che, nelle condizioni della costruzione, le equazioni consentono una perdita di regolarità. È proprio questo il tipo di questione posto dal problema del Millennio.
Che cosa c’entra Lean e perché non basta da solo
Lean è un proof assistant: un sistema che permette di esprimere definizioni e passaggi logici in una forma che il computer può controllare meccanicamente. Se una formalizzazione viene accettata dal kernel di Lean, significa che i passaggi formalizzati rispettano le regole logiche e le definizioni inserite nel sistema.
Questo riduce drasticamente il rischio di errori algebrici o salti logici nascosti. Non elimina però la necessità di una verifica scientifica indipendente. I matematici devono controllare che le definizioni formalizzate corrispondano esattamente al problema dichiarato, che non ci siano assunzioni improprie e che la costruzione soddisfi tutte le condizioni richieste.
È la stessa distinzione che vale in altri campi: una verifica interna molto rigorosa non è la stessa cosa di una validazione esterna. Su Tech abbiamo già visto quanto sia importante separare simulazione, modello e fenomeno fisico quando si parla di turbolenza e modelli numerici complessi.
L’AI ha trovato la prova da sola?
OpenAI descrive un sistema di ricerca multi-agente più capace del modello pubblico GPT-6 Astra. Migliaia di agenti hanno esplorato in parallelo strade diverse, verificato risultati intermedi e contribuito alla costruzione finale. Non è quindi il caso di immaginare una singola chat che riceve il problema e restituisce una prova perfetta in pochi secondi.
Il confronto è utile anche per capire dove sta andando l’AI scientifica. GPT-6 Astra è già un modello generalista molto avanzato, ma l’esperimento Navier-Stokes usa un’infrastruttura di ricerca specializzata, con molte più risorse e un processo di verifica formale costruito attorno al problema.
Il nodo della paternità e dei dati di addestramento
OpenAI affronta anche una questione delicata. Alcuni matematici, tra cui Alpöge e Buckmaster, hanno lavorato su idee collegate a scenari di blow-up per equazioni dei fluidi. L’azienda afferma che il sistema non ha avuto accesso a dati utente specifici riconducibili al loro lavoro. Allo stesso tempo riconosce di non poter escludere in assoluto che dati di utilizzo de-identificati abbiano contribuito in passato al miglioramento generale dei modelli.
È un punto da tenere separato dalla correttezza matematica. Una prova può essere corretta e allo stesso tempo richiedere una discussione distinta sulla provenienza delle idee e sull’attribuzione. OpenAI sostiene che la costruzione per Navier-Stokes sia diversa dai risultati precedenti citati nel dibattito.
OpenAI riceverà il premio da un milione di dollari?
Non è questo il punto dell’annuncio. OpenAI dichiara di non avere intenzione di rivendicare il premio da un milione di dollari. Prima ancora di parlare di premio, il risultato dovrà essere studiato, discusso e verificato dalla comunità matematica secondo i normali tempi della ricerca.
Per questo la formulazione più corretta oggi è: OpenAI sostiene di aver costruito una soluzione formalizzata a una delle formulazioni del problema di Navier-Stokes. La formalizzazione in Lean è un elemento forte, ma non consente di saltare il passaggio del controllo indipendente.
Cosa cambierebbe se la prova fosse confermata
Il primo effetto sarebbe matematico: avremmo una risposta concreta alla domanda sulla possibile formazione di singolarità nelle equazioni tridimensionali incomprimibili nella formulazione considerata. Il secondo riguarderebbe il metodo. Un sistema AI capace di produrre e formalizzare una prova di questo livello diventerebbe uno strumento nuovo per la matematica, non solo un assistente per calcoli o ricerca bibliografica.
Non significa che l’AI sostituisca il lavoro dei matematici. Al contrario, un risultato così complesso aumenta il bisogno di esperti capaci di controllare definizioni, interpretazioni e conseguenze. Il passaggio decisivo adesso non è generare altre frasi sulla prova, ma sottoporla a una verifica indipendente e riproducibile.
