Sul Problema del Millennio di Navier–Stokes

Presentiamo una soluzione al problema dell’esistenza e della regolarità delle equazioni di Navier–Stokes, uno dei Problemi del Millennio. Questa dimostrazione, elaborata da un sistema interno di OpenAI, mostra che la dinamica delle equazioni di Navier–Stokes per il moto dei fluidi può sviluppare una singolarità in un tempo finito. Pubblichiamo sia una descrizione della dimostrazione sia una formalizzazione in Lean.

I Problemi del Millennio⁠(si apre in una nuova finestra) rappresentano alcune delle questioni più profonde della matematica di frontiera. La questione se il moto regolare di un fluido tridimensionale possa degenerare è rimasta irrisolta per circa 90 anni.

Uno dei principali obiettivi del nostro lavoro è fornire agli scienziati gli strumenti per far progredire la ricerca e la tecnologia a beneficio di tutta l’umanità. Per risolvere il problema di Navier–Stokes abbiamo usato un modello interno significativamente più capace di GPT‑6 Astra. Riteniamo importante informare il mondo sul ritmo dei progressi dell’IA e su cosa aspettarsi dai prossimi modelli.

Le equazioni di Navier–Stokes applicano la seconda legge del moto di Newton («F=ma») per descrivere il movimento dei fluidi. Un aspetto importante è che trattano il fluido come un mezzo continuo, anziché seguire le singole molecole. Queste equazioni vengono impiegate nella progettazione aeronautica, nelle previsioni meteorologiche e nello studio del flusso sanguigno.

Una questione fondamentale ancora aperta per queste equazioni dinamiche è se l’approssimazione continua del fluido possa venir meno. In particolare, le equazioni di Navier–Stokes per un fluido tridimensionale incomprimibile a densità costante possono sviluppare una «singolarità» anche se il moto è inizialmente regolare? In questo contesto, una singolarità significa che la dinamica porta la velocità del fluido a crescere senza limite in un intervallo di tempo finito. La singolarità dovrebbe svilupparsi nonostante la presenza della viscosità, che tende a rendere uniforme il moto. Poiché un fluido reale non può muoversi a velocità infinita, ciò segnerebbe il venir meno della capacità delle equazioni di modellarlo. Per continuare a modellare il sistema, bisognerebbe quindi seguire singolarmente il comportamento di ogni particella.

Le equazioni risalgono al lavoro svolto nel XIX secolo da Claude-Louis Navier e George Gabriel Stokes. Nel 1934 Jean Leray dimostrò che le soluzioni esistono in senso generalizzato, ma stabilire se rimangano sempre regolari divenne una questione centrale ancora senza risposta. Nel 2000 il Clay Mathematics Institute incluse il problema dell’esistenza e della regolarità delle equazioni di Navier–Stokes tra i sette Problemi del Millennio.

Il nostro sistema ha prodotto una dimostrazione analitica e una formalizzazione in Lean del fatto che un fluido inizialmente regolare e a riposo può sviluppare una singolarità in un tempo finito. Al fluido viene applicata una forza regolare e la sua energia rimane finita per l’intera dinamica, dallo stato di quiete alla formazione della singolarità. Questo risolve il Problema del Millennio di Navier–Stokes stabilendo l’enunciato «C» (e anche il «D») nella formulazione ufficiale del Problema del Millennio⁠(si apre in una nuova finestra).

La soluzione è un vortice, un mulinello di fluido in rotazione, che forma una spirale verso l’interno e si allunga sempre più, come uno spaghetto. Questa regione centrale si restringe mentre accelera, in modo tale che la sua energia rimanga comunque finita, come richiesto dalle leggi della fisica. La difficoltà tecnica consiste nel far sì che le equazioni degenerino attraverso il moto stesso del fluido, anziché, per esempio, inserendo manualmente una forza infinita. In termini più matematici, i termini delle equazioni di Navier–Stokes che descrivono il moto — accelerazione, gradienti di pressione, trasferimento della quantità di moto e viscosità — devono diventare al contempo grandi e annullarsi a vicenda in modo preciso. Questo equilibrio dettagliato mantiene regolare la forza esterna anche quando la velocità del fluido cresce senza limite.

Dal 28 agosto stiamo addestrando un nuovo modello interno che ha mostrato prestazioni senza precedenti nei nostri benchmark, anche in matematica. L’addestramento di questo modello è tuttora in corso e le sue prestazioni continuano a migliorare.

Martedì 1° settembre abbiamo sentito voci secondo cui erano stati risolti due Problemi del Millennio. Ispirati da queste voci e dal salto di qualità nelle prestazioni del nostro modello interno, abbiamo avviato un progetto per valutarlo su tutti i Problemi del Millennio ancora aperti e su alcuni altri problemi di grande rilevanza.

Abbiamo usato un sistema di agenti coordinati basati sul nostro modello interno. Gli agenti avevano accesso a strumenti che permettevano, tra l’altro, di consultare una versione memorizzata nella cache di Internet e di eseguire codice. Gli agenti erano suddivisi in gruppi e potevano comunicare all’interno del proprio gruppo. Le dimensioni dei gruppi variavano; quello che ha risolto il problema di Navier–Stokes comprendeva circa 10.000 agenti simultanei. Abbiamo sempre mantenuto le stesse rigorose misure di sicurezza che applichiamo a tutte le valutazioni dei nostri modelli di frontiera, inclusi monitoraggio e isolamento.

Per ogni problema abbiamo presentato a diversi gruppi di agenti differenti varianti dell’enunciato, così da coprire tutte le formulazioni del problema. Per il problema di Navier–Stokes abbiamo assegnato a gruppi distinti le versioni «A» e «B» (forme specifiche del problema che avrebbero prodotto una dimostrazione) e le versioni «C» e «D» (che avrebbero prodotto una confutazione).

Oltre ai Problemi del Millennio completi, abbiamo chiesto al nostro sistema multiagente di affrontare una serie di problemi «più facili». Uno di questi riguardava una questione analoga sull’esplosione delle soluzioni nel limite del problema di Navier–Stokes ottenuto eliminando il termine di viscosità. È il cosiddetto problema della regolarità per le equazioni di Eulero, e i nostri agenti ci hanno sorpreso risolvendolo. La variante specifica che hanno risolto era quella senza forzante, nella quale non viene applicata alcuna forza esterna al fluido. Quasi 100 agenti hanno collaborato per circa 50 ore per produrre la nostra confutazione della regolarità di Eulero¹.

Dopo aver esaminato la soluzione per Eulero, abbiamo ritenuto che Navier–Stokes fosse il problema più promettente su cui lavorare. Abbiamo quindi deciso di dedicare le nostre risorse a Navier–Stokes. A questo scopo abbiamo riassegnato gli agenti dagli altri Problemi del Millennio e abbiamo fornito loro la soluzione per Eulero. Quando, nel corso del progetto, è diventata disponibile una versione ulteriormente addestrata del nostro modello interno, abbiamo aggiornato gli agenti affinché la usassero.

Abbiamo incoraggiato i diversi gruppi di agenti a esplorare una varietà di approcci. Dopo qualche tempo abbiamo favorito lo scambio di idee tra i gruppi di agenti, usando Codex per riunire le intuizioni più utili di ciascun gruppo. Questi prompt successivi si basavano sui risultati intermedi ottenuti dagli agenti stessi. Il gruppo che ha trovato la soluzione al problema di Navier–Stokes è stato guidato in questo modo.

Gli agenti sono giunti alla soluzione sabato 5 settembre, circa 88 ore dopo l’avvio dei primi agenti. La formalizzazione e la verifica in Lean tramite GPT‑6 Astra hanno richiesto altre 17 ore.

Considerando tutti i problemi affrontati, gli agenti hanno inviato 4,9 milioni di messaggi e usato circa 300 miliardi di token di output. Nel risolvere il problema di Navier–Stokes, gli agenti hanno inviato 2,7 milioni di messaggi e usato circa 130 miliardi di token di output.

Il nostro progetto è iniziato il 1° settembre, dopo aver sentito una voce che in seguito abbiamo capito riguardare Levent Alpöge, dipendente di Anthropic, e Tristan Buckmaster, professore di matematica alla NYU.² Dopo aver completato l’intero progetto e la verifica in Lean (il 6 settembre), credendo sulla base di quella voce che anche loro avessero una soluzione per Navier–Stokes, li abbiamo contattati per proporre la pubblicazione simultanea del nostro risultato e riconoscere la loro priorità in un annuncio congiunto. A quel punto abbiamo scoperto che, usando un modello interno di Anthropic, avevano risolto il problema di Eulero con forzante. Durante queste discussioni abbiamo offerto loro piena visibilità su tutti i prompt usati e, in seguito, la possibilità di esaminare la dimostrazione. Riconosciamo la priorità del loro lavoro sul problema di Eulero con forzante e ci congratuliamo per il loro straordinario risultato matematico.

Noi, ricercatori e agenti, non abbiamo avuto accesso in alcun modo al loro lavoro prima che fosse reso pubblico; in particolare, per risolvere questo problema non sono stati consultati dati specifici degli utenti.

A seguito di un’indagine, abbiamo confermato che i prompt inviati da Buckmaster a Codex nei due mesi precedenti l’annuncio e la pubblicazione dell’articolo l’8 settembre 2026 non avrebbero potuto influenzare in alcun modo il sistema, neppure attraverso l’addestramento. Il modello interno di OpenAI usato per questo risultato è stato sviluppato tramite apprendimento per rinforzo su larga scala, a partire da un modello precedentemente preaddestrato. Anche le nostre dimostrazioni differiscono notevolmente. Nel caso di Eulero, Alpöge e Buckmaster hanno dimostrato un risultato con forzante esterna, mentre il sistema di OpenAI ne ha dimostrato uno senza forzante esterna.

Pubblichiamo questo risultato per documentare i notevoli progressi dei nostri modelli di IA. Non intendiamo rivendicare il Premio del Millennio per questo risultato.

Questo traguardo è frutto di un notevole lavoro da parte di matematici e ricercatori nel campo dell’IA. Non rappresenta però un punto d’arrivo, bensì un’istantanea dei progressi nello sviluppo dell’IA in questo momento.

Riteniamo di essere entrati in una nuova fase del progresso dell’IA⁠, e i risultati odierni ne offrono un’ulteriore prova. Ci stiamo concentrando sulla comprensione di questo modello e sull’uso di ciò che impariamo per orientare e modulare il ritmo con cui perseguiamo ulteriori progressi nelle capacità. Uno dei nostri obiettivi principali⁠ è creare sistemi di IA che possano essere orientati, siano responsabili e rimangano connessi alle persone. Ciò potrebbe richiedere scelte più ponderate sul ritmo del progresso mentre proseguiamo nella nostra missione di garantire che l’AGI vada a beneficio di tutta l’umanità.