Il 12 settembre 2026, una lettera firmata da 25 medaglie Fields ha allargato la discussione sul risultato pubblicato da OpenAI quattro giorni prima: l’azienda sostiene che un sistema interno di IA abbia prodotto una dimostrazione analitica e una formalizzazione in Lean per una singolarità in tempo finito nelle equazioni tridimensionali incomprimibili di Navier–Stokes. La tesi è pubblica, ma non equivale ancora a una soluzione matematicamente accettata dal mondo accademico; restano inoltre aperte la disputa sul credito e quella sulla provenienza dei dati.
Che cosa sostiene OpenAI
La formulazione descritta da OpenAI riguarda un flusso tridimensionale incomprimibile a densità costante, inizialmente regolare, con una forzante liscia. Secondo l’azienda, il flusso sviluppa in un tempo finito una singolarità: la velocità diventa illimitata mentre l’energia resta finita.
In termini intuitivi, il modello matematico segue un vortice che si avvolge verso l’interno e si allunga lungo il proprio asse. “Singolarità” non significa che l’acqua reale o le sue molecole possano raggiungere una velocità infinita: descrive un comportamento limite previsto dalle equazioni continue.
Il risultato resta una tesi di OpenAI. La formalizzazione in Lean aggiunge un controllo automatico sui passaggi codificati, ma non decide da sola se la costruzione corrisponda esattamente alla formulazione richiesta dal problema del Clay Mathematics Institute, né se la comunità matematica la riconoscerà come soluzione.
Perché Navier–Stokes è un problema del Millennio
Le equazioni di Navier–Stokes descrivono il moto dei fluidi. Il problema di esistenza e regolarità in tre dimensioni chiede, in sostanza, se un’evoluzione partita da condizioni lisce possa sviluppare una singolarità in tempo finito oppure restare regolare per sempre.
Il Clay Mathematics Institute lo ha inserito tra i sette Millennium Prize Problems, ciascuno associato a un premio di 1 milione di dollari. Questo non trasforma ogni annuncio in una soluzione ufficiale: il riconoscimento richiede che il risultato superi l’esame matematico previsto e venga accettato secondo le regole dell’istituto.
C’è anche una distinzione pratica da tenere a mente. Una dimostrazione di questo tipo avrebbe un enorme peso teorico, ma non produce automaticamente un nuovo metodo per le previsioni del tempo, l’aerodinamica o altre applicazioni ingegneristiche. Il passaggio dalla matematica fondamentale alla tecnologia richiede risultati ulteriori.
10.000 agenti e 88 ore di calcolo
OpenAI riferisce che il gruppo di agenti responsabile del risultato ha raggiunto la soluzione il 5 settembre 2026, circa 88 ore dopo l’avvio della ricerca. La successiva formalizzazione e il controllo in Lean avrebbero richiesto altre 17 ore tramite GPT-6 Astra.
Per il solo lavoro su Navier–Stokes, l’azienda indica circa 2,7 milioni di messaggi e 130 miliardi di token generati. Nell’insieme dei problemi tentati, parla invece di 4,9 milioni di messaggi e circa 300 miliardi di token.
Sono numeri che descrivono la scala dell’operazione, non la sua efficienza rispetto a un matematico umano e nemmeno la correttezza del risultato. Un’enorme esplorazione parallela può produrre una soluzione interessante; non sostituisce la necessità di capire perché funzioni.
Due linee di ricerca, non lo stesso risultato
La controversia nasce anche dalla vicinanza temporale con il lavoro di Tristan Buckmaster e Levent Alpöge. I due ricercatori stavano studiando risultati di blow-up per equazioni di Euler forzate e di Boussinesq, con l’assistenza di Claude e Codex. OpenAI presenta il proprio risultato come distinto: riguarda Navier–Stokes e una diversa configurazione della forzante.
| Dimensione | Risultato riportato da OpenAI | Lavoro collegato di Tristan Buckmaster e Levent Alpöge |
| Obiettivo matematico | Singolarità in tempo finito per Navier–Stokes tridimensionale incomprimibile con forzante liscia | Risultati di blow-up collegati per equazioni di Euler forzate e di Boussinesq |
| Strumenti di IA | Sistema interno di OpenAI con agenti coordinati; formalizzazione successiva in Lean tramite GPT-6 Astra | Claude e Codex come assistenti di ricerca, documentazione e passaggi logici |
| Rapporto tra i risultati | OpenAI sostiene che la propria costruzione abbia una portata diversa | Il lavoro è una linea di ricerca collegata, ma non coincide con il risultato dichiarato da OpenAI |
| Questione del credito | OpenAI attribuisce il risultato al proprio sistema e ai propri ricercatori | Tristan Buckmaster sostiene che priorità e discussioni sul credito siano state gestite male |
Buckmaster ha contestato la gestione della priorità, dell’attribuzione e delle domande sull’uso dei dati. Queste accuse restano controverse: non è stabilito che OpenAI abbia usato impropriamente il lavoro privato dei due ricercatori.
Dati privati: due questioni diverse
OpenAI nega che i propri ricercatori o agenti abbiano visto il lavoro specifico di Buckmaster e Alpöge prima della pubblicazione. La stessa azienda afferma però di non poter escludere che dati desidentificati derivati dall’uso dei suoi prodotti abbiano contribuito a migliorare i modelli.
Le due affermazioni non sono equivalenti. La prima riguarda l’accesso diretto a un lavoro privato durante la ricerca; la seconda riguarda un possibile contributo indiretto al miglioramento dei modelli. OpenAI non presenta quest’ultima possibilità come un fatto accaduto, e la disputa non è risolta.
Lean non significa ancora accettazione indipendente
Lean è un assistente per la dimostrazione formale: controlla che una prova codificata segua dalle definizioni e dalle ipotesi inserite nel sistema. È un controllo potente, ma opera sul testo matematico che gli viene sottoposto.
Questo lascia aperte domande decisive: la formalizzazione rappresenta esattamente il problema di Navier–Stokes definito dal Clay Mathematics Institute? La costruzione con la forzante soddisfa la portata richiesta? I passaggi possono essere compresi, spiegati e verificati senza affidarsi soltanto all’output del sistema?
Una critica tecnica ha sollevato proprio il problema del passaggio dalla costruzione forzata alla formulazione pertinente di Navier–Stokes. La questione richiede un esame matematico completo; non può essere chiusa dal semplice fatto che Lean abbia controllato una formalizzazione.
Analisi del rapporto tra formalizzazione in Lean, obiezioni tecniche e revisione matematica
La lettera delle 25 medaglie Fields allarga il problema
La lettera resa pubblica il 12 settembre, firmata da 25 medaglie Fields, non stabilisce che OpenAI abbia commesso una scorrettezza. Critica però un modello più ampio: annunci matematici generati dall’IA pubblicati troppo rapidamente, con poco tempo per la revisione, l’attribuzione dei contributi e la trasmissione della comprensione concettuale.
Il punto è meno spettacolare di un “computer che risolve la matematica”, ma molto più importante per il lavoro scientifico. Una dimostrazione non è soltanto una sequenza di passaggi validi: è anche un oggetto che altri ricercatori devono poter leggere, discutere, collegare ai risultati precedenti e insegnare.
Che cosa succede adesso
Per OpenAI, il risultato rappresenta una dimostrazione pubblicata e formalizzata di una portata notevole. Per la matematica, il passaggio decisivo è un altro: l’esame indipendente dovrà stabilire se la costruzione risponde davvero alla formulazione pertinente e se il suo significato può essere difeso davanti alla comunità.
La vicenda mette così sullo stesso piano tre standard diversi: produrre una possibile dimostrazione, controllarne formalmente i passaggi e renderla una conquista matematica condivisa. Il primo può essere accelerato da migliaia di agenti; gli altri richiedono ancora comprensione, attribuzione trasparente e tempo umano. Ed è su questo terreno, non sul numero di token, che si deciderà il peso reale della prova di OpenAI.
