Equazioni di Navier Stokes, perché la CFD aeronautica resta un mestiere di taratura

Ogni ala che arriva in produzione ha attraversato centinaia di simulazioni fluidodinamiche, e tutte poggiano sulle equazioni di Navier-Stokes. Nessuna di quelle simulazioni le risolve. Il solutore che gira nell'ufficio aerodinamico calcola una versione mediata delle equazioni, chiude con un modello tarato su misure sperimentali i termini che restano aperti dopo la media, e poi il profilo finisce in galleria del vento perché qualcuno verifichi di quanto si è sbagliato. La ragione di questo modo di lavorare sta a monte del calcolatore, e riguarda il fatto che nessuno sa se quelle equazioni ammettano sempre una soluzione regolare.

L'8 settembre 2026 OpenAI ha dichiarato di aver chiuso la questione, sostenendo che una singolarità in tempo finito può formarsi. La vicenda ha una parte tecnica e una parte di attribuzione, e la seconda è ingarbugliata; chi cerca la ricostruzione puntuale delle rivendicazioni concorrenti la trova nella verifica di cosa sia stato dimostrato davvero pubblicata su ScienceCue. Qui interessa un'altra domanda. Perché un ufficio tecnico aeronautico convive da decenni con un'equazione di cui nessuno conosce la teoria, e che cosa un risultato del genere sposta, o non sposta, dentro un ciclo di progetto.

Punti chiave

• Il numero di elementi richiesti da una simulazione numerica diretta cresce come il numero di Reynolds elevato a nove quarti, e a un Reynolds di crociera dell'ordine di dieci milioni servirebbe una griglia da qualche milione di miliardi di punti.

• Il modello di turbolenza a una equazione di Spalart e Allmaras è stato presentato al trentesimo Aerospace Sciences Meeting dell'AIAA nel gennaio 1992, con costanti fissate su dati sperimentali e alcune modificate nella versione del 1994.

• Le formulazioni (C) e (D) dell'enunciato di Fefferman ammettono una forzante liscia, mentre (A) e (B) richiedono forzante identicamente nulla, e OpenAI rivendica (C) e (D).

• Caffarelli, Kohn e Nirenberg hanno dimostrato nel 1982 che l'insieme singolare di una soluzione debole adatta ha misura di Hausdorff parabolica unidimensionale nulla, quindi non può contenere una curva nello spazio-tempo.

• La formalizzazione e la verifica in Lean sono state completate in diciassette ore con GPT-6 Astra, dopo circa ottantotto ore di lavoro di diecimila agenti in parallelo e 2,7 milioni di messaggi scambiati.

• Il premio del Clay Mathematics Institute richiede pubblicazione in una sede qualificata, due anni di attesa e accettazione generale della comunità matematica, e OpenAI ha dichiarato di non volerlo rivendicare.

Che cosa chiede davvero il problema del millennio

Il testo ufficiale del problema, redatto da Charles Fefferman per il Clay Mathematics Institute, ammette quattro formulazioni alternative. Le prime due, indicate come (A) e (B), chiedono di dimostrare che per un fluido incomprimibile tridimensionale con dato iniziale liscio e forzante identicamente nulla esistono soluzioni lisce per ogni tempo, sull'intero spazio oppure sul toro periodico. Le altre due, (C) e (D), chiedono l'opposto, cioè di esibire un dato iniziale liscio e una forzante liscia con decadimento controllato per i quali una soluzione regolare non esista. La forzante entra per esplicita concessione dell'enunciato, e la distinzione conta, perché parte del dibattito di questi giorni l'ha ignorata.

Jean Leray nel 1934 aveva già dimostrato che soluzioni in senso debole esistono sempre. Il punto aperto è se restino lisce. Una soluzione debole soddisfa l'equazione integrata contro funzioni di prova, quindi ammette oggetti che un progettista non riconoscerebbe come flussi, e in tre dimensioni la sua unicità non è nota.

Il risultato annunciato da OpenAI, presentato in un writeup accompagnato da una formalizzazione in Lean, rivendica (C) e anche (D). Nella descrizione dell'azienda la soluzione è un vortice che si avvolge verso l'interno allungandosi, con la regione centrale che si restringe accelerando in modo tale che l'energia resti finita. Levent Alpöge e Tristan Buckmaster avevano pubblicato il giorno prima blowup con forzante liscia per l'equazione dei media porosi incomprimibili, per il sistema di Boussinesq bidimensionale e per Euler tridimensionale, anch'essi con verifica in Lean. Terence Tao, commentando quel lavoro sul proprio blog il 7 settembre, ha osservato che la comunità si attendeva da tempo la costruibilità di dati e forzanti lisci capaci di generare singolarità, e ha attribuito la strategia originaria a Diego Córdoba e Luis Martínez-Zoroa.

Perché la simulazione diretta non è un'opzione

Landau e Lifshitz stimarono nel 1959 che il numero di elementi necessari a risolvere un flusso turbolento fino alla scala di Kolmogorov cresce come il numero di Reynolds elevato a nove quarti. La stima compare ancora nella letteratura sulla risoluzione spaziale delle simulazioni numeriche dirette, e basta applicarla per capire dove finisce il discorso. Su un'ala di velivolo da trasporto il numero di Reynolds basato sulla corda in crociera è dell'ordine di dieci milioni, e quella potenza restituisce una griglia da qualche milione di miliardi di punti. Nessun calcolatore esistente si avvicina a quell'ordine di grandezza.

Da questo divario nasce l'intera architettura della fluidodinamica computazionale industriale. Le equazioni si mediano nel tempo, ottenendo la formulazione RANS, e gli sforzi turbolenti che sopravvivono alla media vanno chiusi con un modello. Oppure si risolvono le scale grandi e si modella il sottogriglia, ed è la LES, pesante e ancora fuori portata per un velivolo intero ai numeri di Reynolds di volo. In mezzo stanno gli approcci ibridi e la LES con modello di parete, che rinuncia a risolvere la regione vicina alla superficie e la sostituisce con una legge di parete, tagliando la parte più costosa del conto.

Un caso concreto dice quanto questa architettura sia empirica. Nella giunzione fra ala e fusoliera si forma una separazione d'angolo che i modelli RANS a viscosità turbolenta lineare prevedono in modo incoerente, e la NASA ha allestito un esperimento apposta per avere dati con cui tararli, il Juncture Flow Experiment, condotto nella galleria subsonica 14 per 22 piedi di Langley su un modello con ala DLR-F6 troncata a un numero di Reynolds basato sulla corda di 2,4 milioni. Fra i coautori del lavoro di validazione compare Philippe Spalart, lo stesso del modello di turbolenza più diffuso in aerodinamica esterna. Un settore che deve costruire una campagna di galleria del vento per sapere se il proprio solutore azzecca la separazione in un angolo sta dicendo con chiarezza dove si trova il limite della teoria.

Le chiusure di turbolenza sono modelli tarati

La chiusura più diffusa in aerodinamica esterna, il modello a una equazione di Spalart e Allmaras, è stata presentata nel gennaio 1992 al trentesimo Aerospace Sciences Meeting dell'AIAA con un titolo che dichiara la propria destinazione, "A One-Equation Turbulence Model for Aerodynamic Flows". Le costanti sono state fissate su misure sperimentali e su flussi di riferimento, e la versione uscita nel 1994 su La Recherche Aérospatiale ne ha cambiate alcune rispetto al paper di conferenza. Un modello così non discende dalle equazioni. Le approssima in un intervallo di condizioni dove è stato validato, e fuori da quell'intervallo nessuno garantisce niente.

L'assenza di una teoria di esistenza e regolarità pesa qui, e pesa in modo molto concreto. Senza teoria non esiste una stima d'errore a priori per il solutore. Il progettista non può dimostrare che la propria soluzione numerica approssimi una soluzione vera, perché non sa se una soluzione vera esista. Quello che gli resta è confrontare, tarare, ripetere in galleria del vento e accumulare campagne di validazione. La certificazione per analisi, cioè la sostituzione parziale delle prove sperimentali con la simulazione, avanza lentamente proprio per questa ragione, e la quantificazione dell'incertezza sui parametri dei modelli di turbolenza è diventata un filone di ricerca a sé.

Quando il continuo si rompe, l'aerospazio lo fa già

Una singolarità significa velocità che crescono senza limite in un punto e in un tempo finito. Un fluido reale non può muoversi a velocità infinita, quindi il messaggio fisico è che il modello di mezzo continuo cede e che per continuare a descrivere il sistema bisogna seguire le singole molecole. Lo scrive la stessa nota di OpenAI. Per chi progetta veicoli di rientro quella frase descrive una condizione di lavoro ordinaria.

Il parametro che decide è il numero di Knudsen, rapporto fra libero cammino medio molecolare e lunghezza caratteristica del corpo. Finché resta piccolo le equazioni di Navier-Stokes descrivono il flusso. Quando cresce, l'ipotesi di equilibrio locale cade, e le relazioni costitutive che legano sforzo viscoso e flusso termico ai gradienti perdono validità. In alta atmosfera e nelle prime fasi di un rientro il regime esce dal continuo, e allora si passa a metodi particellari.

Il più usato è il Direct Simulation Monte Carlo introdotto da Graeme Bird, che sostituisce il mezzo continuo con particelle rappresentative e ne simula moto e collisioni per risolvere numericamente l'equazione di Boltzmann. Il Langley Research Center della NASA lo ha applicato alla capsula Apollo nel regime ipersonico rarefatto tipico della fase alta del rientro, ancorando i risultati in regime continuo a simulazioni Navier-Stokes. Gli schemi ibridi fanno convivere i due mondi nello stesso calcolo, usando criteri di rottura del continuo per decidere dove collocare l'interfaccia, e quei criteri sono a loro volta empirici o semi-empirici. La progettazione di uno scudo termico vive in questa zona di confine, come mostrano le scelte di materiale e di margine che accompagnano i sistemi di protezione termica per il rientro atmosferico.

Quello che una singolarità dimostrata non cambia in un solutore

La singolarità di cui si discute è costruita. Richiede una forzante progettata con cura, con regolarità e decadimento scelti per far funzionare l'argomento, e vive in un fluido incomprimibile a densità costante, senza pareti, senza compressibilità, senza chimica, senza scambio termico. Nessuna di queste condizioni somiglia all'aria intorno a un profilo alare in transonico. Il fenomeno non è osservabile, non è misurabile e non compare in nessuna campagna sperimentale.

Esiste poi un risultato che spiega perché gli ingegneri hanno potuto convivere serenamente con il problema per oltre quarant'anni. Nel 1982 Luis Caffarelli, Robert Kohn e Louis Nirenberg dimostrarono che una soluzione debole adatta delle equazioni di Navier-Stokes è liscia fuori da un insieme la cui misura di Hausdorff parabolica unidimensionale è nulla. In termini pratici l'eventuale insieme singolare risulta talmente sottile da non poter contenere nemmeno una curva nello spazio-tempo. Fefferman lo richiama nel proprio enunciato come il miglior teorema di regolarità parziale disponibile, e aggiunge che andare oltre sembra molto difficile.

Una conferma del risultato non toglierebbe una riga a un solutore RANS e non modificherebbe una taratura. Il valore sta nella teoria delle equazioni alle derivate parziali, dove chiuderebbe una domanda aperta da novant'anni e indicherebbe che la regolarità globale va cercata altrove. Il caso senza forzante resta aperto per Navier-Stokes, e vale la pena notare che il risultato su Euler rivendicato dagli stessi agenti riguarda invece la versione priva di forze esterne.

Metodi formali, un linguaggio che la certificazione conosce già

Lean, l'assistente di dimostrazione usato per formalizzare entrambi i lavori, appartiene a una famiglia di strumenti che l'industria aeronautica ha incontrato per ragioni completamente diverse. La DO-178C, adottata nel 2011 come riferimento per il software avionico, porta con sé un supplemento dedicato, la DO-333, che stabilisce come i metodi formali possano soddisfare obiettivi di verifica al posto del test o accanto a esso. L'analizzatore Astrée è stato impiegato per verificare l'assenza di errori a run time nel codice C del sistema di controllo di volo dell'A380, e il linguaggio SPARK ha permesso di sostituire parte dei test unitari con analisi formale in progetti Airbus e Dassault Aviation. Fuori dall'avionica esistono un compilatore C dimostrato corretto, CompCert, e un microkernel con proprietà verificate, seL4.

Chi lavora nell'assicurazione del software riconosce quindi il gesto, e la domanda interessante riguarda la scala dei tempi. La formalizzazione e la verifica in Lean dell'argomento di OpenAI hanno richiesto diciassette ore di calcolo con GPT-6 Astra, su una dimostrazione che nessun revisore umano avrebbe letto in un giorno. In un settore dove il collo di bottiglia di un programma è spesso il ciclo di verifica e la produzione delle evidenze di certificazione, quel rapporto fra lunghezza dell'argomento e tempo di controllo meccanico merita attenzione.

Va però tenuta ferma una precisazione che nel settore è pane quotidiano. Una verifica formale certifica che le conclusioni seguono dalle premesse scritte nel modello, e tace completamente sul fatto che quelle premesse descrivano il sistema che si voleva descrivere. Chi distingue per mestiere fra verifica e validazione riconosce il punto al primo colpo. Nel caso di Navier-Stokes la premessa sotto esame è la corrispondenza fra l'enunciato formalizzato in Lean e la formulazione di Fefferman, e quel confronto è esattamente il controllo indipendente che la comunità matematica ha appena iniziato.

Diecimila agenti e il conto del calcolo

I numeri dichiarati da OpenAI raccontano una scala industriale. Il gruppo di agenti che ha prodotto il risultato ne contava circa diecimila operanti in parallelo, con accesso a una copia in cache della rete e alla possibilità di eseguire codice. Sono arrivati alla soluzione il 5 settembre, circa ottantotto ore dopo l'avvio, dopo che il progetto era stato riorientato su Navier-Stokes in seguito alla risoluzione inattesa del problema di regolarità per Euler, ottenuta da un centinaio di agenti in una cinquantina di ore. Sul solo Navier-Stokes gli agenti si sono scambiati 2,7 milioni di messaggi e hanno prodotto circa 130 miliardi di token in uscita.

Sul costo l'azienda non ha pubblicato una cifra, ma il direttore della ricerca Mark Chen lo ha collocato nell'ordine dei milioni di dollari parlando con la stampa, come riportato dalla rivista Science. Nello stesso articolo Karthik Duraisamy dell'Università del Michigan stima circa sei milioni di dollari ai prezzi di listino degli strumenti OpenAI e circa un milione di dollari di calcolo di inferenza per chi possiede già modello e infrastruttura, cifra che coincide con l'ammontare del premio. OpenAI ha dichiarato di non volerlo rivendicare, e le regole del Clay lo renderebbero comunque irraggiungibile per ora, dato che richiedono pubblicazione in una sede qualificata, due anni di attesa e accettazione generale nella comunità matematica mondiale.

Un ufficio tecnico che oggi volesse comprare quella capacità non troverebbe nulla sul mercato. Il modello impiegato è interno e ancora in addestramento, il costo per singolo problema si misura in milioni, e il rendimento è stato ottenuto su una domanda con enunciato chiuso e verificabile in modo meccanico, condizione che un problema di progetto aerodinamico non possiede quasi mai. Le informazioni su questa vicenda sono aggiornate al 9 settembre 2026, e nelle settimane successive sono attese la verifica indipendente della corrispondenza fra enunciato Lean e formulazione di Clay ed eventuali repliche.

Resta un dettaglio che dice quanto queste equazioni diventino strane appena si esce dal terreno delle soluzioni lisce. Nel testo ufficiale del problema Fefferman ricorda una costruzione di Vladimir Scheffer, poi ripresa da Alexander Shnirelman, che produce soluzioni deboli delle equazioni di Euler a supporto compatto nello spazio-tempo. Descrive un fluido che sta fermo, comincia a muoversi da solo senza nessuno stimolo esterno e torna fermo poco dopo, con il moto sempre confinato in una palla. È matematicamente lecito e fisicamente assurdo, e ricorda che la nozione di soluzione con cui si lavora conta esattamente quanto l'equazione.

Domande frequenti

Le equazioni di Navier-Stokes servono davvero a progettare gli aerei?

Sì, ogni simulazione fluidodinamica usata per dimensionare un'ala, una presa d'aria o una gondola motore parte dalle equazioni di Navier-Stokes. Il solutore però non le risolve nella forma esatta, perché lavora su una versione mediata nel tempo e affida i termini turbolenti residui a un modello di chiusura tarato su misure di galleria del vento.

Che cosa cambia per la CFD aeronautica se Navier-Stokes ammette una singolarità?

Sul piano operativo non cambia niente. La singolarità costruita richiede una forzante progettata a tavolino in un fluido incomprimibile idealizzato, senza pareti né compressibilità, quindi non descrive alcun flusso reale intorno a un velivolo. Nessun solutore RANS, nessuna mesh e nessuna taratura di modello vanno riscritti in conseguenza del risultato.

Perché non si risolvono direttamente le equazioni di Navier-Stokes in una simulazione?

Perché il numero di celle necessarie a risolvere tutte le scale della turbolenza cresce come il numero di Reynolds elevato a nove quarti. Su un'ala in crociera, con Reynolds dell'ordine di dieci milioni, la griglia richiesta arriva a qualche milione di miliardi di punti, molto oltre le simulazioni dirette più grandi mai eseguite.

Quando le equazioni di Navier-Stokes smettono di valere in aerodinamica?

Quando il numero di Knudsen, rapporto fra libero cammino medio molecolare e dimensione del corpo, diventa abbastanza grande da far cadere l'ipotesi di equilibrio locale. Succede in alta atmosfera e nella fase iniziale di un rientro, dove si passa a metodi particellari come il Direct Simulation Monte Carlo introdotto da Graeme Bird.

I metodi formali come Lean sono già usati nella certificazione aeronautica?

La DO-333, supplemento sui metodi formali della DO-178C adottata nel 2011, definisce come impiegarli per soddisfare obiettivi di verifica del software avionico. Astrée è stato usato sul codice di controllo di volo dell'A380 e SPARK in progetti Airbus e Dassault Aviation, mentre Lean appartiene alla stessa famiglia di strumenti dimostrativi.

OpenAI ha vinto il premio da un milione di dollari per Navier-Stokes?

No, e ha dichiarato di non volerlo rivendicare. Le regole del Clay Mathematics Institute impongono la pubblicazione in una sede qualificata, almeno due anni di attesa e l'accettazione generale nella comunità matematica mondiale. La verifica indipendente della corrispondenza fra enunciato formalizzato in Lean e formulazione ufficiale è appena iniziata.