Un’IA risolve uno dei problemi del millennio e punta al premio da un milione

OpenAI punta a risolvere il problema di Navier-Stokes con una singolarità costruita dagli agenti: una possibile prova, verificata da Lean ma ancora legata al lavoro umano, tra controversie e premio da un milione.

OpenAI ha annunciato il 9 settembre 2026 di avere ottenuto, attraverso un sistema composto da agenti artificiali, una dimostrazione legata alle equazioni di Navier-Stokes, uno dei sette Problemi del Millennio scelti dal Clay Mathematics Institute. Per arrivare al risultato sarebbero serviti circa 10.000 agenti, 88 ore di calcolo e una spesa valutata in milioni di dollari. Il titolo, per, va ridimensionato: quella di OpenAI per ora una soluzione annunciata, sottoposta al controllo della comunit matematica. Il premio non stato assegnato.

La distinzione riguarda la sostanza, non la forma. Un sistema artificiale pu formulare una congettura, proporre una strategia, sviluppare passaggi tecnici oppure aiutare a esaminare una prova. Perch il risultato venga riconosciuto dal Clay Institute occorrono una dimostrazione completa e pubblica, la correttezza dei passaggi e laccettazione da parte degli specialisti dopo un adeguato periodo di esame. Sul caso pesa anche una controversia: riguarda la priorit delle idee e leventuale impiego di dati prodotti da due matematici impegnati nello stesso ambito.

Il problema di Navier-Stokes indicato da OpenAI

Il quesito al centro dellannuncio il Problema dellesistenza e della regolarit delle soluzioni delle equazioni di Navier-Stokes. Queste equazioni servono a descrivere il movimento di fluidi come acqua e aria, usando grandezze quali velocit, pressione e densit. La loro formulazione si svilupp nellOttocento grazie ai lavori dellingegnere francese Claude-Louis Navier e del matematico e fisico irlandese George Gabriel Stokes.

In termini semplificati, la domanda la seguente: quando un fluido parte da condizioni regolari e i dati iniziali sono sufficientemente lisci, la soluzione resta regolare per ogni istante oppure pu formarsi una singolarit in un tempo finito? In una singolarit, una quantit matematica, per esempio la velocit, potrebbe crescere senza limite o smettere di avere la regolarit richiesta.

Non si sta chiedendo se lacqua reale possa raggiungere una velocit infinita. Un fluido fisico fatto di molecole e il modello continuo delle equazioni ha un preciso campo di applicazione. La questione interna alla teoria: il modello matematico produce sempre una soluzione liscia e controllabile, oppure consente condizioni nelle quali la soluzione esplode?

Perch le equazioni interessano anche le applicazioni

Navier-Stokes viene usato per rappresentare fenomeni con conseguenze pratiche molto diverse. Le equazioni entrano nello studio dellaerodinamica e nella progettazione degli aeromobili, nelle previsioni meteorologiche, nellanalisi del flusso sanguigno e nella modellazione della diffusione degli inquinanti.

Una possibile singolarit, per, non implica che le previsioni del tempo cambieranno domani o che gli aerei verranno progettati da capo. Gli strumenti applicativi lavorano con approssimazioni numeriche, condizioni controllate e riscontri sperimentali. La dimostrazione annunciata riguarda la struttura teorica delle equazioni. Un effetto pratico immediato, quindi, non scontato.

Il valore delleventuale risultato sarebbe soprattutto matematico. Mostrerebbe che una soluzione inizialmente regolare pu arrivare a una condizione di rottura in un tempo finito, almeno nella configurazione studiata. Risponderebbe a una domanda aperta da decenni, senza sostenere che ogni fluido o ogni simulazione reale sia destinato a diventare instabile.

La costruzione della singolarit

Il percorso descritto nei materiali pubblicati prende avvio dal lavoro dei matematici spagnoli Diego Crdoba e Luis Martnez-Zoroa. La loro attenzione si concentrata su un termine della formulazione che rappresenta una forza esterna in grado di mettere in moto il fluido. Quel termine fa parte del problema del Clay Institute, ma nelle analisi viene spesso lasciato da parte, perch si riteneva che non potesse generare il comportamento ricercato.

Crdoba e Martnez-Zoroa hanno indicato come forcing la tecnica che utilizza questa forza. La costruzione analitica, dunque non si fonda soltanto su simulazioni numeriche. Mette insieme una successione di strati regolari in una struttura descritta come una cascata infinita. Nel 2023 i due matematici avevano gi raggiunto un risultato su una versione delle equazioni di Eulero, priva di viscosit, nella quale compariva per una forza esterna non abbastanza regolare.

La difficolt successiva era conservare la singolarit mentre si imponeva una forza liscia, quindi regolare. Lidea ha interessato Tristan Buckmaster, matematico della New York University, e Levent Alpge, ricercatore che lavora per Anthropic. I due avrebbero impiegato modelli linguistici differenti per vagliare strategie, scrivere formulazioni e controllare parti della dimostrazione.

Il lavoro degli agenti di OpenAI

OpenAI ha presentato un processo fondato su agenti coordinati. Un agente un sistema software capace di scomporre un obiettivo, svolgere operazioni, valutare i risultati intermedi e andare avanti senza una supervisione umana costante. Nel caso in questione, gli agenti avrebbero letto materiale scientifico, scritto ed eseguito codice, messo a confronto approcci diversi e scambiato tra loro i risultati.

Prima dellesperimento su Navier-Stokes ci sarebbe stata una fase preparatoria dedicata a problemi collegati. Circa 1.000 agenti avrebbero affrontato una versione pi accessibile, riferita alle equazioni di Eulero, lavorando per circa 50 ore. Le soluzioni considerate pi solide sarebbero state usate per indirizzare la fase successiva.

Per la forma completa di Navier-Stokes, OpenAI avrebbe messo in funzione circa 10.000 copie del proprio modello interno. La dimostrazione sarebbe arrivata dopo circa 88 ore di lavoro, mentre il costo computazionale sarebbe stato stimato dallazienda in milioni di dollari. Gli agenti avrebbero scambiato milioni di messaggi e generato una quantit enorme di testo matematico. Le cifre sul traffico complessivo, per, provengono dalla descrizione di OpenAI e non verificano da sole la correttezza del risultato.

Una parte del procedimento avrebbe coinvolto anche Lean, un linguaggio accompagnato da un sistema di verifica formale. Una prova tradotta in Lean consente a un elaboratore di controllare la coerenza logica di molti passaggi formalizzati. uno strumento prezioso, ma non elimina lesame umano. Bisogna accertare che la formalizzazione descriva davvero lenunciato del problema e che durante la traduzione non siano state aggiunte ipotesi pi forti o condizioni differenti.

La prova resta legata al lavoro umano

Dire che lIA ha risolto la matematica riduce a una formula semplice una procedura molto pi complessa. Gli agenti avrebbero lavorato allinterno di un territorio preparato da decenni di ricerca. Definizioni, risultati preliminari, tecniche analitiche e scelta del termine associato al forcing provengono da matematici e gruppi di ricerca.

Nel caso specifico, la direzione basata sulla forza esterna viene ricondotta ai risultati di Crdoba e Martnez-Zoroa. Buckmaster e Alpge avrebbero poi sviluppato una linea parallela sulle equazioni di Eulero e sul problema di Navier-Stokes, usando anche modelli linguistici. OpenAI afferma di avere costruito una dimostrazione distinta e di non avere consultato il lavoro privato dei due ricercatori prima di ottenere il proprio risultato.

Il merito, in una vicenda del genere, non si assegna con una regola automatica. In matematica possono contare lintuizione iniziale, la costruzione di un lemma, lorganizzazione della prova, la verifica dei passaggi o la formalizzazione. Un sistema artificiale non un autore umano nel senso ordinario del termine. Chi progetta, dirige e controlla il processo deve per descrivere con chiarezza il contributo delle persone e delle istituzioni coinvolte.

La controversia con Buckmaster e Alpge

Buckmaster ha sostenuto che OpenAI avrebbe cominciato a lavorare seriamente su Navier-Stokes dopo avere ricevuto informazioni sui progressi suoi e di Alpge. Il matematico ha raccontato di avere domandato quando fosse stato inviato il primo prompt rilevante. La risposta, secondo il suo resoconto, avrebbe collocato quel passaggio dopo la diffusione delle notizie sul lavoro dei due.

Ha posto anche una domanda sulleventuale presenza delle proprie conversazioni con Codex nei dati utilizzati per laddestramento o per il miglioramento dei modelli. Il punto delicato. Per alcuni account individuali, la condivisione dei contenuti con i processi di addestramento pu dipendere dalle impostazioni del servizio. Questo, da solo, non prova che una sessione specifica sia stata letta dagli agenti impegnati nella dimostrazione.

OpenAI ha respinto lipotesi di un accesso diretto al lavoro dei due ricercatori e ha dichiarato che n il gruppo umano n gli agenti avrebbero consultato quel materiale prima della pubblicazione. Lazienda ha anche riconosciuto di non potere escludere, in astratto, che conversazioni anonimizzate e mescolate con altri dati siano confluite nei processi generali di addestramento. Ha precisato, per, che nessun dato utente specifico sarebbe stato usato per risolvere il problema.

La cronologia, i contatti e la somiglianza tra le dimostrazioni restano oggetto di ricostruzioni diverse. C poi la questione del riconoscimento di Alpge, che lavora per Anthropic, concorrente di OpenAI. I documenti completi dovranno essere esaminati pubblicamente. Prima di allora, le accuse di appropriazione non possono essere presentate come fatti accertati.

Il peso del lavoro di Crdoba e Martnez-Zoroa

La vicenda mette in evidenza un punto che gli annunci tecnologici tendono a lasciare sullo sfondo: trovare una prova non significa creare da zero ogni idea che la compone. Charles Fefferman, matematico di Princeton e autore della descrizione ufficiale del problema per il Clay Institute, ha indicato proprio Crdoba e Martnez-Zoroa come figure decisive per la direzione concettuale collegata al risultato annunciato.

Il loro lavoro aveva messo in discussione unassunzione diffusa, cio che il termine della forza esterna potesse essere ignorato senza cambiare la sostanza del problema. Se confermata nella forma richiesta, una costruzione capace di combinare singolarit e forza regolare sarebbe il prodotto di unevoluzione collettiva della ricerca. Non soltanto della potenza di calcolo impiegata da OpenAI.

La ricostruzione serve anche alla correttezza scientifica. Una prova pu essere nuova pur basandosi su strumenti gi conosciuti, ma la priorit delle idee va stabilita confrontando manoscritti, date, versioni, comunicazioni e passaggi matematici. Un comunicato aziendale non pu chiudere da solo questa verifica.

Che cosa pu e non pu garantire Lean

La formalizzazione in Lean uno degli elementi pi interessanti del caso. Un verificatore formale pu esaminare migliaia di inferenze seguendo regole precise, con un rischio ridotto di errori algebrici o logici. Pu rendere riproducibile una parte del controllo, a condizione che il codice e tutte le sue dipendenze siano pubblici e utilizzabili.

La verifica, per, si articola su almeno tre piani:

• Formalizzazione: il sistema deve accertare che il codice Lean compili e che i teoremi derivino correttamente dalle ipotesi dichiarate.
• Enunciato: i matematici devono verificare che quelle ipotesi coincidano davvero con la formulazione del problema del Clay Institute.
• Comunicazione della prova: la dimostrazione deve essere completa, comprensibile e sottoposta allanalisi di esperti indipendenti, non soltanto controllabile da una macchina.

Una prova corretta dal punto di vista formale, ma riferita a un enunciato pi debole, modificato o ristretto, non risolverebbe il Problema del Millennio. Ecco perch la pubblicazione integrale e il confronto con gli specialisti restano necessari.

I sette Problemi del Millennio

Nel 2000 il Clay Mathematics Institute, organizzazione dedicata alla ricerca matematica, selezion sette problemi considerati tra i pi profondi e influenti. Per ciascuno stabil un premio di un milione di dollari. La scelta si colloca nella tradizione dei 23 problemi presentati da David Hilbert nel 1900.

I quesiti sono:

• Navier-Stokes: esistenza e regolarit delle soluzioni delle equazioni che descrivono i fluidi.
• Ipotesi di Riemann: posizione degli zeri non banali della funzione zeta e conseguenze sulla distribuzione dei numeri primi.
• Congettura di Birch e Swinnerton-Dyer: rapporto tra curve ellittiche e punti razionali.
• Congettura di Hodge: relazione tra oggetti geometrici e classi di coomologia.
• Equazioni di Yang-Mills e problema del mass gap: fondamenti matematici di una teoria fisica dei campi.
• Congettura di Poincar: caratterizzazione tridimensionale della sfera.
• Problema P contro NP: rapporto tra problemi facilmente verificabili e problemi facilmente risolvibili.

La congettura di Poincar lunica soluzione riconosciuta ufficialmente. Grigori Perelman la dimostr tra il 2002 e il 2003, mentre il Clay Institute riconobbe il risultato nel 2010. Il matematico russo rifiut il premio previsto e anche la Medaglia Fields ricevuta nel 2006.

Le condizioni per ottenere il milione

Un comunicato aziendale non basta, cos come non basta un testo plausibile prodotto da un modello. Le regole del Clay Institute prevedono che la soluzione venga pubblicata in una sede scientifica qualificata e che passi un periodo sufficiente per permettere alla comunit matematica di esaminarla e accettarla.

La procedura comprende questi passaggi:

• Pubblicazione: la dimostrazione deve essere disponibile in forma completa e valutabile secondo criteri scientifici.
• Revisione: specialisti indipendenti analizzano definizioni, ipotesi, lemmi e conclusioni.
• Accettazione: il risultato deve essere riconosciuto come corretto dopo il periodo previsto dalle regole del Clay Institute.
• Decisione dellistituto: soltanto a quel punto il premio pu essere considerato assegnabile secondo la procedura ufficiale.

Il Clay Institute ha continuato a classificare Navier-Stokes come problema non risolto, poich la dimostrazione di OpenAI non aveva completato questo iter. La stessa OpenAI ha dichiarato che non intende reclamare il milione, nel caso in cui il risultato venga confermato. Per ora, dunque, si pu parlare di una possibile candidatura al riconoscimento. Il premio non maturato.

Tre stati diversi: congettura, prova assistita, soluzione

Un esempio aiuta a distinguere le categorie. Supponiamo che un programma proponga lidea secondo cui ogni numero pari maggiore di due pu essere scritto come somma di due numeri primi. Sarebbe una congettura: un enunciato plausibile, magari sostenuto dal controllo di moltissimi casi, ma non dimostrato per tutti i numeri.

Se un sistema artificiale suggerisce una strategia e un matematico la trasforma in una dimostrazione, si parla di prova assistita dallIA. Il contributo della macchina pu essere molto ampio; la correttezza, per, dipende dal testo completo, dalle ipotesi e dal controllo umano o formale dei passaggi.

Per una soluzione ufficiale di un problema del Millennio serve un passaggio ulteriore. La prova deve riguardare esattamente lenunciato del Clay Institute, essere pubblica, affrontare lesame della comunit scientifica e superare il periodo di accettazione previsto. Il fatto che la prima versione sia stata generata da un algoritmo non abbrevia nessuna di queste fasi.

Le conseguenze per la ricerca matematica

Il caso Navier-Stokes potrebbe rendere pi rapida la ricerca su problemi troppo estesi per un singolo gruppo che lavori con strumenti tradizionali. Gli agenti possono seguire direzioni parallele, automatizzare calcoli, cercare controesempi e tradurre argomenti in linguaggi formali. Un controllo meccanico pu rendere pi affidabili alcune parti delle dimostrazioni.

Il modello introduce per anche un rischio istituzionale. Se i sistemi apprendono da grandi quantit di produzione scientifica, i ricercatori potrebbero condividere meno intuizioni e risultati parziali per paura di perdere la priorit. Roberto Natalini, direttore dellIstituto per le Applicazioni del Calcolo del Consiglio Nazionale delle Ricerche, ha avvertito che una chiusura della comunit danneggerebbe il meccanismo attraverso cui la matematica procede.

La trasparenza quindi una condizione tecnica, oltre che etica. Bisogna sapere quali dati sono stati impiegati, quali modelli hanno contribuito, quali prompt o procedure hanno indirizzato il lavoro e quali passaggi sono stati controllati da persone indipendenti. Senza questa documentazione diventa difficile capire se si davanti a una scoperta autonoma oppure a una ricombinazione opaca di materiale gi prodotto.

Che cosa dimostrerebbe per lintelligenza artificiale

Per OpenAI, una prova di questo tipo mostrerebbe che i sistemi agentici possono fare qualcosa di pi della generazione di testo: pianificare attivit, collaborare, correggersi e sostenere per molte ore una ricerca tecnica. Il costo, stimato in milioni di dollari, indica allo stesso tempo un limite economico. La prestazione dipenderebbe dalla qualit del modello, dalla quantit di calcolo e dal lavoro necessario per coordinare i vari agenti.

Il risultato non dimostrerebbe che lIA comprende la matematica nello stesso modo di un ricercatore umano. Indicherebbe piuttosto che un insieme di modelli in grado di produrre una struttura candidata alla prova e, se la verifica la confermasse, di affrontare un compito rimasto aperto. La differenza conta quando si valutano capacit ed errori possibili.

Una dimostrazione matematica non diventa vera perch arriva da un sistema avanzato. Allo stesso modo, non diventa falsa perch stata generata da una macchina. A decidere sono le definizioni, la logica, le ipotesi e le conseguenze controllabili.

Il punto, per ora, una candidatura

La formulazione pi precisa, sulla base dei fatti descritti, questa: OpenAI ha annunciato una dimostrazione candidata e promettente per il problema dellesistenza e della regolarit delle equazioni di Navier-Stokes. Non ancora un premio da un milione di dollari assegnato. Il Clay Mathematics Institute considera infatti il problema non risolto finch la verifica indipendente non sar conclusa.

La fase successiva dovr chiarire almeno quattro questioni: se la dimostrazione copra davvero lenunciato richiesto, se ogni passaggio sia valido, se la formalizzazione in Lean corrisponda al testo matematico e come vadano riconosciuti i contributi di Crdoba, Martnez-Zoroa, Buckmaster, Alpge e OpenAI. Anche leventuale uso di dati privati dovr essere valutato attraverso documenti e riscontri, non soltanto sulla base di dichiarazioni contrapposte.

Se la prova superer lesame, il risultato avr un peso storico per la collaborazione tra matematici, software e sistemi di calcolo. Se emergeranno lacune, lannuncio rester comunque un esperimento significativo sullimpiego degli agenti nella ricerca. La questione decisiva, in ogni caso, non si risolve contando gli agenti utilizzati. La risposta arriver dalla dimostrazione pubblica e dal giudizio degli esperti.