Hva som faktisk ble bevist
Levent Alpöge og Tristan Buckmaster har lagt ut tre preprinter som fastslår blowup på endelig tid med et glatt drivende ledd for den inkompressible porøse medium-ligningen, det todimensjonale Boussinesq-systemet og de tredimensjonale inkompressible Euler-ligningene.
Terence Tao skrev om resultatene mandag og bemerket at argumentene er «tungt KI-assisterte», og at arbeidet også er formalisert i Lean. Han tilskriver det underliggende programmet Diego Córdoba og Luis Martínez-Zoroa, som først tok tilfellet med porøst medium.
Blowup betyr at ligningene gir en løsning der hastigheten blir uendelig på endelig tid — et matematisk sammenbrudd, ikke et fysisk. Å fastslå det for Euler med drivende ledd er et skritt mot det samme spørsmålet for Navier-Stokes, som bærer en millenniumspris fra Clay-instituttet.
KI-delen
Buckmaster er ved New York University. Alpöge er forsker i Anthropic. Ifølge Unite.AI opplyste de to at de brukte Anthropics Claude og OpenAIs Codex til bokføring av induktive ordener og konstanter, og til trinnvis forbedring av teksten.
De var åpne om kvaliteten på prosaen modellene produserte. Buckmaster beskrev den første KI-genererte teksten som «den mest grufulle jeg noensinne har lest», og forfatterne kalte førsteutkastet det dårligste de hadde sett. Det er Lean-formaliseringen som bærer vissheten: en bevisassistent godtar et argument eller gjør det ikke.
Striden
I en uttalelse publisert sammen med preprintene sier Buckmaster at OpenAI fortalte ham at en intern modell hadde produsert et rundt 100 sider langt bevis for blowup på endelig tid for de drevne Navier-Stokes-ligningene. Han beskriver to samtaler 6. september med OpenAI-forskere, blant dem Sébastien Bubeck.
Buckmaster sier OpenAI foreslo enten at de to gruppene skulle publisere på påfølgende dager, med OpenAIs Navier-Stokes-resultat etter hans Euler-artikkel, eller at han alene skrev opp Navier-Stokes-resultatet og krediterte en unavngitt intern OpenAI-modell, med Alpöge fjernet fra forfatterskapet — et punkt Buckmaster knytter til Alpöges ansettelse i Anthropic. Han forteller at han etter å ha avslått fikk spørsmål om hvorfor han skulle ødelegge karrieren sin. Han sier også at han spurte om teamets Codex-økter var brukt i trening, og med hans ord ikke fikk noe svar.
Buckmaster er varsom i uttalelsen: han har ikke sett OpenAIs bevis, og han skriver at han ikke anklager noen for noe.
Bubeck har avvist framstillingen. OfficeChai meldte at han kalte påstandene falske og oppviglerske, sa at OpenAI ikke brukte parets ledetekster eller bevis til å instruere sine egne modeller, og at han gikk inn i samtalen i tråd med akademiske normer. Han sa at OpenAI nådde Euler uavhengig med andre metoder, og at arbeidet med Navier-Stokes brukte en liknende tilnærming, utviklet i løpet av en helg.
Hva som er og ikke er avgjort
Alpöge og Buckmasters resultater er offentlige og Lean-verifiserte. OpenAIs Navier-Stokes-påstand er det ikke: mandag hadde selskapet ikke lagt ut resultatet på sin egen nyhetsside, og ingen utenforstående har gransket beviset.
Selv om det holder, er millenniumsspørsmålet ikke åpenbart besvart. Scientific American gjenga Buckmasters eget forbehold om at deler av fagfeltet kan komme til å si at problemet ikke egentlig er løst, fordi den drevne versjonen hviler på et ledd den klassiske formuleringen utelukker.
Det som skal følges, er avgrenset og kontrollerbart: om OpenAI slipper beviset og Lean-sertifikatet så andre kan verifisere det, og om Clay Mathematics Institute sier noe om drivende ledd. Til det første skjer, har den ene siden i denne historien publisert arbeidet sitt, og den andre beskrevet det.
