AI helpt wiskundigen aan bewijs voor Euler-vergelijkingen

Twee wiskundigen hebben deze week een resultaat gepubliceerd dat al jaren buiten bereik lag: het bewijs dat de driedimensionale incompressibele Euler-vergelijkingen in eindige tijd kunnen exploderen, ook bij een gladde krachtterm. Opvallend is hoe het bewijs tot stand kwam. Levent Alpöge, onderzoeker bij Anthropic, en Tristan Buckmaster van New York University leunden zwaar op taalmodellen, en lieten de uitkomst daarna volledig machinaal controleren in Lean.

Terence Tao, Fields-medaillewinnaar en een van de bekendste namen in dit vakgebied, noemde het werk op zijn blog een remarkable achievement. Hij belde Buckmaster op om het door te spreken.

Wat er precies bewezen is

Alpöge en Buckmaster maakten drie resultaten openbaar: blow-up in eindige tijd met gladde forcering voor de incompressibele poreuze-mediavergelijking, voor Boussinesq, en voor 3D Euler. Ze bouwen daarmee voort op werk van Diego Córdoba en Luis Martínez-Zoroa, die eerder lieten zien dat zo’n singulariteit kon ontstaan bij ruwere, fysisch minder realistische krachttermen. De stap naar een gladde term is de moeilijke versie, en juist die maakt het resultaat interessant.

Tao schrijft dat hij geen duidelijk obstakel ziet om deze methoden richting Navier-Stokes uit te breiden. Wel temperde hij de verwachtingen: de officiele Millennium Prize-opgave gaat over vloeistoffen zonder externe kracht, en tussen dat punt en het huidige resultaat staat volgens hem nog een flink aantal technische hordes.

De rol van de modellen, en van Lean

De auteurs zetten Claude in om zich door de bestaande literatuur te werken, en gebruikten Claude en Codex-gebaseerde modellen van OpenAI voor het opstellen van argumenten en het bijhouden van constanten en inductiestappen, steeds onder menselijke regie. Buckmaster en Alpöge zijn er zelf openhartig over dat de eerste versie onleesbaar was. Ze omschreven hun eigen concept als de slechtste uitwerking die ze ooit in de wiskunde hadden gezien, en besteedden weken aan herschrijven.

Daar zit meteen het antwoord op de voor de hand liggende twijfel. De kern van Euler, Boussinesq en IPM is nagerekend in Lean, een systeem dat regel voor regel controleert of een redenering sluit. Een model dat overtuigend klinkt maar een gat in de logica laat, komt daar niet doorheen. Dezelfde combinatie zagen we eerder toen Claude de stelling van Fermat in Lean formaliseerde en bij het werk waarmee de Riemann-ondergrens werd opgeschoven.

Ruzie over de eer

Rond de publicatie ontstond een conflict. Buckmaster zegt dat OpenAI-onderzoeker Sébastien Bubeck hem twee scenario’s voorlegde, waaronder een waarin Buckmaster alleen zou publiceren met krediet voor een OpenAI-model, en dat Bubeck er tweemaal op aandrong Alpöge weg te laten vanwege diens dienstverband bij Anthropic. Toen Buckmaster weigerde en dreigde ermee naar buiten te treden, kreeg hij naar eigen zeggen te horen: waarom zou je je carriere ruïneren. OpenAI zou intern een bewijs van zo’n honderd pagina’s hebben laten genereren langs vergelijkbare lijnen. Buckmaster benadrukt dat hij dat stuk niet heeft gezien en niemand van concreet wangedrag beschuldigt. Anthropic en OpenAI hadden bij publicatie niet gereageerd. De twee bedrijven staan de laatste tijd vaker tegenover elkaar, onder meer in het wetgevingsdebat in Massachusetts.

Wat betekent dit

Voor wie AI-claims volgt is dit een nuttig ijkpunt. Niet omdat een model iets zou hebben opgelost, maar omdat de rolverdeling zichtbaar wordt: modellen leveren snelheid en volume, mensen bepalen de richting, en Lean beslist of het klopt. Die derde stap ontbreekt bij vrijwel alle spectaculaire wiskundeclaims die de afgelopen maanden voorbijkwamen, inclusief de benchmarkcijfers die OpenAI na de lancering van Astra bijstelde. Wie de komende tijd leest dat een model een groot probleem heeft gekraakt, kan dus beginnen met een simpele vraag: is het geformaliseerd, en zo ja, waarin? Het gevecht om de credits laat daarnaast zien hoeveel prestige de labs aan dit soort resultaten hechten, en dat maakt onafhankelijke verificatie eerder belangrijker dan minder.