OpenAI afferma che il suo sistema ha dimostrato una singolarità in tempo finito per le equazioni tridimensionali di Navier-Stokes, con un fluido inizialmente a riposo, una forza esterna regolare ed energia finita. L’azienda identifica il risultato con gli enunciati C e D del problema del Clay Mathematics Institute. In un preprint depositato il 6 ottobre 2026, tre autori sostengono però che la formalizzazione in Lean non corrisponde alla dimostrazione scritta.
Che cosa afferma OpenAI
Una singolarità in tempo finito si verifica quando una soluzione matematica perde regolarità dopo un intervallo finito. Il risultato annunciato da OpenAI riguarda questa possibilità nel modello delle equazioni di Navier-Stokes, con le condizioni specifiche descritte dall’azienda: il fluido parte da uno stato regolare e fermo, è sottoposto a una forza esterna regolare e mantiene energia finita.
OpenAI ha indicato che il risultato riguarda gli enunciati C e D della formulazione del problema del Clay Mathematics Institute. Ha anche dichiarato di non voler richiedere il premio Millennium, che vale 1 milione di dollari.
Secondo il resoconto di OpenAI, circa 10.000 agenti hanno lavorato in parallelo e hanno raggiunto il risultato circa 88 ore dopo l’avvio. La formalizzazione e la verifica in Lean hanno richiesto altre 17 ore con GPT-6 Astra. L’azienda riferisce inoltre 2,7 milioni di messaggi e circa 130 miliardi di token generati per questo lavoro.
Euler e Navier-Stokes hanno condizioni diverse
Le equazioni di Euler e quelle di Navier-Stokes sono sistemi matematici distinti. Anche la presenza di una forza esterna cambia le condizioni del problema: un risultato con forza e uno senza forza non descrivono lo stesso caso.
| Risultato | Equazione | Forza esterna |
| Lavoro di Tristan Buckmaster e Levent Alpöge | Euler | Presente |
| Risultato di OpenAI sulla regolarità | Euler | Assente |
| Risultato annunciato da OpenAI | Navier-Stokes | Presente, regolare |
OpenAI descrive il proprio risultato su Euler come non forzato; la ricostruzione di Scientific American del 22 ottobre 2026 descrive come forzato il lavoro di Buckmaster e Alpöge. Il risultato Navier-Stokes di OpenAI, invece, usa una forza esterna regolare. Le tre condizioni non sono intercambiabili.
La stessa ricostruzione riferisce valutazioni diverse sulla provenienza delle idee. Buckmaster ritiene che il lavoro di OpenAI abbia seguito una strada aperta dalla sua collaborazione con Alpöge; altri matematici considerano distinta la costruzione Navier-Stokes di OpenAI rispetto al programma con forza sviluppato da Diego Córdoba e Luis Martínez-Zoroa.
Che cosa contesta il preprint su Lean
Lean è un assistente per le dimostrazioni formali: controlla una prova codificata rispetto all’enunciato inserito nel sistema. Il controllo riguarda quindi il testo matematico formalizzato; per collegarlo alla dimostrazione scritta, la formalizzazione deve rappresentare lo stesso enunciato e lo stesso ragionamento.
Nel preprint depositato su arXiv il 6 ottobre, Alexander Bastounis, Fabian Circelli e Anders C. Hansen sostengono che la formalizzazione Lean di OpenAI non corrisponde alla dimostrazione in linguaggio naturale. La loro critica riguarda il rapporto tra i due testi, un passaggio distinto dal controllo meccanico della prova codificata. OpenAI aveva presentato sia una dimostrazione analitica sia una formalizzazione Lean nel suo annuncio sul problema di Navier-Stokes.
La disputa sulla provenienza
Secondo la ricostruzione pubblicata da Scientific American il 22 ottobre, Buckmaster sospetta che il lavoro precedente svolto con Alpöge abbia influenzato il percorso di OpenAI. L’azienda ha dichiarato che gli input degli utenti successivi al 3 luglio 2026, compreso l’uso di Codex e ChatGPT da parte di Buckmaster, non potevano influenzare il modello o i risultati.
Il tema si inserisce nel dibattito più ampio sui lavori matematici di OpenAI: NeoTeo ha raccontato anche il ritiro di tre manoscritti dopo un errore di segno.
