Om Navier–Stokes-Millenniumprisproblemet

Vi offentliggør en løsning på Navier–Stokes-problemet om eksistens og glathed, et af Millenniumprisproblemerne. Dette bevis, som er frembragt af et internt OpenAI-system, viser, at dynamikken i Navier–Stokes-ligningerne for væskebevægelse kan udvikle en singularitet på endelig tid. Vi offentliggør både en redegørelse for beviset og en formalisering i Lean.

Millenniumprisproblemerne⁠(åbner i et nyt vindue) omfatter nogle af de dybeste spørgsmål inden for banebrydende matematik. Spørgsmålet om, hvorvidt en glat tredimensionel væskebevægelse kan bryde sammen, har været uløst i omkring 90 år.

Et vigtigt mål med vores arbejde er at sætte forskere i stand til at fremme forskning og teknologi til gavn for hele menneskeheden. For at løse Navier–Stokes-problemet brugte vi en intern model, der er markant mere kompetent end GPT‑6 Astra. Vi mener, at det er vigtigt at informere verden om tempoet i AI-udviklingen, og hvad man kan forvente af kommende modeller.

Navier–Stokes-ligningerne anvender Newtons anden bevægelseslov (»F=ma«) til at beskrive, hvordan væsker bevæger sig. Det er vigtigt, at de behandler en væske som et kontinuert medium frem for at følge de enkelte molekyler. Disse ligninger bruges til flydesign, vejrudsigter og studier af blodgennemstrømning.

Et grundlæggende åbent spørgsmål for disse dynamiske ligninger har været, om kontinuumsapproksimationen af væsken kan bryde sammen. Kan Navier–Stokes-ligningerne for en tredimensionel inkompressibel væske med konstant massefylde nærmere bestemt udvikle en »singularitet«, selv når bevægelsen begynder jævnt? Her betyder en singularitet, at dynamikken medfører, at hastighederne i væsken vokser ubegrænset inden for et endeligt tidsrum. En singularitet ville skulle opstå trods viskositeten, som har en tendens til at udjævne bevægelsen. Da en virkelig væske ikke kan bevæge sig uendeligt hurtigt, ville det betyde, at ligningernes modellering af væsken bryder sammen. For fortsat at kunne modellere systemet ville man derefter være nødt til at følge hver enkelt partikels adfærd.

Ligningerne stammer fra Claude-Louis Naviers og George Gabriel Stokes' arbejde i det 19. århundrede. I 1934 beviste Jean Leray, at løsninger findes i generaliseret forstand, men spørgsmålet om, hvorvidt de altid forbliver glatte, blev et centralt uløst problem. I 2000 udpegede Clay Mathematics Institute Navier–Stokes-problemet om eksistens og glathed som et af syv Millenniumprisproblemer.

Vores system frembragte et analytisk bevis og en Lean-formalisering af, at en væske, som oprindeligt er glat og i hvile, kan udvikle en singularitet på endelig tid. Væsken påvirkes af en glat kraft, og dens energi forbliver endelig gennem hele dynamikken, fra hvile til singularitetens dannelse. Dette løser Navier–Stokes-Millenniumprisproblemet ved at fastslå udsagn »C« (og også »D«) i den officielle formulering af Millenniumprisproblemet⁠(åbner i et nyt vindue).

Løsningen er en hvirvel, en roterende væskestrøm, der snor sig indad og bliver stadig mere langstrakt som spaghetti. Dette centrale område skrumper, mens hastigheden stiger på en måde, så energien fortsat er endelig, som fysikkens love kræver. Den tekniske udfordring er, at ligningerne skal udvikle sammenbruddet gennem væskens egen bevægelse, frem for at vi eksempelvis manuelt tilfører en uendelig kraft. Mere matematisk skal leddene i Navier–Stokes-ligningerne, der beskriver bevægelsen – acceleration, trykgradienter, impulsoverførsel og viskositet – både blive store og samtidig udligne hinanden på en præcis måde. Denne nøje afstemning efterlader en glat ekstern kraft, selvom væskens hastighed vokser ubegrænset.

Siden den 28. august har vi trænet en ny intern model, der har udvist hidtil usete resultater i vores benchmarks, herunder inden for matematik. Træningen af denne model fortsætter, og dens ydeevne bliver stadig bedre.

Tirsdag den 1. september hørte vi rygter om, at to Millenniumprisproblemer var blevet løst. Inspireret af disse rygter og det markante spring i vores interne models ydeevne iværksatte vi en indsats for at evaluere den på alle åbne Millenniumprisproblemer og enkelte andre problemer med stor betydning.

Vi brugte et system af koordinerende agenter drevet af vores interne model. Agenterne havde adgang til værktøjer, herunder mulighed for at læse en cachelagret version af internettet og for at køre kode. Agenterne blev opdelt i grupper, der kunne kommunikere internt. Gruppernes størrelse varierede, og gruppen, der løste Navier–Stokes-problemet, omfattede omkring 10.000 samtidige agenter. Vi opretholdt hele tiden de samme strenge sikkerhedsforanstaltninger, som vi anvender ved alle evalueringer af vores banebrydende modeller, herunder overvågning og isolation.

For hvert problem gav vi forskellige grupper af agenter forskellige varianter af problemformuleringen, så alle problemets varianter blev dækket. For Navier–Stokes-problemet gav vi separate grupper af agenter version »A« og »B« (bestemte former af Navier–Stokes-problemet, som ville føre til et bevis) samt version »C« og »D« (som ville føre til et modbevis).

Ud over de fulde Millenniumprisproblemer bad vi vores multiagentsystem om at forsøge sig med en række »lettere« problemer. Et af disse problemer var et tilsvarende spørgsmål om singularitetsdannelse i grænsetilfældet af Navier–Stokes-problemet, hvor viskositetsleddet er fjernet. Dette er kendt som regularitetsproblemet for Euler-ligningerne, og vores agenter overraskede os ved at løse spørgsmålet. Den specifikke variant af spørgsmålet, de løste, var versionen uden ekstern kraft, hvor væsken ikke påvirkes af nogen ekstern kraft. Næsten 100 agenter arbejdede sammen i cirka 50 timer for at frembringe vores modbevis vedrørende Euler-regularitet¹.

Da vi så Euler-løsningen, vurderede vi, at Navier–Stokes var det mest lovende problem at arbejde videre med. Derfor besluttede vi at afsætte vores ressourcer til Navier–Stokes. Vi flyttede derfor agenter fra de øvrige Millenniumprisproblemer og gav dem Euler-løsningen som input. Da en videreudviklet version af vores interne model blev tilgængelig under arbejdet, opdaterede vi vores agenter til denne model.

Vi opfordrede de forskellige grupper af agenter til at udforske en bred vifte af tilgange. Efter noget tid skabte vi videndeling mellem agentgrupperne ved at bruge Codex til at samle de mest nyttige indsigter fra hver gruppe. Disse opfølgende prompts byggede på agenternes egne foreløbige resultater. Gruppen, der fandt løsningen på Navier–Stokes, blev vejledt på denne måde.

Agenterne nåede frem til deres løsning lørdag den 5. september, cirka 88 timer efter at de første agenter blev sat i gang. Lean-formalisering og -verifikation via GPT‑6 Astra tog yderligere 17 timer.

På tværs af alle de afprøvede problemer sendte agenterne 4,9 millioner beskeder og brugte omkring 300 milliarder outputtokens. Under løsningen af Navier–Stokes-problemet sendte agenterne 2,7 millioner beskeder og brugte cirka 130 milliarder outputtokens.

Vores indsats begyndte den 1. september, efter at vi havde hørt et rygte, som vi senere fandt ud af vedrørte Levent Alpöge, der er ansat hos Anthropic, og Tristan Buckmaster, der er matematikprofessor ved NYU.² Da hele vores projekt og Lean-verifikationen var afsluttet den 6. september, kontaktede vi dem, fordi rygtet fik os til at tro, at de også havde en løsning på Navier–Stokes. Vi tilbød at offentliggøre vores resultat samtidig og anerkende deres prioritet i en fælles meddelelse. På det tidspunkt fandt vi ud af, at de ved hjælp af en intern Anthropic-model havde fundet en løsning på Euler-problemet med ekstern kraft. Under disse drøftelser tilbød vi dem indsigt i alle de prompts, vi havde brugt, og senere også adgang til at se beviset. Vi anerkender, at deres arbejde med Euler-problemet med ekstern kraft kom først, og lykønsker dem med deres bemærkelsesværdige matematiske bedrift.

Vi – forskerne og agenterne – fik ikke på nogen måde adgang til deres arbejde, før de offentliggjorde det. Der blev navnlig ikke tilgået specifikke brugerdata for at løse dette problem.

Efter en undersøgelse har vi bekræftet, at Buckmasters Codex-prompts i de to måneder op til denne meddelelse og artikel den 8. september 2026 ikke kan have påvirket systemet på nogen måde, heller ikke gennem træning. Den interne OpenAI-model, der blev brugt til dette resultat, blev udviklet gennem forstærkende læring i stor skala oven på en tidligere fortrænet model. Vores beviser adskiller sig også væsentligt. I Euler-tilfældet beviste Alpöge og Buckmaster et resultat med ekstern kraft, mens OpenAI-systemet beviste et resultat uden ekstern kraft.

Formålet med at offentliggøre dette resultat er at orientere om vores AI-modellers betydelige fremskridt. Vi har ikke til hensigt at gøre krav på Millenniumprisen for dette resultat.

Denne milepæl repræsenterer en betydelig indsats fra matematikere og AI-forskere. Dette er dog ikke et højdepunkt, men snarere et øjebliksbillede af fremskridtene inden for AI-udvikling.

Vi mener, at vi nu er gået ind i den næste fase af AI-udviklingen⁠, og dagens resultater underbygger dette yderligere. Vi fokuserer på at forstå denne model og bruge vores erfaringer til at styre og afpasse tempoet i vores videre udvikling af dens evner. Et af vores vigtigste mål⁠ er at bygge AI-systemer, der kan styres, står til ansvar og er forbundet med mennesker. Det kan kræve mere bevidste valg om udviklingens tempo, mens vi fortsætter vores mission om at sikre, at AGI gavner hele menneskeheden.