Det her har OpenAI lagt ud
OpenAI har offentliggjort grundlaget for påstanden om at have fundet en singularitet i endelig tid i de tredimensionelle Navier-Stokes-ligninger: en redegørelse på selskabets eget site, en artikel og maskinkontrollerbare bevisfiler i et offentligt GitHub-arkiv. Selskabet siger, at det ikke agter at gøre krav på Clay Mathematics Institutes millionpris for resultatet.
Det er forskellen fra mandag, hvor påstanden kun fandtes som en beskrivelse, der gik mellem forskere. Arkivet indeholder formaliseringer i Lean 4, bygget mod Mathlib og udgivet under Apache 2.0, for to Navier-Stokes-tilfælde med positiv viskositet — et i hele rummet og et på den periodiske torus — samt en tilhørende Euler-konstruktion. Den, der har Lean installeret, kan nu køre certifikatet i stedet for at tage påstanden på ordet.
Tallene, OpenAI opgiver
Beregningstallene kommer fra OpenAI og er ikke efterprøvet uafhængigt. Selskabet oplyser, at arbejdet brugte en intern model, som det beskriver som betydeligt stærkere end GPT-6 Astra, og at omkring 10.000 agenter kørte parallelt i cirka 88 timer i begyndelsen af september og producerede i størrelsesordenen 130 milliarder outputtokens. Yderligere omkring 17 timer, ifølge The Next Web, gik med til at formalisere argumentet med GPT-6 Astra.
Det er input, ikke bevis. Beviset er Lean-filen, og Lean er ligeglad med, hvor mange agenter der skrev den.
Hvorfor prisen ikke kræves
Clays formulering af Navier-Stokes-problemet er delt i fire udsagn. OpenAI siger, at resultatet etablerer udsagn C og D: sammenbrudsalternativerne, som løser problemet ved at fremvise en løsning, der holder op med at være glat. Selskabet siger også, at det ikke vil kræve prisen.
Grunden ligger i konstruktionen. Væsken starter i hvile, og en glat ydre kraft lægges på hele vejen, og singulariteten opstår under den kraft. Om et tvunget eksempel tæller for det klassiske spørgsmål, er en vurdering for matematikere og for Clay, ikke for en bevisassistent. Instituttets egen side fører stadig Navier-Stokes som et åbent problem.
Striden om æren kører stadig
Resultatet lander midt i en diskussion, Aivio News beskrev mandag. Tristan Buckmaster fra NYU og Levent Alpöge fra Anthropic lagde deres egne AI-assisterede og Lean-verificerede blowup-beviser ud for ligningerne for porøst medium, Boussinesq og Euler, og Buckmaster offentliggjorde en udtalelse om, hvordan OpenAI henvendte sig til ham om tidspunkt og forfatterskab for Navier-Stokes-resultatet. OpenAI’s Sébastien Bubeck kaldte den fremstilling falsk og opildnende.
Quanta Magazine skrev, at Charles Fefferman fra Princeton, der forfattede den officielle problemformulering, kaldte Diego Córdoba og Luis Martínez-Zoroa for historiens helte — parret, hvis ikke-beregningsmæssige metode begge indsatser bygger på.
Hvad man skal holde øje med
To ting kan nu kontrolleres i stedet for at diskuteres. Det første er, om uafhængige matematikere kompilerer Lean-filerne og bekræfter, at de beviser det, redegørelsen siger. Det andet er, om Clay Mathematics Institute udtaler sig om kraftled. Indtil da er den ærlige beskrivelse, at der findes en maskinverificeret singularitet, og at dens forhold til prisspørgsmålet er uafklaret.
