Om millenniumprisproblemet Navier–Stokes

Vi deler en løsning på Navier–Stokes-problemet om eksistens og glatthet, ett av millenniumprisproblemene. Dette beviset, som er utarbeidet av et internt OpenAI-system, viser at dynamikken i Navier–Stokes-ligningene for væskebevegelse kan utvikle en singularitet på endelig tid. Vi deler både en redegjørelse for beviset og en formalisering i Lean.

Millenniumprisproblemene⁠(åpnes i et nytt vindu) representerer noen av de dypeste spørsmålene innen banebrytende matematikk. Spørsmålet om glatt tredimensjonal væskebevegelse kan bryte sammen, har vært uløst i omtrent 90 år.

Et viktig mål med arbeidet vårt er å sette forskere i stand til å fremme forskning og teknologi som gagner hele menneskeheten. For å løse Navier–Stokes-problemet brukte vi en intern modell som er betydelig mer kapabel enn GPT‑6 Astra. Vi mener det er viktig å informere verden om tempoet i KI-utviklingen og hva man kan forvente av kommende modeller.

Navier–Stokes-ligningene bruker Newtons andre lov («F=ma») til å beskrive hvordan væsker beveger seg. Det er viktig at de behandler en væske som et kontinuerlig medium i stedet for å følge enkeltmolekyler. Disse ligningene brukes til flydesign, værvarsling og studier av blodstrøm.

Et grunnleggende, uløst spørsmål ved disse dynamiske ligningene har vært om kontinuumstilnærmingen for væsken kan bryte sammen. Kan Navier–Stokes-ligningene for en tredimensjonal, inkompressibel væske med konstant tetthet utvikle en «singularitet», selv når bevegelsen starter glatt? Her betyr en singularitet at dynamikken fører til at hastighetene i væsken vokser uten grenser i løpet av endelig tid. En singularitet måtte oppstå til tross for viskositeten, som har en tendens til å jevne ut bevegelsen. Fordi en virkelig væske ikke kan bevege seg uendelig raskt, ville dette innebære at ligningenes modell av væsken bryter sammen. For å fortsette å modellere systemet måtte man da følge oppførselen til hver partikkel for seg.

Ligningene stammer fra Claude-Louis Navier og George Gabriel Stokes’ arbeid på 1800-tallet. I 1934 beviste Jean Leray at løsninger finnes i en generalisert forstand, men spørsmålet om de alltid forblir glatte, ble stående som et sentralt uløst problem. I 2000 utpekte Clay Mathematics Institute Navier–Stokes-problemet om eksistens og glatthet som ett av de sju millenniumprisproblemene.

Systemet vårt utarbeidet et analytisk bevis og en Lean-formalisering som viser at en væske som i utgangspunktet er glatt og i ro, kan utvikle en singularitet på endelig tid. Væsken påvirkes av en glatt kraft, og energien forblir endelig gjennom hele dynamikken, fra hvile til singulariteten dannes. Dette løser millenniumprisproblemet om Navier–Stokes ved å fastslå utsagn «C» (og også «D») i den offisielle formuleringen av millenniumprisproblemet⁠(åpnes i et nytt vindu).

Løsningen er en virvel, en roterende væskestrøm, som går i spiral innover og strekkes stadig mer ut, som spagetti. Dette sentrale området krymper samtidig som hastigheten øker på en slik måte at energien fortsatt er endelig, slik fysikkens lover krever. Den tekniske utfordringen er at sammenbruddet må oppstå i ligningene gjennom selve væskebevegelsen, og ikke ved at vi for eksempel legger inn en uendelig kraft manuelt. Mer matematisk uttrykt må leddene i Navier–Stokes-ligningene som beskriver bevegelsen – akselerasjon, trykkgradienter, impulsoverføring og viskositet – både bli store og samtidig utligne hverandre på en presis måte. Denne nøyaktige balansen gjør at den ytre kraften forblir glatt, selv når væskehastigheten vokser uten grenser.

Siden 28. august har vi trent en ny intern modell som har vist enestående resultater i referansetestene våre, også innen matematikk. Treningen av modellen pågår fortsatt, og ytelsen fortsetter å bli bedre.

Tirsdag 1. september hørte vi rykter om at to millenniumprisproblemer var blitt løst. Inspirert av disse ryktene og det markante ytelseshoppet til den interne modellen startet vi et arbeid med å evaluere den på alle uløste millenniumprisproblemer og noen andre problemer med stor betydning.

Vi brukte et system av koordinerende agenter drevet av den interne modellen vår. Agentene hadde tilgang til verktøy som lot dem lese en bufret versjon av internett og kjøre kode. Agentene ble delt inn i grupper og kunne kommunisere innad i gruppen. Gruppene varierte i størrelse, og gruppen som løste Navier–Stokes-problemet, besto av rundt 10 000 agenter som arbeidet samtidig. Vi opprettholdt hele tiden de samme strenge sikkerhetstiltakene som ved alle evalueringer av våre banebrytende modeller, inkludert overvåking og isolasjon.

For hvert problem ga vi ulike agentgrupper forskjellige varianter av problemformuleringen, slik at alle variantene av problemet ble dekket. For Navier–Stokes-problemet ga vi separate agentgrupper versjon «A» og «B» (bestemte former av Navier–Stokes-problemet som ville gi et bevis) og versjon «C» og «D» (som ville gi et motbevis).

I tillegg til de fullstendige millenniumprisproblemene ba vi multiagentsystemet vårt prøve seg på et sett med «enklere» problemer. Ett av disse var et lignende spørsmål om singularitetsdannelse for grensen av Navier–Stokes-problemet når viskositetsleddet fjernes. Dette er kjent som regularitetsproblemet for Euler-ligningene, og agentene våre overrasket oss ved å løse det. Den konkrete varianten de løste, var versjonen uten ytre kraft, der væsken ikke påvirkes av noen ekstern kraft. Nesten 100 agenter samarbeidet i rundt 50 timer for å utarbeide motbeviset vårt for Euler-regularitet¹.

Da vi så Euler-løsningen, mente vi at Navier–Stokes var det mest lovende problemet å arbeide videre med. Derfor bestemte vi oss for å vie ressursene våre til Navier–Stokes. Vi flyttet derfor agenter fra de andre millenniumprisproblemene og ga dem Euler-løsningen som utgangspunkt. Da en videre trent versjon av den interne modellen ble tilgjengelig underveis, oppdaterte vi agentene våre til denne modellen.

Vi oppfordret de ulike agentgruppene til å utforske forskjellige tilnærminger. Etter en stund lot vi agentgruppene utveksle ideer ved å bruke Codex til å sammenfatte de mest nyttige innsiktene fra hver gruppe. Disse oppfølgingsinstruksjonene bygget på agentenes egne foreløpige resultater. Gruppen som fant løsningen på Navier–Stokes, ble veiledet på denne måten.

Agentene kom frem til løsningen lørdag 5. september, rundt 88 timer etter at de første agentene ble startet. Formalisering og verifisering i Lean tok ytterligere 17 timer ved hjelp av GPT‑6 Astra.

På tvers av alle problemene de forsøkte å løse, sendte agentene 4,9 millioner meldinger og brukte rundt 300 milliarder utdatatokener. I arbeidet med å løse Navier–Stokes-problemet sendte agentene 2,7 millioner meldinger og brukte omtrent 130 milliarder utdatatokener.

Arbeidet vårt begynte 1. september etter at vi hørte et rykte som vi senere forsto var knyttet til Levent Alpöge, en Anthropic-ansatt, og Tristan Buckmaster, professor i matematikk ved NYU.² Da hele prosjektet og Lean-verifiseringen var fullført 6. september, trodde vi på bakgrunn av ryktet at de også hadde en løsning på Navier–Stokes. Vi kontaktet dem derfor og tilbød å publisere resultatene samtidig og anerkjenne at de var først, i en felles kunngjøring. Da fikk vi vite at de ved hjelp av en intern Anthropic-modell hadde løst Euler-problemet med ytre kraft. I disse samtalene tilbød vi dem innsyn i alle instruksjonene vi brukte, og senere også i beviset. Vi anerkjenner at de var først med arbeidet om Euler med ytre kraft, og gratulerer dem med en bemerkelsesverdig matematisk prestasjon.

Vi – forskerne og agentene – fikk ikke se noe av arbeidet deres på noen måte før de offentliggjorde det. Det ble særlig ikke åpnet noen spesifikke brukerdata for å løse dette problemet.

Etter en undersøkelse har vi bekreftet at Buckmasters Codex-instruksjoner i de to månedene før denne kunngjøringen og artikkelen 8. september 2026 ikke kan ha påvirket systemet på noen måte, heller ikke gjennom trening. Den interne OpenAI-modellen som ble brukt til dette resultatet, ble utviklet gjennom forsterkende læring i stor skala med utgangspunkt i en tidligere forhåndstrent modell. Bevisene våre er også vesentlig forskjellige. For Euler beviste Alpöge og Buckmaster et resultat med ytre kraft, mens OpenAIs system beviste et resultat uten ytre kraft.

Målet med å offentliggjøre dette resultatet er å rapportere om den betydelige fremgangen til KI-modellene våre. Vi har ikke til hensikt å kreve millenniumprisen for dette resultatet.

Denne milepælen representerer et omfattende arbeid utført av matematikere og KI-forskere. Dette er imidlertid ikke et sluttpunkt, men et øyeblikksbilde av fremgangen i KI-utviklingen.

Vi mener at vi nå er inne i den neste fasen av KI-utviklingen⁠, og dagens resultater gir ytterligere støtte for dette. Vi arbeider med å forstå denne modellen og bruker det vi lærer, til å styre og avpasse hvordan vi videreutvikler kapasiteten. Et av våre viktigste mål⁠ er å bygge KI-systemer som kan styres, holdes ansvarlige og er knyttet til mennesker. Det kan kreve mer bevisste valg om utviklingstakten mens vi fortsetter arbeidet med å sikre at AGI gagner hele menneskeheten.