Dette har OpenAI lagt ut
OpenAI har publisert grunnlaget for påstanden om å ha funnet en singularitet i endelig tid i de tredimensjonale Navier-Stokes-likningene: en redegjørelse på selskapets eget nettsted, en artikkel og maskinkontrollerbare bevisfiler i et offentlig GitHub-arkiv. Selskapet sier at det ikke akter å kreve Clay Mathematics Institutes millionpris for resultatet.
Det er forskjellen fra mandag, da påstanden bare fantes som en beskrivelse som gikk mellom forskere. Arkivet inneholder formaliseringer i Lean 4, bygget mot Mathlib og sluppet under Apache 2.0, for to Navier-Stokes-tilfeller med positiv viskositet — ett i hele rommet og ett på den periodiske torusen — samt en tilhørende Euler-konstruksjon. Den som har Lean installert, kan nå kjøre sertifikatet i stedet for å stole på ordet.
Tallene OpenAI oppgir
Beregningstallene kommer fra OpenAI og er ikke uavhengig etterprøvd. Selskapet opplyser at arbeidet brukte en intern modell det beskriver som betydelig kraftigere enn GPT-6 Astra, og at rundt 10 000 agenter kjørte parallelt i omtrent 88 timer i begynnelsen av september og produserte i størrelsesorden 130 milliarder utdatatokener. Ytterligere omtrent 17 timer, ifølge The Next Web, gikk med til å formalisere argumentet med GPT-6 Astra.
Det er innsatsfaktorer, ikke bevis. Beviset er Lean-filen, og Lean bryr seg ikke om hvor mange agenter som skrev den.
Hvorfor prisen ikke kreves
Clays formulering av Navier-Stokes-problemet er delt i fire utsagn. OpenAI sier at resultatet etablerer utsagn C og D: sammenbruddsalternativene, som løser problemet ved å vise fram en løsning som slutter å være glatt. Selskapet sier også at det ikke vil kreve prisen.
Grunnen ligger i konstruksjonen. Væsken starter i ro og en glatt ytre kraft legges på hele veien, og singulariteten oppstår under den kraften. Om et tvunget eksempel teller for det klassiske spørsmålet, er en vurdering for matematikere og for Clay, ikke for en bevisassistent. Instituttets egen side fører fortsatt Navier-Stokes som et åpent problem.
Striden om æren pågår fortsatt
Resultatet lander midt i en diskusjon Aivio News omtalte mandag. Tristan Buckmaster ved NYU og Levent Alpöge ved Anthropic la ut sine egne AI-assisterte og Lean-verifiserte blowup-bevis for likningene for porøst medium, Boussinesq og Euler, og Buckmaster publiserte en uttalelse om hvordan OpenAI kontaktet ham om tidspunkt og forfatterskap for Navier-Stokes-resultatet. OpenAIs Sébastien Bubeck kalte den framstillingen falsk og oppviglersk.
Quanta Magazine meldte at Charles Fefferman ved Princeton, som skrev den offisielle problemformuleringen, kalte Diego Córdoba og Luis Martínez-Zoroa historiens helter — paret hvis ikke-beregningsmessige metode begge innsatsene bygger på.
Hva man bør følge med på
To ting lar seg nå kontrollere i stedet for å diskuteres. Det første er om uavhengige matematikere kompilerer Lean-filene og bekrefter at de beviser det redegjørelsen sier. Det andre er om Clay Mathematics Institute sier noe om kraftledd. Inntil da er den ærlige beskrivelsen at det finnes en maskinverifisert singularitet, og at forholdet til prisspørsmålet er uavklart.
