Hvad der faktisk blev bevist
Levent Alpöge og Tristan Buckmaster har offentliggjort tre preprints, der fastslår blowup på endelig tid med et glat drivende led for den inkompressible porøse medium-ligning, det todimensionale Boussinesq-system og de tredimensionale inkompressible Euler-ligninger.
Terence Tao skrev om resultaterne mandag og bemærkede, at argumenterne er “kraftigt AI-assisterede”, og at arbejdet også er formaliseret i Lean. Han tilskriver det underliggende program Diego Córdoba og Luis Martínez-Zoroa, som først tog tilfældet med porøst medium.
Blowup betyder, at ligningerne giver en løsning, hvis hastighed bliver uendelig på endelig tid — et matematisk sammenbrud, ikke et fysisk. At fastslå det for Euler med drivende led er et skridt mod det samme spørgsmål for Navier-Stokes, der bærer en millenniumpris fra Clay-instituttet.
AI-delen
Buckmaster er ved New York University. Alpöge er forsker i Anthropic. Ifølge Unite.AI oplyste de to, at de brugte Anthropics Claude og OpenAI’s Codex til bogføring af induktive ordener og konstanter og til trinvis forbedring af teksten.
De var åbne om kvaliteten af den prosa, modellerne producerede. Buckmaster beskrev den første AI-genererede tekst som “den mest rædselsfulde, jeg nogensinde har læst”, og forfatterne kaldte deres første udkast det dårligste, de havde set. Det er Lean-formaliseringen, der bærer vissheden: en bevisassistent godtager et argument eller gør det ikke.
Striden
I en udtalelse offentliggjort sammen med preprintene siger Buckmaster, at OpenAI fortalte ham, at en intern model havde produceret et cirka 100 sider langt bevis for blowup på endelig tid for de drevne Navier-Stokes-ligninger. Han beskriver to samtaler den 6. september med OpenAI-forskere, blandt dem Sébastien Bubeck.
Buckmaster siger, at OpenAI foreslog enten, at de to grupper udgav på hinanden følgende dage med OpenAI’s Navier-Stokes-resultat efter hans Euler-artikel, eller at han alene skrev Navier-Stokes-resultatet op og krediterede en unavngiven intern OpenAI-model, med Alpöge fjernet fra forfatterskabet — et punkt, Buckmaster knytter til Alpöges ansættelse i Anthropic. Han fortæller, at han efter sit afslag blev spurgt, hvorfor han ville ødelægge sin karriere. Han siger også, at han spurgte, om holdets Codex-sessioner var brugt i træning, og med hans ord ikke fik noget svar.
Buckmaster er varsom i udtalelsen: han har ikke set OpenAI’s bevis, og han skriver, at han ikke anklager nogen for noget.
Bubeck har afvist fremstillingen. OfficeChai skrev, at han kaldte påstandene falske og ophidsende, sagde, at OpenAI ikke brugte parrets prompts eller beviser til at instruere sine egne modeller, og at han gik ind i samtalen efter akademiske normer. Han sagde, at OpenAI nåede Euler uafhængigt med andre metoder, og at arbejdet med Navier-Stokes brugte en lignende tilgang, udviklet i løbet af en weekend.
Hvad der er og ikke er afgjort
Alpöge og Buckmasters resultater er offentlige og Lean-verificerede. OpenAI’s Navier-Stokes-påstand er det ikke: mandag havde selskabet ikke lagt resultatet ud på sin egen nyhedsside, og ingen udenforstående har gennemgået beviset.
Selv om det holder, er millenniumspørgsmålet ikke åbenlyst besvaret. Scientific American gengav Buckmasters eget forbehold om, at dele af fagfeltet kan komme til at sige, at problemet ikke rigtig er løst, fordi den drevne version hviler på et led, den klassiske formulering udelukker.
Det, man skal følge, er afgrænset og kontrollerbart: om OpenAI frigiver beviset og dets Lean-certifikat, så andre kan verificere det, og om Clay Mathematics Institute siger noget om drivende led. Indtil det første sker, har den ene side i denne historie offentliggjort sit arbejde, og den anden beskrevet det.
