Navier-Stokes, OpenAI rivendica la soluzione: adesso tocca ai matematici

OpenAI sostiene di aver ottenuto una soluzione al problema del millennio sulla regolarità delle equazioni di Navier-Stokes attraverso un sistema composto da molti agenti AI. La notizia OpenAI e Navier-Stokes sarebbe storica se la dimostrazione superasse la verifica indipendente della comunità matematica.

La cautela è parte della notizia, non una nota a margine. Un risultato matematico non diventa vero perché annunciato da un laboratorio famoso, né perché formalizzato da un altro modello. Deve essere esaminato, compreso e validato da specialisti indipendenti secondo le procedure della disciplina.

OpenAI e Navier-Stokes: 88 ore e milioni di messaggi

Nel proprio resoconto ufficiale, OpenAI afferma che gli agenti hanno raggiunto la soluzione dopo circa 88 ore dall’avvio del lavoro sul problema. La successiva formalizzazione e verifica in Lean, realizzata con GPT-6 Astra, avrebbe richiesto altre 17 ore.

Il dato più interessante non è soltanto la potenza del singolo modello, ma l’organizzazione del calcolo. OpenAI parla di circa 2,7 milioni di messaggi e 130 miliardi di token di output per il lavoro dedicato a Navier-Stokes. È ricerca trattata come un sistema distribuito: molti tentativi, verifiche, diramazioni e consolidamento finale.

La formalizzazione in Lean non sostituisce la verifica scientifica

Lean permette di controllare formalmente passaggi logici rispetto a un insieme di assiomi e definizioni. È uno strumento potentissimo contro errori nascosti in dimostrazioni molto lunghe. Ma rimane necessario stabilire che la formalizzazione rappresenti correttamente il problema, che le ipotesi siano appropriate e che l’intera catena sia leggibile e valutabile dalla comunità.

In altre parole, “il computer ha verificato” non è la nuova versione di ipse dixit. La matematica moderna usa da tempo software e proof assistant, ma la credibilità di un risultato nasce dalla possibilità di controllarlo indipendentemente, non dal logo sulla pagina che lo annuncia.

Perché conta anche oltre questo singolo problema

Se il risultato reggesse, la conseguenza più grande potrebbe essere metodologica. Sistemi di agenti capaci di esplorare uno spazio di ricerca matematico per giorni, scambiarsi risultati e produrre una prova formalizzata cambierebbero il rapporto tra matematici e calcolo. L’AI passerebbe da strumento che suggerisce idee a infrastruttura che sostiene campagne di ricerca.

Per ora, però, la formula più corretta resta “OpenAI rivendica”. È meno spettacolare di “l’AI ha risolto un problema del millennio”, ma ha un vantaggio raro nell’era dell’intelligenza artificiale: lascia ancora un po’ di lavoro agli esseri umani. In questo caso, per fortuna, proprio quello decisivo.