The Pulse

OpenAI sostiene che la sua IA abbia trovato una soluzione con blowup per Navier–Stokes

Un sistema di IA interno ha prodotto una dimostrazione secondo cui un flusso tridimensionale di Navier–Stokes può sviluppare una singolarità in tempo finito, afferma OpenAI. L’annuncio ha sollevato interrogativi sulla verifica matematica, s

AI.info Team · Scritto con l’IA · verificato · 2026-09-12

«Ho pensato che dovesse esserci un errore da qualche parte. E domenica mattina avevamo la soluzione finale, formalizzata in Lean e tutto il resto.»

Sebastien Bubeck, matematico e ricercatore di IA, OpenAI

OpenAI afferma che un sistema di intelligenza artificiale interno ha prodotto una soluzione al problema dell’esistenza e regolarità delle soluzioni delle equazioni di Navier–Stokes, uno dei sette problemi per il premio del millennio che da decenni mettono alla prova i matematici. L’8 settembre la società ha pubblicato un articolo tecnico di 166 pagine e una formalizzazione in Lean verificabile da un computer, sostenendo che un fluido tridimensionale regolare può sviluppare una velocità illimitata in tempo finito mentre la sua energia cinetica rimane limitata.

L’annuncio descrive un risultato matematico, non un nuovo modo di calcolare i normali flussi di fluidi. Gli ingegneri usano già approssimazioni numeriche delle equazioni di Navier–Stokes per la progettazione di aeromobili, i modelli meteorologici e gli studi sul flusso sanguigno. La questione ancora irrisolta è se le equazioni possano perdere validità nelle condizioni specificate dal Clay Mathematics Institute, che ha posto il problema nel 2000 e ha associato un premio di 1 milione di dollari a una soluzione valida.

OpenAI non reclamerà il premio. L’articolo e la dimostrazione formale sono ora disponibili per l’esame dei matematici e la formulazione usata dalla società è significativa: il risultato viene presentato come una soluzione generata dall’IA e come prova dei progressi nella ricerca automatizzata, ma lo stato formale del problema del millennio dipende ancora dalla valutazione degli esperti.

Il risultato di OpenAI riguarda le alternative C e D

Le equazioni di Navier–Stokes descrivono il moto di un fluido incomprimibile attraverso velocità, pressione, viscosità e forza esterna. In tre dimensioni, i matematici sanno che esistono soluzioni deboli a energia finita, ma non hanno stabilito se le soluzioni regolari restino tali per ogni istante. Una singolarità significherebbe che la velocità diventa illimitata in un tempo finito, facendo venir meno la descrizione classica.

L’articolo di OpenAI costruisce una soluzione che parte da uno stato di quiete e sviluppa una singolarità mantenendo limitata l’energia cinetica. La costruzione utilizza una forza regolare a supporto compatto nello spazio e nel tempo. Secondo l’articolo, la velocità rimane regolare prima dell’istante singolare, poi cresce senza limite in prossimità di un punto di concentrazione.

La dimostrazione affronta le alternative «C» e «D» nella formulazione ufficiale del problema del Clay Mathematics Institute redatta da Charles Fefferman. L’alternativa C riguarda la perdita di regolarità nello spazio euclideo tridimensionale, mentre l’alternativa D riguarda un dominio tridimensionale periodico. Il repository pubblico di OpenAI descrive i due risultati come una dimostrazione del fatto che dati iniziali e forzante regolari possono impedire l’esistenza di una soluzione globale regolare con energia cinetica uniformemente limitata nel caso dell’intero spazio e possono impedire l’esistenza di una soluzione globale regolare sul toro periodico.

La costruzione ruota attorno a un vortice in collasso. OpenAI descrive una regione centrale che si avvolge a spirale verso l’interno, si allunga lungo il proprio asse e diventa sempre più concentrata. La velocità aumenta man mano che il nucleo si restringe, ma l’energia cinetica totale resta controllata perché la regione in cui il flusso è più veloce diventa più piccola.

Questo equilibrio costituisce la difficoltà matematica. L’accelerazione, la pressione, il trasferimento non lineare della quantità di moto e i termini viscosi possono ciascuno assumere valori elevati in prossimità della singolarità. La dimostrazione fa sì che si compensino in modo da lasciare una forza esterna regolare. Impulsi oscillatori in una regione anulare trasportano quantità di moto attraverso il fluido e forniscono lo sforzo necessario a sostenere la struttura in collasso.

10.000 agenti e 88 ore

Il lavoro è iniziato dopo che il 1º settembre la società aveva appreso voci secondo cui alcuni ricercatori avrebbero potuto aver fatto progressi su due problemi per il premio del millennio. La società stava addestrando un nuovo modello interno dal 28 agosto e ha deciso di metterlo alla prova sui problemi aperti, insieme a diverse altre difficili questioni matematiche.

Il sistema non consisteva in un solo modello che produceva un’unica risposta in una sola sessione. OpenAI ha suddiviso il lavoro tra gruppi di agenti coordinati tra loro, ciascuno dei quali esplorava versioni e approcci diversi. Secondo la società, il gruppo che ha prodotto il risultato su Navier–Stokes comprendeva circa 10.000 agenti operanti contemporaneamente. Gli agenti potevano consultare una versione di Internet salvata nella cache, eseguire codice e comunicare all’interno dei gruppi a cui erano stati assegnati.

I primi agenti sono stati avviati il 1º settembre e il sistema è arrivato alla sua soluzione per Navier–Stokes il 5 settembre, circa 88 ore dopo, afferma OpenAI. Altre 17 ore di lavoro sono state dedicate alla formalizzazione e alla verifica attraverso GPT-6 Astra, il modello annunciato dalla società per controllare la dimostrazione in Lean.

La scala del calcolo è insolita anche per gli standard della matematica automatizzata. Secondo OpenAI, considerando tutti i problemi affrontati, gli agenti hanno inviato 4,9 milioni di messaggi e generato circa 300 miliardi di token in output. Il lavoro su Navier–Stokes ha rappresentato 2,7 milioni di messaggi e circa 130 miliardi di token in output.

Il resoconto di OpenAI mostra anche come il sistema sia passato da un problema all’altro. Gli agenti hanno prima prodotto un risultato per una questione di regolarità correlata, riguardante le equazioni di Eulero, che omettono il termine di viscosità presente in quelle di Navier–Stokes. La società ha poi indirizzato gli agenti verso Navier–Stokes e ha usato Codex per riunire le idee utili provenienti da gruppi di agenti distinti.

Lean verifica la dimostrazione formale, non l’intera affermazione

Lean fornisce un linguaggio formale in cui gli enunciati matematici e i passaggi delle relative dimostrazioni possono essere verificati da un software. OpenAI ha pubblicato file Lean e un repository pubblico contenente certificati associati ai risultati su Navier–Stokes ed Eulero. Questo offre ai ricercatori esterni un modo per verificare se i passaggi formalizzati discendano dalle definizioni e dagli assiomi scelti.

La verifica formale è importante perché i modelli linguistici possono produrre argomentazioni persuasive ma non valide. Un assistente alla dimostrazione può individuare molti errori locali, casi mancanti e trasformazioni non giustificate. Da solo, non stabilisce se l’enunciato formale rappresenti il problema matematico inteso, se l’esposizione che lo accompagna sia chiara o se una costruzione sia stata trascritta correttamente dalla ricerca sottostante.

L’articolo di OpenAI formula un’affermazione specifica: per ogni viscosità positiva, costruisce una forza regolare e una soluzione che parte da velocità zero, mantiene un’energia cinetica finita e sviluppa una velocità illimitata in tempo finito. La dimostrazione è molto più circoscritta di una previsione generale secondo cui ogni fluido fisico formerà un vortice a velocità infinita. La sua conclusione si applica alle condizioni matematiche indicate nell’articolo.

I matematici indipendenti devono ancora leggere l’intera argomentazione. La formulazione del problema del Clay Mathematics Institute richiede soluzioni regolari e fisicamente ragionevoli e distingue tra le formulazioni sull’intero spazio e quelle periodiche. Qualsiasi decisione sul premio richiederebbe che il risultato superi l’esame di esperti di equazioni alle derivate parziali e di dinamica dei fluidi, non soltanto una verifica tramite software.

L’annuncio si è scontrato con una ricerca esterna

L’annuncio di OpenAI è arrivato nel mezzo di una controversia che coinvolge Tristan Buckmaster, professore di matematica alla New York University, e Levent Alpöge, ricercatore di Anthropic. Buckmaster ha detto che i due lavoravano da circa un anno su equazioni dei fluidi correlate, con l’aiuto di diversi modelli di IA, tra cui Codex di OpenAI e Claude di Anthropic.

Secondo il racconto di Buckmaster, i ricercatori hanno compiuto importanti progressi il 15 agosto e li hanno verificati entro il 22 agosto. Il loro lavoro si concentrava su un problema di Eulero con forzante, basato su un’equazione correlata che elimina la viscosità da Navier–Stokes. L’approccio dei due si basava su lavori precedenti di Diego Córdoba e Luis Martínez-Zoroa ed era abbastanza insolito da indurre Buckmaster a ritenere improbabile che un altro gruppo vi arrivasse semplicemente fornendo a un modello l’enunciato del problema come prompt, ha detto lo stesso Buckmaster.

OpenAI aveva appreso voci sul lavoro esterno prima di avviare il proprio. La società ha negato di aver usato i prompt o la dimostrazione dei due per indirizzare i propri agenti. Nel briefing dell’8 settembre descritto da WIRED, Bubeck ha detto che i ricercatori e gli agenti non avevano visto il lavoro esterno prima che diventasse pubblico.

Buckmaster non ha accusato OpenAI di aver sottratto il lavoro. Ha detto di non sapere se i suoi dati siano stati usati e si è chiesto se i sistemi di OpenAI possano aver incontrato materiale proveniente dalle sue sessioni con Codex attraverso i dati di addestramento o quelli dei prodotti. La distinzione è importante: dimostrare che due progetti hanno seguito percorsi matematici correlati non proverebbe che uno abbia copiato l’altro.

La successione temporale ha comunque posto al centro della vicenda il riconoscimento dei meriti della ricerca. Il risultato di OpenAI e il lavoro su Eulero dei ricercatori esterni non sono identici. Secondo la società, la dimostrazione di OpenAI tratta le equazioni viscose di Navier–Stokes senza forzante esterna nel meccanismo che genera la singolarità, mentre il lavoro esterno affrontava un risultato relativo a Eulero con forzante. L’eventuale esistenza di una dipendenza matematica più profonda tra gli approcci è una questione per specialisti in grado di confrontare le dimostrazioni complete.

Una prova per le affermazioni sulla ricerca con l’IA

L’annuncio di OpenAI mette a confronto due criteri di successo. Uno è computazionale: il sistema ha generato una lunga dimostrazione, l’ha formalizzata e ha messo online i file sottostanti. L’altro è scientifico: i matematici devono stabilire se la costruzione sia corretta, se soddisfi l’esatta formulazione del Clay Mathematics Institute e quali idee possano essere comprese e riutilizzate dalle persone.

La distinzione è importante perché una dimostrazione completa può nascondere il percorso che l’ha prodotta. I matematici umani imparano spesso dagli approcci falliti, dai lemmi intermedi e dalle ragioni per cui una particolare costruzione funziona. Un sistema multiagente può esplorare molte direzioni contemporaneamente, ma la sua velocità può lasciare ai ricercatori un risultato difficile da interpretare anche quando il verificatore formale lo accetta.

OpenAI presenta il lavoro come un resoconto delle capacità di un modello interno più potente di GPT-6 Astra, piuttosto che come una richiesta del premio. Questa impostazione evita che sia la sola società a dichiarare risolto il problema del millennio, ma pone anche l’articolo e il repository pubblicati sotto pressione. La documentazione tecnica dovrà sostenere la tesi oltre la descrizione fornita dalla stessa OpenAI.

Per ora, il fatto verificato è più circoscritto del titolo che circolerà su Internet: OpenAI ha pubblicato una dimostrazione che sostiene l’esistenza di un blowup in tempo finito per una determinata classe di soluzioni tridimensionali di Navier–Stokes, insieme a una formalizzazione in Lean e ai file sorgente da esaminare. Il premio del Clay Mathematics Institute non è stato reclamato e il verdetto matematico spetta ai ricercatori che esamineranno la dimostrazione riga per riga.