Il 13 ottobre 2026 Scientific American ha riferito che diversi gruppi di esperti considerano sempre più distinto dal programma dei matematici spagnoli il metodo dello sciame finale di OpenAI per la prova di Navier–Stokes. Un’analisi tecnica separata segnala inoltre una discrepanza fra un passaggio dell’articolo matematico e la stima corrispondente formalizzata in Lean: sono due questioni diverse, e gli autori dell’analisi non concludono che la prova in linguaggio naturale sia falsa.
Gli esperti distinguono il metodo dello sciame finale
Nel suo resoconto del 13 ottobre, Scientific American riferisce che i gruppi di esperti interpellati vedono una differenza tra il metodo dello sciame finale di OpenAI e il programma associato a Diego Córdoba e Luis Martínez-Zoroa. Entrambi gli approcci ricorrono a una forza costruita appositamente, ammessa dalla formulazione del problema di Clay ma non rappresentativa di una forza fisica; il modo in cui la costruiscono, però, è diverso.
Secondo lo stesso resoconto, alcuni esperti ritengono possibile che un gruppo preliminare più piccolo abbia seguito quel programma per ottenere un risultato intermedio. La valutazione sul metodo finale, quindi, non risolve la questione di un’eventuale influenza: gli esperti non possono ricostruire l’esatto percorso di ragionamento del modello.
Che cosa verifica Lean
Lean è un assistente di dimostrazione: controlla una prova formale rispetto all’enunciato codificato. Quel controllo, da solo, non dimostra che l’enunciato formalizzato corrisponda esattamente a quello scritto nell’articolo matematico. È su questa corrispondenza che si concentra l’analisi di A. Bastounis, F. Circelli e A. C. Hansen, pubblicata il 6 ottobre 2026.
Nel Lemma 8.6: quattro derivate nel testo, cinque in Lean
Gli autori confrontano l’equazione (8.19) del Lemma 8.6 con la stima Lean corrispondente: nel testo in linguaggio naturale il limite usa quattro derivate aggiuntive dell’input, mentre nella stima Lean esaminata ne usa cinque. Gli autori descrivono la stima Lean come più debole rispetto a quella formulata nell’articolo. È una discrepanza in un passaggio intermedio, non una conclusione sulla falsità del risultato finale.
| Versione confrontata | Derivate aggiuntive dell’input | Passaggio |
| Enunciato in linguaggio naturale | 4 | Lemma 8.6, equazione (8.19) |
| Stima Lean esaminata | 5 | Stima corrispondente del Lemma 8.6 |
L’analisi di Bastounis, Circelli e Hansen esamina anche la stima del flusso di pressione nell’equazione (10.19): le due formulazioni impiegano termini e ipotesi differenti, e gli autori giudicano difficile confrontarle direttamente. Il loro studio riguarda la fedeltà della formalizzazione Lean al testo; non sostiene che la prova di OpenAI in linguaggio naturale sia falsa.
Che cosa afferma OpenAI di aver dimostrato
Nell’annuncio dell’8 settembre 2026, OpenAI ha sostenuto che il suo risultato dimostra gli enunciati C e D della formulazione del problema di Navier–Stokes del Clay Mathematics Institute. La costruzione descritta dall’azienda riguarda un fluido incomprimibile tridimensionale, a densità costante, inizialmente regolare e fermo, sottoposto a una forza esterna regolare; secondo OpenAI, può svilupparsi una singolarità in tempo finito pur mantenendo energia finita. È dunque una costruzione con forza esterna, come specifica l’annuncio dell’azienda.
