L’8 settembre OpenAI ha annunciato una soluzione al problema di esistenza e regolarità delle equazioni di Navier-Stokes, pubblicando una dimostrazione e la sua formalizzazione in Lean. È un’affermazione di grande rilievo per la ricerca matematica. Per capirne la portata serve però precisare quale risultato viene rivendicato e come può essere controllato.
Nel testo dell’annuncio, l’azienda attribuisce la scoperta a un sistema basato su un modello interno, descritto come più capace di GPT-6 Astra. Non è una funzione che quel comunicato rende disponibile agli utenti di ChatGPT.
Quale problema viene affrontato?
Le equazioni di Navier-Stokes descrivono il moto dei fluidi. Una delle grandi domande matematiche riguarda la possibilità che un moto inizialmente regolare sviluppi una singolarità in un tempo finito: un punto in cui la descrizione perde determinate proprietà di regolarità.
OpenAI sostiene di aver costruito un caso con una forza esterna regolare applicata al fluido. Nel repository pubblico della formalizzazione, il risultato è collegato alle alternative C e D della formulazione del Clay Mathematics Institute. La presenza della forza esterna è quindi parte dell’enunciato da valutare. Liquidarla come un dettaglio estraneo al problema sarebbe impreciso quanto ometterla del tutto.
Questo aiuta anche a evitare una lettura troppo ampia. Una dimostrazione di singolarità, nelle condizioni descritte, non offre automaticamente un metodo per prevedere ogni flusso turbolento o per migliorare qualsiasi simulazione industriale. Per arrivare a un’applicazione servirebbero altri passaggi, da documentare separatamente.
Che cosa aggiunge Lean?
Lean consente di esprimere enunciati e dimostrazioni in una forma che un sistema informatico può controllare. Pubblicare la formalizzazione mette a disposizione un oggetto verificabile, oltre al testo destinato ai matematici. Il repository di OpenAI include istruzioni per costruirla e rimanda a controlli indipendenti con Comparator.
La verifica formale va letta insieme all’enunciato: quali ipotesi sono state tradotte, che cosa viene dimostrato esattamente e come quel risultato corrisponde alla domanda originaria. Chi controlla il lavoro deve poter seguire anche questo collegamento.
In questo articolo abbiamo consultato l’annuncio e la documentazione pubblicata. Non abbiamo eseguito il controllo della formalizzazione né revisionato la dimostrazione matematica. La correttezza del risultato resta quindi un’affermazione che attribuiamo agli autori, senza presentare la nostra lettura come una validazione scientifica.
Il riconoscimento del premio segue regole proprie
Il Clay Mathematics Institute prevede condizioni specifiche prima di considerare una soluzione per il premio: pubblicazione in una sede qualificata, almeno due anni da quella pubblicazione e accettazione generale nella comunità matematica mondiale.
Sono criteri per l’assegnazione del premio. Il mancato riconoscimento immediato, da solo, non dimostra che un argomento sia sbagliato. Allo stesso modo, un annuncio aziendale non equivale a quel riconoscimento. OpenAI dichiara inoltre di non voler richiedere il Millennium Prize per questo risultato.
La notizia da seguire adesso
Il materiale pubblicato permette di spostare l’attenzione sui controlli: quali verifiche vengono completate da soggetti indipendenti e quale giudizio emerge sul rapporto tra la prova e il problema formulato dal Clay.
Per chi segue l’AI, questa vicenda è interessante anche come caso di comunicazione della ricerca. La dimensione dell’annuncio invita a un verdetto immediato, mentre il lavoro disponibile consente domande più precise. Le prossime notizie utili saranno quelle che aggiungeranno un controllo riproducibile o un chiarimento matematico, con il relativo documento da leggere.
