Navier–Stokes en het bewijs in Lean: geforceerde singulariteiten en de ondoorzichtigheid van het lab

Op 8 september 2026 verklaarde OpenAI dat een eigen intern model, dat nooit publiek is uitgebracht, een bewijs heeft geproduceerd van blowup in eindige tijd voor de driedimensionale incompressibele Navier–Stokes-vergelijkingen. Het bedrijf verspreidde het theoretische document samen met de openbare repository NavierStokesAndEuler, die de formalisering in de taal Lean 4 bevat van de stellingen over gladde begindata onder een externe forceringsterm. Volgens de reconstructie van het lab dekt het resultaat de uitspraken over het verlies van regulariteit uit de formulering die de wiskundige Charles Fefferman voor het Clay Mathematics Institute opstelde, zonder echter het geval zonder externe kracht te behandelen — door de wetenschappelijke gemeenschap gezien als de moeilijkste variant van het probleem. De auteur van de officiële formulering noemde de oplossing opwindend en verwees naar de bijdragen van Córdoba en Martínez-Zoroa, terwijl het bedrijf meteen duidelijk maakte de prijs van een miljoen dollar niet te willen opeisen.

De operatie verweeft wiskundige automatisering met het tempo van academische instellingen. Het Clay Mathematics Institute rekent Navier–Stokes nog altijd tot de onopgeloste problemen: het reglement vereist publicatie op een gekwalificeerde plek, een wachttijd van minstens twee jaar na publicatie en algemene aanvaarding door de wiskundige gemeenschap, en het instituut heeft zich inhoudelijk tot dusver niet uitgesproken. Voorzitter Martin Bridson herinnerde eraan dat de beoordeling met opzet een onhaastig ritme volgt, om absolute striktheid te waarborgen. Het beeld wordt verder gecompliceerd door een prioriteitskwestie rond parallel werk dat de wiskundige Terence Tao heeft toegelicht en dat door de auteurs wordt omschreven als sterk door kunstmatige intelligentie ondersteund. Een wiskundige van de New York University betwistte de weergave van de contacten die het lab gaf, en opperde dat privésessies met een propriëtair hulpmiddel aan de uitkomst kunnen hebben bijgedragen; het bedrijf ontkent het ongepubliceerde werk rechtstreeks te hebben gezien, maar geeft toe niet te kunnen uitsluiten dat gede-identificeerde gebruiksdata invloed hadden op de training van de eigen modellen.

De repository bevat de instructies om het bewijs machinaal te laten hercontroleren, maar er is tot nu toe geen onafhankelijke verificatie afgerond; los van die controle verhindert het propriëtaire karakter van de gebruikte infrastructuur elke onafhankelijke toetsing van de kosten en de rondgebazuinde efficiëntiecijfers. De opgegeven rekeninzet — zo'n tienduizend gelijktijdige agenten tussen 1 en 5 september, 88 uur tot het bewijs en nog eens 17 voor de formalisering en de Lean-verificatie — blijft een bedrijfsclaim die van buitenaf niemand kan reproduceren. Zonder toegang tot de trainingscode of tot de gewichten van het systeem kan de wetenschappelijke gemeenschap uitsluitend de formele stappen in de repository valideren, terwijl de werkelijke reproduceerbaarheid van het experiment in het duister blijft.

De formele wiskunde heeft in de automatische controle van logische stappen een geduchte bondgenoot gevonden, maar de race om wetenschappelijke voorrang via gesloten modellen toont haar structurele grenzen. Een stelling verifiëren is inmiddels werk voor een machine; vaststellen hoe transparant de keten is die haar voortbracht, vergt nog altijd een volstrekt menselijke striktheid.

— Olya