OpenAI hævder gennembrud i Navier–Stokes – men matematikere kræver uafhængig kontrol

OpenAI's påståede resultat om Navier–Stokes-ligningerne kan blive et historisk gennembrud – hvis det består matematisk granskning. Virksomheden oplyser, at et ikke-offentliggjort internt system koordinerede omkring 10.000 AI-agenter i 88 timer og frembragte både et analytisk bevis og en Lean-formalisering. Ifølge OpenAI viser materialet, at en fluidbevægelse, der begynder glat, kan udvikle en singularitet på endelig tid. Men et offentligt tilgængeligt bevismateriale og en formel verificering er ikke det samme som uafhængig faglig accept. 14

Hvad OpenAI siger, at systemet har vist

Navier–Stokes-problemet om eksistens og glathed handler i én formulering om, hvorvidt glatte tredimensionelle strømninger altid forbliver glatte, eller om de kan bryde sammen på endelig tid. OpenAI siger, at dets resultat etablerer den sidste mulighed: Dynamikken kan udvikle en singularitet på endelig tid under de angivne betingelser. 4

Virksomheden har offentliggjort en skriftlig redegørelse og en formalisering i Lean, et værktøj til formelle beviser. Omtalen beskrev manuskriptet som 166 sider langt og systemet som en ikke-offentliggjort model, der arbejdede med cirka 10.000 samtidige agenter over 88 timer. 31

Det er en væsentlig skelnen. Lean kan kontrollere, om et indkodet bevis følger af de præcise definitioner og antagelser, der er lagt ind i systemet. Matematikere skal fortsat vurdere, om den formelle sætning svarer til det problem, man faktisk ønsker at løse, om både den analytiske argumentation og formaliseringen er komplette, og om forudsætningerne er de rigtige. Ved den første omtale havde Clay Mathematics Institute – organisationen bag Millennium Prize-problemerne – ikke uafhængigt accepteret påstanden. 1

Hvorfor det blev en strid om prioritet og kredit

Den matematiske påstand kom samtidig med en konflikt om forskningsforløb og anerkendelse. Tristan Buckmaster fra New York University og Levent Alpöge, der arbejder hos Anthropic, havde arbejdet med beslægtede problemer i fluiddynamik. Buckmaster anklagede OpenAI for at have fået kendskab til deres tilgang og derefter fremskyndet sit eget forsøg; han rejste også spørgsmål om kreditering.

OpenAI afviste, at hverken virksomhedens forskere eller AI-agenter havde set de to matematikeres arbejde, før det blev offentliggjort. Omtalen peger desuden på, at resultaterne var beslægtede, men ikke dokumenteret identiske. Den centrale beskyldning er derfor fortsat uafklaret: Det er en alvorlig offentlig anklage, ikke en fastslået konklusion.

Kontroversen handler dermed ikke kun om, hvorvidt en AI fandt korrekte ligninger. Den handler også om processen: Hvordan en virksomhed får kendskab til en forskningsretning, om tidslinjen kan efterprøves, hvordan beslægtede bidrag skal anerkendes, og om lukkede systemer reelt kan undersøges af resten af forskningsverdenen.

Lean gør ikke den faglige debat overflødig

Formel verifikation hæver beviskravet markant. Lean kontrollerer bevistrin i et formelt sprog og kan derfor fange huller, som kan overleve i traditionel gennemlæsning. OpenAI's offentliggørelse af både en menneskeligt læsbar fremstilling og en formalisering giver fagfolk konkret materiale at undersøge. 4

Men formel verifikation løser kun en del af den videnskabelige vurdering. Fagmiljøet skal stadig afklare:

• Rækkevidde: Hvilken præcis version af Navier–Stokes-problemet beviset afgør.
• Overensstemmelse: Om den uformelle formulering, antagelserne og den formelle sætning faktisk matcher.
• Nyhed og kreditering: Hvilke idéer der kom fra hvem – og hvornår.
• Forståelse: Om beviset giver genanvendelige matematiske indsigter frem for blot en kontrolleret afledning.
• Efterprøvbarhed: Om eksterne forskere kan gennemgå, forklare og bygge videre på arbejdet.

Matematikeren Javier Gómez-Serrano har kaldt situationen en »eksistentiel krise« for matematikken – et udtryk for bekymringen for, at AI-genererede resultater kan løbe hurtigere end de normale mekanismer for forståelse, kontrol, undervisning og kredit.

Kritik af et AI-kapløb i matematikken

Reaktionen rakte hurtigt ud over dette ene bevis. 25 modtagere af Fields-medaljen, herunder Terence Tao, underskrev en erklæring, der advarede om, at konkurrencen mellem AI-virksomheder om at kunne hævde løsninger på svære matematiske problemer kan skade både videnskaben og uddannelsen af nye forskere. 17

Et særskilt åbent brev fra nuværende og tidligere Caltech-matematikere protesterede mod OpenAI's rolle i et planlagt AI-matematikarrangement. Brevet havde 771 underskrifter ved offentliggørelsen, ifølge omtalen, og OpenAI trak senere sit sponsorat af Caltech Mathathon.

Indvendingerne er ikke nødvendigvis et krav om at holde AI ude af matematikken. Bekymringen er, at proprietære systemer og en jagt på overskrifter kan belønne spektakulære påstande på bekostning af åben udveksling, omhyggelig kreditering og matematisk forklaring. De samme værktøjer kan være nyttige i en anden ramme: til at kontrollere beviser, udforske formodninger, forbedre formidling og bidrage til fælles formelle biblioteker.

Er Hodge-formodningen det næste mål?

OpenAI har ifølge omtalen sagt til The New York Times, at selskabet har gjort »betydelige fremskridt« på endnu et Millennium Prize-problem, uden at navngive det eller offentliggøre et bevis. Det er grænsen for den bekræftede offentlige oplysning i de tilgængelige kilder.

Hodge-formodningen er ofte blevet nævnt som et muligt mål, og Birch og Swinnerton-Dyer-formodningen cirkulerer også i spekulationerne. En omtale med henvisning til en OpenAI-kilde skrev, at medarbejdere forventede fremskridt på Hodge-formodningen, men OpenAI har ikke offentligt annonceret et Hodge-bevis. Påstande om, at en af de to formodninger allerede er løst, bør derfor behandles som rygter – ikke som matematiske resultater.

Det afgørende er den uafhængige gennemgang

Det næste afgørende skridt er ikke endnu en pressemeddelelse. Det er en uafhængig undersøgelse af det frigivne Navier–Stokes-materiale: ekspertgennemgang af argumentet, kontrol af Lean-projektet og dets afhængigheder samt klarhed over, hvilken konkret Clay-formulering der hævdes løst.

Hvis OpenAI fremsætter en ny påstand om et Millennium Prize-problem, vil den blive målt efter de samme standarder. Et overbevisende resultat bør ledsages af en præcis sætning, tilgængelige formelle og uformelle materialer, en gennemsigtig redegørelse for oprindelsen og nok forklaring til, at andre forskere kan afprøve og videreudvikle idéerne. I AI-assisteret matematik er korrekthed afgørende – men det samme gælder kreditering, åbenhed og menneskelig forståelse.