OpenAI's påstand om Navier–Stokes-beviset, forklaret

Navier–Stokes-ligningerne beskriver, hvordan fluider som vand og luft bevæger sig. De er centrale for fluiddynamik, ingeniørvidenskab og fysik, men matematikere har ikke haft en fuldstændig analytisk forståelse af deres opførsel i tre dimensioner.

Millennium Prize-versionen spørger groft sagt, om glatte begyndelsesbetingelser altid fører til glatte løsninger for al fremtidig tid, eller om ligningerne kan “blow up” — skabe en singularitet, hvor en størrelse som hastighed bliver uendelig. Clay Mathematics Institute udpegede problemet som et af syv Millennium Prize Problems i 2000, hver forbundet med en præmie på $1 million. Før denne annoncering var kun Poincaré-formodningen blevet løst blandt de syv, som opsummeret af Wikipedia.

OpenAI's påstand, som rapporteret af Quanta Magazine, er, at autonome AI-agenter, der kørte på en intern model, fandt en singularitet i de tredimensionelle Navier–Stokes-ligninger. Quanta rapporterer, at arbejdet brugte omkring 10.000 agenter, at agenterne fandt et bevis efter 88 timer, og at en anden AI-model formaliserede resultatet i Lean efter yderligere 17 timer. Agenterne udvekslede næsten 5 millioner beskeder, og Sébastien Bubeck fra OpenAI anslog ifølge Quanta de beregningsmæssige omkostninger til flere millioner dollars.

MIT Technology Review rapporterer, at OpenAI siger, at de ikke planlægger at gøre krav på præmien på $1 million. Ifølge Wikipedia er modeksemplet endnu ikke blevet verificeret af eksterne matematikere eller af Clay Mathematics Institute.

Det sidste punkt er vigtigt. En Lean-formalisering er et stærkt signal, men det er ikke det samme som accept i fagmiljøet. Quanta bemærker, at formelle beviser kan fastslå, at et udsagn følger inde i proof assistenten, mens matematikere stadig skal kontrollere, at det formaliserede udsagn er logisk ækvivalent med den matematiske påstand, folk ønskede at bevise.

Differentialligninger beskriver relationer mellem størrelser i forandring. I fluidmekanik kombinerer Navier–Stokes-ligningerne hastighed, tryk, viskositet, eksterne kræfter og massebevarelse. De er nemme nok at skrive ned i standardnotation, men deres langsigtede opførsel kan være ekstremt svær at forstå.

Den centrale vanskelighed er ikke, om ingeniører kan simulere fluider. Det gør de hele tiden. Spørgsmålet er, om de idealiserede matematiske ligninger med garanti opfører sig pænt under de betingelser, der er specificeret af Millennium Prize-problemet.

En singularitet ville betyde, at ligningerne forudsiger et sammenbrud: En del af fluiden udvikler sig mod en umulig matematisk tilstand. Som Quanta forklarer, indebærer det ikke et øjeblikkeligt praktisk svigt i virkelig ingeniørpraksis, fordi faktiske fluider består af molekyler og atomer snarere end perfekt glatte kontinua. Men matematisk ville det vise, at de idealiserede ligninger har mere overraskende opførsel, end mange forventede.

Problemet hænger også sammen med turbulens, et af de sværeste fænomener i fysik. Wikipedia beskriver turbulens som et af de største uløste problemer i fysik på trods af dets betydning for videnskab og ingeniørarbejde. Et bevis for blowup ville ikke “løse turbulens” i praktisk forstand, men det ville ændre, hvad matematikere ved om ligningerne bag den.

Kontroversen handler om forholdet mellem OpenAI's arbejde og Buckmaster og Alpöges arbejde.

Quanta rapporterer, at OpenAI's annoncering kom omkring 12 timer efter, at Buckmaster annoncerede resultater med Alpöge om nært beslægtede problemer. Deres arbejde brugte en række AI-modeller, inklusive OpenAI-modeller. MIT Technology Review rapporterer, at Buckmaster og Alpöge havde arbejdet på problemet i næsten et år, og at Buckmaster offentliggjorde et bevis, der viste, at en forenklet version af Navier–Stokes-ligningerne kan bryde sammen.

Både OpenAI-arbejdet og Buckmaster–Alpöge-arbejdet ser ud til at bygge på en tilgang forbundet med Diego Córdoba og Luis Martínez-Zoroa. Quanta siger, at begge teams trak kraftigt på arbejde af Córdoba og Martínez-Zoroa, som udviklede en strategi, der afveg fra de metoder, de fleste matematikere brugte. MIT Technology Review citerer Brown Universitys matematikprofessor Javier Gómez-Serrano for at sige, at denne tilgang var en af flere, man mente havde potentiale for problemet.

OpenAI har ifølge MIT Technology Review erkendt, at teamet blev inspireret til at forfølge problemet efter at have hørt et rygte om Buckmaster og Alpöges indsats. Striden handler om, hvorvidt OpenAI's modeller eller medarbejdere havde adgang til, blev trænet på eller på anden måde drog fordel af Buckmaster og Alpöges arbejde.

MIT Technology Review rapporterer, at Buckmaster offentliggjorde et dokument, der beskrev interaktioner med OpenAI-medarbejdere. Ifølge Buckmasters beretning præsenterede OpenAI-medarbejdere to muligheder. Buckmaster og Alpöge kunne offentliggøre deres arbejde, og OpenAI ville offentliggøre sin Navier–Stokes-løsning den følgende dag, eller Buckmaster kunne arbejde med OpenAI på en Navier–Stokes-artikel, der udelukkede Alpöge fra forfatterskab på grund af hans tilknytning til Anthropic. MIT Technology Review rapporterer også, at OpenAI afviste, at deres medarbejdere eller agenter tilgik Buckmaster og Alpöges transskriptioner.

Det er alvorlige anklager, men den offentlige dokumentation er ufuldstændig. Den rigtige tilgang er at adskille den matematiske påstand fra krediteringsstriden. Beviset kan være korrekt, mens processen stadig er etisk omstridt. Eller beviset kan falde ved gennemgang, mens krediteringsspørgsmålene stadig betyder noget.

Lean er en proof assistant: et system til at udtrykke matematiske udsagn og kontrollere, at hvert trin følger af formelle regler. I matematik med høje indsatser kan det fjerne en stor klasse af fejl. Det kan også gøre AI-genererede beviser lettere at auditere, fordi beviset ikke kun er prosa; det er eksekverbar formel logik.

Det er derfor, Lean-komponenten er vigtig. Hvis formaliseringen er solid og matcher det tilsigtede Navier–Stokes-udsagn, bliver resultatet langt sværere at afvise som flydende hallucination. For AI-byggere er det forskellen mellem en model, der skriver plausibel ræsonnering, og et system, der producerer artefakter, et andet program kan kontrollere.

Men Lean løser ikke alle tillidsproblemer. Det fastslår ikke prioritet. Det afslører ikke, hvordan beviset blev fundet. Det forklarer ikke, om private data, transskriptioner eller upublicerede idéer påvirkede søgningen. Og det erstatter ikke det matematiske fagmiljøs rolle i at fortolke bevisets betydning.

Denne skelnen bør føles velkendt for folk, der bygger AI-produkter. Strukturerede outputs, tests, evals og formelle kontroller kan gøre systemer mere pålidelige, men de besvarer ikke i sig selv governance-spørgsmål. Hvis en AI-agent kan kalde værktøjer, inspicere logs, genbruge privat kontekst eller koordinere med andre agenter, har systemet brug for grænser og audit trails lige så meget som rå kapacitet.

Det er en af grundene til, at multi-agent-arbejde er et ingeniørproblem, ikke bare et prompting-trick. Uanset om du designer forskningsagenter eller forretningsworkflows, ligner de praktiske spørgsmål hinanden: Hvilke agenter kan se hvilken kontekst, hvilke værktøjer kan de kalde, hvor sker handoffs, og hvad bliver logget? De designvalg betyder noget i AI-agenter længe før indsatserne når Millennium Prize-niveau.

Den mest slående operationelle detalje er skalaen. Quanta rapporterer omtrent 10.000 agenter, 88 timers søgning, yderligere 17 timer til formalisering og næsten 5 millioner beskeder mellem agenter. MIT Technology Review rapporterer, at OpenAI sagde, at kørslen kostede millioner af dollars.

Den skala er ikke tilgængelig for de fleste akademiske grupper. Den peger på en mulig fremtid, hvor matematiske fremskridt i frontlinjen afhænger af interne modeller, private compute-budgetter og agentinfrastruktur koncentreret hos nogle få AI-virksomheder.

MIT Technology Review fremstiller dette som et vendepunkt for matematik: Hvis store åbne problemer kan angribes af private sværme af agenter, kan normerne for akademisk samarbejde komme under pres. Matematikere lærer ofte af mislykkede forsøg, delresultater og omveje. Hvis de sker inde i private systemer og aldrig bliver offentlige, kan feltet få svar uden den fælles vej, der traditionelt skaber nye værktøjer og underfelter.

Quanta citerer Princeton-matematikeren Charles Fefferman, som skrev Clay Institutes officielle problembeskrivelse, for at sige, at han var begejstret for, at problemet var løst, og for at udpege Córdoba og Martínez-Zoroa som historiens helte. Den kreditering er en nyttig korrektion. Selv hvis det sidste skridt var automatiseret, kom forskningssmagen — valget af en lovende retning — fra menneskeligt matematisk arbejde opbygget over år.

For byggere er lektien ikke “brug flere agenter”. Den er, at agentiske systemer forstærker kvaliteten af det søgerum, de får. Bedre modeller og større budgetter hjælper, men problemindramning, kontekstvalg, værktøjsadgang og verificeringsloops afgør stadig, om systemet udforsker nyttigt terræn eller brænder compute af.

Hvis du router arbejde på tværs af flere modeller, gælder det samme princip i mindre skala. Brug den bedste model til opgaven, men behandl ikke modelvalg som hele systemet. Det omgivende workflow — retrieval, begrænsninger, kontroller, godkendelser og logs — er der, pålideligheden kommer fra. Med andre ord kommer kapacitet fra hele workflowet, ikke fra et valg på en leaderboard.

Det første at holde øje med er matematisk validering. Eksterne matematikere og Clay Mathematics Institute får brug for tid til at vurdere, om beviset er korrekt, om Lean-formaliseringen matcher den tilsigtede påstand, og hvordan resultatet passer ind i tidligere arbejde.

Det andet er kreditering. De offentlige beretninger fra OpenAI, Buckmaster, Alpöge og udefrakommende matematikere udgør endnu ikke en afklaret dokumentation. De centrale spørgsmål er faktuelle: Hvad tilgik OpenAI's agenter eller medarbejdere, hvad trænede de på, hvad vidste de, og hvornår vidste de det?

Det tredje er, om dette bliver en skabelon. Hvis frontier-AI-labs kan rette massive agentsværme mod berømte uløste problemer, vil der komme flere annonceringer. Nogle vil være rene. Nogle vil blive bestridt. Nogle vil falde ved gennemgang. De berørte felter får brug for normer for kredit, offentliggørelse, privat compute og AI-assisterede prioritetspåstande.

For folk, der bygger med AI uden for ren matematik, er budskabet klart nok: Kapacitet bevæger sig mod systemer, ikke enkeltprompts. Agenter, værktøjer, model routing og verificering er ved at blive arbejdsenheden. Teams, der håndterer proveniens og gennemgang godt, vil stå bedre end teams, der kun jagter større outputs.

Vi følger fortsat historien om verificering og kreditering, efterhånden som den udvikler sig. Hvis du vil have AI-nyheder med den tekniske kontekst bevaret, kan du abonnere på LIA-nyhedsbrevet.

• OpenAI hævder, at autonome AI-agenter fandt en singularitet i de tredimensionelle Navier–Stokes-ligninger og producerede en Lean-formalisering.
• Resultatet er endnu ikke blevet verificeret af eksterne matematikere eller accepteret af Clay Mathematics Institute.
• Et Lean-bevis kan reducere mange fejl i beviskontrol, men reviewere skal stadig bekræfte, at det formelle udsagn matcher den tilsigtede matematiske påstand.
• Annonceringen er viklet ind i en krediteringsstrid, der involverer arbejde af Tristan Buckmaster, Levent Alpöge, Diego Córdoba og Luis Martínez-Zoroa.
• Den rapporterede skala for kørslen fremhæver en ressourcekløft mellem frontier-AI-labs og de fleste akademiske grupper.
• For AI-byggere viser episoden, at agenter har brug for proveniens, audit trails, verificeringsloops og klare grænser, ikke bare mere compute.

Denne sektion besvarer de praktiske spørgsmål bag OpenAI's Navier–Stokes-påstand: Svarene nedenfor dækker annonceringen, Leans rolle og de dele, der stadig kræver uafhængig gennemgang. Den adskiller også de matematiske indsatser fra krediteringsstriden omkring arbejdet.

OpenAI siger, at de har en AI-genereret løsning, men påstanden kræver stadig ekstern matematisk gennemgang og vurdering fra Clay Mathematics Institute.

Ifølge de citerede rapporter hævder OpenAI, at deres agenter fandt en singularitet i de tredimensionelle Navier–Stokes-ligninger, og at en anden model formaliserede resultatet i Lean.

Lean kan kontrollere, at hvert formelt trin følger af regler, hvilket gør beviset sværere at afvise som plausibel prosa. Matematikere skal stadig verificere, at det formaliserede udsagn matcher den tilsigtede Navier–Stokes-påstand.

Striden handler om, hvorvidt OpenAI's arbejde drog fordel af AI-assisteret forskning udført af Tristan Buckmaster og Levent Alpöge uden korrekt kreditering. OpenAI har ifølge MIT Technology Review afvist, at deres medarbejdere eller agenter tilgik deres transskriptioner.

Nej. Et blowup-bevis ville ændre den matematiske forståelse af ligningerne bag fluiders bevægelse, men det ville ikke direkte løse turbulens som et praktisk ingeniørproblem.