Equazioni di Eulero, l’AI aiuta a dimostrare il blow-up in tempo finito e Tao parla di un risultato notevole

Per la prima volta un blocco di risultati di punta sulla fluidodinamica arriva insieme a due elementi che fino a pochi anni fa sembravano estranei alla matematica pura: un contributo massiccio dei modelli di intelligenza artificiale e una verifica formale al computer. A firmare il lavoro sono Tristan Buckmaster, della New York University, e Levent Alpöge, matematico legato ad Anthropic, che affermano di aver dimostrato il cosiddetto blow-up in tempo finito per alcune tra le equazioni più studiate della dinamica dei fluidi.

La notizia ha fatto discutere non solo per il contenuto tecnico, ma anche perché a commentarla è stato Terence Tao, medaglia Fields e tra i matematici viventi più autorevoli, che ha parlato di un risultato notevole. Un giudizio che pesa, perché Tao è tra le pochissime persone al mondo in grado di valutare davvero la solidità di un lavoro del genere.

Che cosa significa blow-up e perché conta

Prima di capire perché questo annuncio è importante, ti conviene fissare un’idea. Il blow-up in tempo finito descrive una situazione in cui una grandezza fisica, per esempio la velocità o la sua variazione in un punto del fluido, smette di restare limitata e schizza verso l’infinito in un intervallo di tempo finito. In parole semplici, il modello matematico che dovrebbe descrivere il fluido a un certo istante si rompe e smette di avere senso.

Capire se e quando le equazioni della fluidodinamica possono comportarsi così è una delle domande centrali del settore. Non è un esercizio astratto: riguarda la stessa affidabilità dei modelli con cui descriviamo l’aria, l’acqua e qualsiasi fluido in movimento.

Buckmaster e Alpöge affermano di aver dimostrato che tre equazioni molto note, l’equazione di Eulero incomprimibile in tre dimensioni, l’equazione di Boussinesq e l’equazione dei mezzi porosi incomprimibili nota con la sigla inglese IPM, possono sviluppare un blow-up quando viene applicata una forza esterna liscia, cioè regolare in senso matematico.

Il dettaglio della forza liscia è il cuore della questione.

Perché la forzante liscia cambia tutto

Il risultato si innesta su un programma di ricerca pluriennale portato avanti dai matematici Diego Córdoba e Luis Martínez-Zoroa, che in precedenza avevano mostrato come il blow-up fosse possibile solo con una forzante più ruvida, meno regolare e quindi meno realistica dal punto di vista fisico. Portare quella forza fino a renderla completamente liscia è la versione più difficile e più significativa del problema, ed è esattamente ciò che i due autori sostengono di aver raggiunto.

La differenza non è cosmetica. Una forzante liscia è molto più vicina a ciò che consideriamo un ingrediente fisicamente sensato, e avvicina il risultato al tipo di domande che i matematici si pongono davvero sulle equazioni non forzate.

Il ruolo dell’intelligenza artificiale e la verifica in Lean

La parte che rende questa storia diversa dalle solite dimostrazioni è il modo in cui è stata costruita. Gli argomenti, spiegano gli autori, sono stati sviluppati con un aiuto massiccio dei modelli di intelligenza artificiale e poi controllati con il sistema di verifica formale Lean, che funziona come una garanzia certificata dalla macchina: se il codice viene accettato, la catena logica della dimostrazione regge senza buchi.

Questo è importante perché una delle obiezioni classiche verso la matematica assistita dall’AI riguarda proprio l’affidabilità. Un modello linguistico può produrre passaggi convincenti ma sbagliati. La verifica in Lean sposta la fiducia dal testo, che può essere elegante o confuso, alla logica formale, che o è corretta o non compila.

Gli autori, per loro stessa ammissione, hanno passato le ultime settimane a riscrivere il materiale generato dall’AI in una forma più leggibile e di qualità professionale, così da renderlo comprensibile alla comunità matematica e non solo alle macchine.

Non è un caso isolato. Negli ultimi mesi su questo sito hai letto come Claude abbia contribuito a formalizzare in Lean l’ultimo teorema di Fermat e come un modello di OpenAI abbia affrontato dieci problemi aperti pubblicando le dimostrazioni sempre in Lean. Il filo conduttore è chiaro: l’AI non si limita più a suggerire idee, ma entra nel merito di dimostrazioni che vengono poi certificate in modo rigoroso.

Terence Tao parla di un risultato notevole

A dare peso alla vicenda è stato l’intervento di Terence Tao. Sul suo blog il matematico ha confermato il titolo tecnico della notizia: Alpöge e Buckmaster hanno preso l’approccio di Córdoba e Martínez-Zoroa e lo hanno spinto da una versione parziale, a regolarità sottocritica della forzante, fino a una versione completamente liscia, qualcosa che il lavoro precedente degli stessi autori non era riuscito a ottenere.

Tao ha sottolineato che gli argomenti sono stati formalizzati in Lean e ha aggiunto un dettaglio curioso: per farsi spiegare le idee ha parlato direttamente al telefono con Buckmaster, definendo quella conversazione umana un piacevole cambio di ritmo rispetto alla comunicazione mediata dall’AI. Ha comunque riconosciuto che le dimostrazioni si appoggiano in modo consistente a contenuti generati dai modelli.

Il matematico ha anche ricordato quanto lavoro tecnico serva per trasformare un’idea pulita in una dimostrazione a prova di errore: il solo articolo dedicato all’equazione di Boussinesq, la cugina più semplice di Eulero spesso usata come banco di prova, arriverebbe a settantasei pagine anche dopo i tentativi di accorciarlo.

Come funziona la dimostrazione, in parole semplici

Tao ha offerto una descrizione accessibile della strategia. Immagina di voler costruire un flusso che va fuori controllo. Il metodo di Córdoba e Martínez-Zoroa lo fa sovrapponendo piccole increspature localizzate ad alta frequenza a un flusso di fondo più ampio e regolare, a bassa frequenza, un po’ come aggiungere dettagli sempre più fini a uno schizzo. È un’idea affine alla cosiddetta integrazione convessa, una tecnica usata da anni per costruire soluzioni bizzarre delle equazioni dei fluidi.

La novità sta nella direzione in cui viaggia l’energia. Di solito c’è uno scambio in entrambi i sensi tra lo strato grossolano e quello fine. Qui invece non torna quasi nulla dalle increspature fini verso il fondo. Il flusso di fondo fa un solo lavoro: amplifica in modo esponenziale le increspature, spingendole finché, al momento giusto, diventano abbastanza forti da prendere il controllo e innescare il ciclo successivo di amplificazione. Ripeti il processo un numero sufficiente di volte, sempre più in fretta, e ottieni un vero blow-up in tempo finito.

Per l’equazione di Boussinesq, ha notato Tao, ampiezza e frequenza di queste increspature finiscono per seguire una regola matematica sorprendentemente semplice. Trasformare quell’idea elegante in una prova blindata resta però un enorme lavoro di contabilità tecnica.

La strada verso Navier-Stokes

La domanda che tutti si pongono è se questo metodo possa avvicinare la soluzione di Navier-Stokes, una delle equazioni fondamentali della fisica e uno dei sette problemi del millennio, il cui premio vale un milione di dollari. La posizione di Tao è di ottimismo prudente.

Il matematico ha detto di non vedere, nel metodo attuale, alcun ostacolo evidente che impedisca di estenderlo proprio a Navier-Stokes. Ha persino ipotizzato che la forzante possa in prospettiva essere eliminata del tutto, il che avvicinerebbe il risultato al vero problema del millennio, che chiede appunto cosa succede ai fluidi non forzati.

Attenzione però a non correre. Tao è stato altrettanto chiaro nel dire che tra il punto in cui siamo e quel traguardo restano moltissime difficoltà tecniche. Non si è detto sorpreso all’idea che qualcuno, con abbastanza potenza di calcolo e assistenza dell’AI, possa un giorno superarle, ma ha ammesso che macinare quell’estensione non lo appassiona particolarmente. Ciò che lo interessa davvero è digerire la nuova tecnica e capire quali idee genuinamente nuove contenga, a prescindere dal premio.

L’ombra della polemica con OpenAI

Attorno all’annuncio non c’è solo matematica. Nel rendere pubblici i risultati, Buckmaster ha accompagnato il lavoro con accuse pesanti verso OpenAI, sostenendo che l’azienda avrebbe tentato di fare pressione su di lui durante il processo di pubblicazione e di intestarsi parte del merito. Sono affermazioni al momento non confermate da OpenAI e vanno trattate come tali.

Secondo il racconto dei diretti interessati, proprio quella pressione avrebbe costretto gli autori a pubblicare prima di quanto avessero programmato, con le dimostrazioni ancora in fase di ripulitura. È un dettaglio che dice molto sul clima competitivo intorno alla matematica assistita dall’AI, dove i grandi laboratori vedono nei problemi aperti un banco di prova ideale per mostrare le capacità dei propri modelli.

Non è la prima volta che l’AI viene spinta a misurarsi con le vette del ragionamento tecnico. Di recente hai visto un modello di NVIDIA battere il miglior concorrente umano alle Olimpiadi internazionali di informatica, un altro segnale di quanto la corsa si stia spostando sul terreno della dimostrazione e del problem solving avanzato.

Che cosa cambia da qui in avanti

Al di là della singola dimostrazione, il messaggio di fondo è che sta cambiando il modo stesso in cui nasce un teorema. Fino a poco tempo fa una dimostrazione era un prodotto quasi interamente umano, discusso a voce e su carta. Oggi vediamo un intreccio inedito: idee suggerite dai modelli, riscritte da esseri umani e sigillate da un verificatore automatico come Lean.

Il giudizio prudente ma positivo di Tao aiuta a separare il segnale dal rumore. Nessuno sta dicendo che Navier-Stokes è risolto. Quello che possiamo dire è che la matematica alla base sembra reale, poggia su solide basi di verifica formale e rappresenta un avanzamento concreto su un problema difficile e molto studiato.

Se ti occupi di ricerca, di sviluppo di modelli o semplicemente segui l’evoluzione dell’AI, vale la pena tenere d’occhio questo filone. Continua a seguirci per capire, annuncio dopo annuncio, fino a che punto l’intelligenza artificiale sta davvero riscrivendo le regole della scoperta scientifica.