Il 25 ottobre 2026 Scott Armstrong ha descritto il risultato di OpenAI su Navier–Stokes come forse oltre ciò che una persona avrebbe potuto ideare, ma comunque comprensibile. Il suo giudizio riguardava l’ambizione e la comprensibilità del lavoro. Nel preprint del 6 ottobre, A. Bastounis, F. Circelli e A. C. Hansen sostengono invece che la formalizzazione in Lean non corrisponda semanticamente alla prova scritta; gli autori precisano che la loro analisi non afferma che quella dimostrazione sia errata.
Che cosa valutava Armstrong
Nel suo post su X, Armstrong ha espresso un giudizio sulla portata tecnica della costruzione e sulla possibilità che gli esperti la comprendano. Non era una valutazione matematica della correttezza della dimostrazione. Greg Brockman, presidente di OpenAI, ha pubblicato separatamente un post con una formulazione centrale analoga.
Il commento si aggiunge al dibattito sulle reazioni dei matematici all’annuncio, già seguito da NeoTeo nel confronto tra Richard Borcherds e Robin Huang sull’IA nella matematica.
La discrepanza tra Lean e la prova scritta
Nel preprint del 6 ottobre, Bastounis, Circelli e Hansen sostengono che la formalizzazione di OpenAI in Lean non conservi semanticamente la dimostrazione in linguaggio naturale. La fedeltà semantica è la corrispondenza di significato tra il testo matematico e la sua versione formalizzata.
Un esempio riguarda il numero di derivate aggiuntive nelle stime messe a confronto dagli autori:
| Stima confrontata | Derivate aggiuntive |
| Prova in linguaggio naturale | 4 |
| Stima citata nella formalizzazione Lean | 5 |
Gli autori descrivono anche differenze nella stima del flusso di pressione e nella relativa dimostrazione, comprese variazioni nelle variabili e nelle condizioni temporali considerate. Limitano esplicitamente la loro conclusione alla corrispondenza tra le due versioni: non sostengono che la prova in linguaggio naturale sia errata.
Che cosa verifica Lean
Lean è un assistente per le dimostrazioni formali: controlla un enunciato matematico e una dimostrazione codificati nel proprio linguaggio. Quel controllo riguarda la formulazione formale. Stabilire se questa conservi il significato della prova scritta è una questione distinta, al centro dell’analisi dei tre autori.
La portata dichiarata da OpenAI e l’avviso di Clay
Nell’annuncio dell’8 settembre 2026, OpenAI ha presentato un risultato che, secondo l’azienda, produce una singolarità in tempo finito per un fluido incomprimibile tridimensionale, inizialmente fermo e sottoposto a una forza esterna regolare, mantenendo finita l’energia. OpenAI ha dichiarato che il risultato riguarda i casi forzati C e D della formulazione del problema di Clay e che non intende chiedere il premio.
Nel comunicato dell’11 settembre 2026, il Clay Mathematics Institute ha definito il problema apparentemente risolto e ha descritto la valutazione del premio come deliberatamente lenta.
