Vad som faktiskt bevisades

Levent Alpöge och Tristan Buckmaster har publicerat tre preprints som fastställer blowup i ändlig tid med en jämn tvingande term för den inkompressibla porösa medium-ekvationen, det tvådimensionella Boussinesq-systemet och de tredimensionella inkompressibla Eulerekvationerna.

Terence Tao skrev om resultaten på måndagen och noterade att argumenten är “kraftigt AI-assisterade” och att arbetet också har formaliserats i Lean. Han tillskriver det underliggande programmet Diego Córdoba och Luis Martínez-Zoroa, som först klarade fallet med poröst medium.

Blowup innebär att ekvationerna ger en lösning vars hastighet blir oändlig på ändlig tid — ett matematiskt sammanbrott, inte ett fysiskt. Att fastställa det för Euler med tvingande term är ett steg mot samma fråga för Navier-Stokes, som bär ett Millennieproblem-pris från Clay-institutet.

AI-delen

Buckmaster är vid New York University. Alpöge är forskare på Anthropic. Enligt Unite.AI uppgav paret att de använt Anthropics Claude och OpenAI:s Codex för bokföring av induktiva ordningar och konstanter, och för att stegvis förbättra texten.

En svart tavla täckt av handskrivna matematiska ekvationer
Argumenten formaliserades i bevisassistenten Lean. Illustrationsbild. https://kaboompics.com/ · pexels · Pexels License

De var uppriktiga om kvaliteten på prosan modellerna producerade. Buckmaster beskrev den ursprungliga AI-genererade texten som “den mest fasansfulla jag någonsin läst”, och författarna kallade sitt första utkast den sämsta text de sett. Det är Lean-formaliseringen som bär vissheten: en bevisassistent accepterar ett argument eller gör det inte.

Tvisten

I ett uttalande publicerat tillsammans med preprintsen säger Buckmaster att OpenAI berättade för honom att en intern modell producerat ett ungefär 100 sidor långt bevis för blowup i ändlig tid för de tvingade Navier-Stokes-ekvationerna. Han beskriver två samtal den 6 september med OpenAI-forskare, bland dem Sébastien Bubeck.

Buckmaster uppger att OpenAI föreslog antingen att de två grupperna skulle publicera på varandra följande dagar, med OpenAI:s Navier-Stokes-resultat efter hans Euler-artikel, eller att han ensam skrev upp Navier-Stokes-resultatet och krediterade en icke namngiven intern OpenAI-modell, med Alpöge borttagen från författarskapet — något Buckmaster kopplar till Alpöges anställning på Anthropic. Han berättar att han efter sitt nej fick frågan varför han skulle förstöra sin karriär. Han säger också att han frågade om teamets Codex-sessioner använts i träning och, med hans ord, inte fick något svar.

Buckmaster är försiktig i uttalandet: han har inte sett OpenAI:s bevis, och han skriver att han inte anklagar någon för något.

En tom universitetsföreläsningssal med rader av blå stolar
Tvisten handlar om författarskapet mellan en universitetsmatematiker och ett labb. Illustrationsbild. DOAN THANH BINH · pexels · Pexels License

Bubeck har avvisat beskrivningen. OfficeChai rapporterade att han kallade påståendena falska och uppviglande, sade att OpenAI inte använt parets prompter eller bevis för att styra sina egna modeller, och att han gått in i samtalet i enlighet med akademiska normer. Han uppgav att OpenAI nådde Euler självständigt med andra metoder, och att arbetet med Navier-Stokes använde ett liknande angreppssätt, framtaget under en helg.

Vad som är och inte är avgjort

Alpöges och Buckmasters resultat är offentliga och Lean-verifierade. OpenAI:s Navier-Stokes-påstående är det inte: på måndagen hade bolaget inte lagt ut resultatet på sin egen nyhetssida, och ingen utomstående har granskat beviset.

Även om det håller är Millennieproblemet inte uppenbart besvarat. Scientific American återgav Buckmasters egen reservation att delar av fältet kan komma att säga att problemet inte riktigt är löst, eftersom den tvingade versionen vilar på en term som den klassiska formuleringen utesluter.

Det som ska bevakas är avgränsat och kontrollerbart: om OpenAI släpper beviset och dess Lean-certifikat så att andra kan verifiera det, och om Clay Mathematics Institute säger något om tvingande termer. Tills det första sker har den ena sidan i den här historien publicerat sitt arbete och den andra beskrivit det.