L’IA ha appena risolto Navier–Stokes? Cosa dimostra davvero l’affermazione di OpenAI

OpenAI sostiene che uno dei suoi sistemi interni abbia risolto uno dei Millennium Prize Problems del Clay Institute. È una storia notevole, e rappresenterebbe la più grande scoperta matematica assistita dall’IA finora. Ma c’è anche una seconda storia in corso: una lotta su chi merita davvero il merito.

Ecco cosa è successo davvero: OpenAI ha sentito una voce secondo cui il modello di un laboratorio rivale avrebbe fatto progressi su uno dei problemi irrisolti più famosi della matematica. Quella voce è bastata a far partire uno sprint: per lavorare al problema, OpenAI ha usato 10.000 agenti IA in parallelo, 88 ore di calcolo e circa 22,5 milioni di dollari di costi accumulati. Ora afferma di avere una vera dimostrazione. E riguardo al premio da 1 milione di dollari? OpenAI dice di non avere intenzione di richiederlo. (Forse non hanno bisogno dei soldi.)

Risposta rapida: Il premio Clay da 1 milione di dollari per Navier–Stokes non è stato vinto. Ciò che OpenAI afferma di aver dimostrato riguarda una variante specifica del problema, il blow-up sotto forzante regolare, che resta non verificata da matematici indipendenti. Se soddisfi o meno il problema completo, come la maggior parte degli esperti lo intende, è oggetto di reale contestazione.

Che cos’è l’equazione di Navier–Stokes, e perché vale 1 milione di dollari?

Per capire cosa stia sostenendo OpenAI, devi prima capire perché Navier–Stokes è così difficile.

Le equazioni di Navier–Stokes descrivono come si muovono i fluidi: acqua, aria, sangue. Sono alla base delle previsioni meteo, della progettazione aeronautica e della medicina circolatoria. Formulate nel XIX secolo, funzionano straordinariamente bene in pratica. La questione matematica è se funzionino sempre: esistono sempre soluzioni lisce e ben comportate, oppure un fluido governato da queste equazioni può sviluppare una singolarità, un punto in cui la velocità diventa infinita, in tempo finito?

Questa domanda, nota come problema di "esistenza e regolarità", è uno dei sette Millennium Prize Problems del Clay Mathematics Institute, ciascuno con un premio da 1 milione di dollari. Ad oggi, solo uno dei Millennium Prize Problems è stato risolto: la congettura di Poincaré, nel 2003.

Perché ci interessa proprio questo problema: a volte, i problemi matematici sono più o meno puramente accademici. Ma questo non è solo un rompicapo astratto. Ogni modello meteo, simulazione aeronautica e strumento ingegneristico che si basa su queste equazioni presuppone implicitamente che si comportino bene, ma nessuno ha dimostrato che tale presupposto valga sempre. Se risultasse che le soluzioni possono esplodere in tempo finito, si rivelerebbe un vero scollamento tra la matematica su cui facciamo affidamento e i sistemi fisici che dovrebbe descrivere.

Cosa sostiene davvero di aver dimostrato OpenAI

La storia non inizia con un’intuizione matematica, ma con una voce. Sam Altman ha ammesso che OpenAI ha avviato lo sforzo dopo aver sentito che i modelli di Anthropic avevano risolto un importante problema di matematica, scrivendo su X: "Eravamo curiosi di vedere se i nostri potessero farlo anche loro."

Lo sprint di una settimana ha coperto più Millennium Prize Problems e ha consumato in totale 300 miliardi di token in output, circa 22,5 milioni di dollari di calcolo per tutto ciò che è stato tentato. Il solo problema di Navier–Stokes ha usato circa 130 miliardi di quei token e 2,7 milioni di messaggi. Diecimila agenti hanno lavorato in parallelo dal 1° al 6 settembre. E poi - questa è la parte su cui dovresti soffermarti - OpenAI ha detto di non avere intenzione di reclamare il premio da 1 milione, incorniciando il risultato come prova della rapidità con cui stanno avanzando i suoi modelli.

Prima di arrivare a Navier–Stokes, gli agenti di OpenAI hanno prima risolto il problema di regolarità di Euler non forzato, usando quasi 100 agenti in circa 50 ore. Dimostrando prima il comportamento di blow-up nello scenario più semplice di Euler, gli agenti hanno costruito le basi concettuali che hanno reso affrontabile l’approccio a Navier–Stokes.

Qui è dove i dettagli fanno la differenza. La formulazione ufficiale del Clay per Navier–Stokes include quattro opzioni, etichettate A, B, C e D. Le opzioni A e B chiedono soluzioni globali lisce senza forzante esterna, nello spazio tridimensionale ordinario o in un dominio periodico. Le opzioni C e D consentono esempi di blow-up con un termine di forzante esterna regolare. La dimostrazione di OpenAI prende di mira le opzioni C e D, il che significa che la variante forzata fa genuinamente parte del problema ufficiale del Clay.

Detto questo, molti matematici considerano le opzioni A e B la questione più profonda, perché la forzante è imposta dall’esterno: scegli la forza per provocare il blow-up, invece di chiederti se le equazioni possano rompersi da sole. Non è ancora chiaro se l’approccio possa essere esteso rimuovendo la forzante per affrontare A e B, e questa domanda è ancora apertissima. Il divario tra ciò che è stato mostrato e ciò che molti esperti considerano il cuore del problema è la vera conclusione qui.

Dentro la disputa su chi merita il merito

Ora che abbiamo tracciato cosa sia stato effettivamente dimostrato, la storia umana ha una linea chiara, se ci si allontana dal botta e risposta.

Il 15 agosto, Tristan Buckmaster e Levent Alpöge di Anthropic hanno dimostrato che le equazioni di Euler, la cugina senza attrito di Navier–Stokes, possono esplodere sotto forzante regolare, estendendo un approccio sviluppato da Diego Córdoba e Luis Martínez-Zoroa. I loro risultati hanno coperto anche le equazioni di Boussinesq e dei mezzi porosi incomprimibili. Quel lavoro ha richiesto circa un anno. Era inedito, in corso, costruito in silenzio. Poi la voce è uscita.

Lo sprint di OpenAI è iniziato il 1° settembre dopo aver sentito una voce che in seguito hanno collegato ad Alpöge e Buckmaster. Buckmaster aveva inviato un’email privata a OpenAI il 3 settembre dopo aver saputo che il suo lavoro era arrivato in azienda. Dopo aver completato il progetto e la verifica in Lean il 6 settembre, OpenAI ha contattato per proporre un rilascio concomitante. La versione di Buckmaster su ciò che è seguito è nettamente più tagliente: il suo resoconto descrive chiamate in cui dice di essere stato messo sotto pressione su pubblicazione e paternità, inclusi suggerimenti di escludere Alpöge a causa del suo impiego presso Anthropic.

Buckmaster sostiene che quando ha segnalato l’intenzione di rendere pubbliche queste preoccupazioni, si è sentito dire: "Perché dovresti rovinarti la carriera?" e "Se non vuoi che sia gentile, allora non devo essere gentile." Bubeck ha definito queste accuse "false e incendiarie". OpenAI nega di aver avuto accesso a prompt privati o lavori non pubblicati.

Non giudicherò chi ha ragione. Si tratta di resoconti contestati di una conversazione privata, e gli specifici sono davvero poco chiari. Ma il modello non richiede una risoluzione per meritare di essere nominato: un anno di lavoro inedito di un ricercatore indipendente è diventato la risorsa attorno a cui un laboratorio ben finanziato ha condotto uno sprint multimilionario, e ora è il ricercatore indipendente a dover rispondere a domande sulla sua carriera.

Si può davvero fidarsi di una dimostrazione matematica scritta da un’IA?

Messa sul tavolo la disputa sui crediti, resta la questione tecnica più difficile: la dimostrazione regge?

Navier–Stokes è un problema del Premio Millennium, e lo standard di prova è una dimostrazione rilasciata e verificabile. OpenAI ha pubblicato un manoscritto di 166 pagine e una formalizzazione in Lean l’8 settembre, entrambi disponibili pubblicamente per l’esame. Una peer review indipendente non è ancora avvenuta.

Se non conosci Lean, sappi che è un sistema di verifica formale delle dimostrazioni che controlla se ogni passo logico segue dal precedente. Una dimostrazione verificata in Lean non può essere "convinta a sembrare" corretta: se passa, la catena logica è solida. Ciò che Lean non fa è dirti se l’approccio è concettualmente significativo, se affronta il problema come lo intendono gli esperti, o se un matematico umano lo riconoscerebbe come una soluzione genuina.

Terence Tao, probabilmente il matematico vivente più eminente, ha offerto un monito su questa dinamica il 5 settembre, prima dell’annuncio di OpenAI. Scrivendo su Mathstodon in risposta alle voci che circolavano all’epoca, ha osservato che si trattava di una preoccupazione ipotetica: "c’è un sostanziale costo opportunità nel trasformare un problema storicamente produttivo e motivante come la regolarità di Navier–Stokes in un semplice post virale sui social che pubblicizza qualche progresso di benchmark, invece di far avanzare davvero il campo e sviluppare la prossima generazione sia di problemi da porre, sia di persone che ci lavorino." Dopo l’annuncio, Tao ha elogiato il lavoro di Buckmaster–Alpöge come "un risultato notevole" e ha osservato che i loro argomenti erano stati formalizzati in Lean. Non ha espresso pubblicamente un avallo alla specifica dimostrazione rivendicata da OpenAI.

Perché questa disputa è più grande di un solo problema matematico

Una voce, non un risultato pubblicato, non una peer review — una voce — è bastata a mobilitare uno dei laboratori di IA con le migliori risorse al mondo in uno sprint da milioni di dollari. OpenAI ha incorniciato il risultato come prova di quanto rapidamente stiano migliorando i suoi sistemi più avanzati, cioè come un asset di marketing. Questo è un problema del Premio Millennium usato come dimostrazione di benchmark in vista di una quotazione pubblica.

Axios ha posto la domanda scomoda in modo esplicito: cosa succede quando l’azienda che fornisce agli scienziati strumenti di ricerca basati su IA può anche mobilitare risorse immensamente maggiori per competere con loro? Buckmaster e Alpöge hanno usato il Codex di OpenAI per tutto il loro anno di lavoro. Gli strumenti che un ricercatore usa per avvicinarsi a un risultato possono essere di proprietà della stessa organizzazione che può superarli con quegli stessi strumenti su scala 10.000x. Non è una cospirazione. È una caratteristica strutturale di questo momento, ed è lo scenario che preoccupa da tempo, indipendentemente dal fatto che OpenAI abbia fatto qualcosa di sbagliato qui.

C’è anche un’ironia da notare: OpenAI ha sospeso ad agosto alcuni addestramenti RL di frontiera per motivi di sicurezza, poi a settembre ha eseguito a piena capacità per 88 ore un modello non rilasciato dello stesso programma di sviluppo per inseguire un titolo sulla matematica. Questo accostamento non è prova di malafede, ma non è irrilevante, nemmeno.

Quindi, Navier–Stokes è risolto oppure no?

Ecco qual è la situazione realed:

Il modello in sprint ha prodotto un risultato. Se abbia prodotto un Risultato, nel senso in cui lo intendono i matematici, è un’altra questione, e una che richiederà parecchio più tempo per avere risposta.