Matematikerne etterprøver OpenAI: Bare én av 30 tallteoriartikler er verifisert i Lean
Uken etter 6. oktober 2026 sto matematikernes fagfellesskap overfor noe helt nytt: en enkelt utgivelse med hundrevis av påståtte løsninger på åpne forskningsproblemer – og et fagmiljø med begrenset kapasitet til å etterprøve dem. Bevisbyrden er nå flyttet fra de som hevder resultatene til de som skal kontrollere dem.
Hva som faktisk skjedde
OpenAI publiserte en database med påståtte bevis for en lang liste over åpne problemer i matematikk og informatikk. Nøyaktig hvor mange resultater som inngår, er uavklart: Globes og New Scientist omtaler 722 studier, TechCrunch 719 manuskripter, og The New York Times 377 funn. Tallsammenhengen tyder på at kildene delvis omtaler ulike enheter – studier, manuskripter og funn – men ingen av tallene kan fastslås som «riktig» utfra tilgjengelig dekning. Resultatene spenner ifølge The New York Times over algebra, tallteori, teoretisk informatikk, matematisk logikk og topologi, og ble publisert tirsdag 6. oktober med en «mer avansert modell som ikke er utgitt», som avisen beskriver det.
Samtidig, ifølge Globes, offentliggjorde Amnon Shashua at selskapet hans doubleAI har løst det lengste stiproblemet i grafteori – et problem selskapet hevder har vært uløst i 38 år – til en kostnad under 2 000 dollar, med en ny algebraisk formel som skal heve en konstant fra 4/3 til 1,6. Alle disse tallene stammer fra Shashuas innlegg på X og er ikke uavhengig verifisert.
Utgivelsen kom litt over en måned etter at OpenAI annonserte en løsning på et problem utledet fra Navier–Stokes-ligningene – en kontroversiell utgivelse som fagmiljøet hevdet brøt med etablerte normer. Det er mot dette bakteppet matematikerne nå reagerer.
Hva som faktisk hevdes bevist
Til tross for overskriftene i dekningen er ikke Riemann-hypotesen hevdet løst. OpenAI fremmer ifølge Globes et bevis for en svakere versjon, kalt «Quasi-Riemann-hypotesen» – beskrevet som et betydelig steg mot et av matematikkens største mysterier. Blant de øvrige resultatene er et bevis for irrasjonaliteten til Catalans konstant, en versjon av Hilberts tiende problem om rasjonelle løsninger, samt fremgang på Nagatas og Goldfelds formodninger.
New Scientist omtaler et av de mest slående tilfellene: matematikeren Francis Johnson, som har arbeidet i 25 år på Walls D(2)-problem, uttrykte undring over at det skulle være løst. OpenAI nektet å navngi modellen bak funnene, og oppga kun at det var en «internal frontier model» – et internt grensemodellsystem – ifølge New Scientist.
Slik skulle kontrollen fungere – og hvor den bryter sammen
Formell verifisering i matematikk går normalt via Lean, et bevisassistentspråk der maskinsjekkbare bevis kan etterprøves «uten rimelig tvil», som New Scientist beskriver det. Kjeden er: naturlig-språklig bevis, formell oversettelse til Lean, deretter ekspertgjennomgang og fagfellevurdering.
OpenAIs utgivelse bryter på flere punkter i denne kjeden:
- Ifølge TechCrunch var det kun 10 av 719 manuskripter som inkluderte modellens resonnementkjede – det vil si selve bevisføringen maskinen gjennomførte.
- 42 prosent av bevisene hadde ikke gjennomgått Lean-formalisering i det hele tatt.
- Tallteoretikeren Kevin Buzzard ved Imperial College London fortalte New Scientist at utgivelsen inneholdt 30 artikler relevante for hans felt, men at bare syv virket imponerende, og bare ett var formelt verifisert i Lean. De resterende, uformaliserte resultatene må ifølge Buzzard vente på ekspertsjekk.
Et separat problem dokumenterer forskere ved University of Cambridge og King's College London i en artikkel med tittelen «lost in translation»: minst to diskrepanser mellom det naturlig-språklige beviset og Lean-koden bak OpenAIs Navier–Stokes-avledede løsning. Konklusjonen deres er at slike autoformaliserte bevis ikke bør stoles på uten fagfellevurdering. Det er verdt å merke seg: diskrepansene motbeviser ikke løsningene, men viser at selve oversettelsen fra språklig argument til maskinsjekkbar kode kan være feilbehaftet.
Rådgivergruppen som ba om akkurat det OpenAI gjorde
OpenAI sa at de hadde konsultert en rådgivergruppe av elite-matematikere – AGMAI, en ni-medlemmers gruppe tilknyttet Institute for Advanced Study – for å unngå kontroversen fra Navier–Stokes-utgivelsen. Gruppen utstedte retningslinjer ved utgangen av september 2026. Ifølge TechCrunch var gruppens første anmodning å «slutte å teste avanserte matematiske problemer på proprietære modeller». OpenAIs utgivelse sier eksplisitt at selskapet evaluerer sine proprietære modeller på åpne forskningsproblemer i matematikk – altså nøyaktig det gruppen ba om å la være.
I tillegg har 25 vinnere av Fields-medaljen, matematikkens mest prestisjefylte pris, skrevet et åpent brev som advarer mot å gjøre forskningsproblemer til benchmarks for å demonstrere modellkraft. Argumentet er at «masseproduksjon» av løsninger ikke gir fagmiljøet tid til å fordye seg i idéene eller tilskrive tidligere arbeid.
Det manglende menneskelige forståelsesnivået
Terence Tao, en av verdens mest innflytelsesrike matematikere og en gjentatt OpenAI-kritiker, skrev etter utgivelsen på sosiale medier at problemer løses autonomt av «AI-promptere som ikke er interessert i selve det bredere feltet når det opprinnelige målet er «løst», og som ikke forstår AI-resultatene godt nok til å svare på spørsmål om resultatet, holde foredrag eller på annen måte samhandle med resten av fagmiljøet», som TechCrunch gjengir.
Harvard-professor i matematikk Melanie Wood formulerte det til TechCrunch slik: det finnes «ikke menneskelig forståelse av dem på utgivelsestidspunktet, og nå begynner arbeidet». Poenget er ikke at resultatene nødvendigvis er feil – men at matematikk som fagtradisjon bygger på at noen faktisk forstår og kan forklare et bevis, ikke bare at maskinvaren har produsert en tekst.
Hva som gjenstår uavklart
Flere forhold gjør at verken OpenAIs eller doubleAIs resultater kan behandles som etablert matematikk:
- Ingen av bevisene er uavhengig verifisert. Lean-formalisering mangler for 42 prosent av manuskriptene, og selv der den finnes, har Cambridge/King's College-funnene vist at den kan avvike fra det naturlig-språklige beviset.
- OpenAI har ikke navngitt modellen, kun omtalt den som en intern grensemodell, noe som gjør uavhengig reproduksjon av resultatene vanskeligere.
- doubleAIs påstander om det lengste stiproblemet – kostnaden under 2 000 dollar, konstantforbedringen fra 4/3 til 1,6, og 38 år med uløsthet – hviler utelukkende på Shashuas innlegg på X, som Globes har gjengitt, og har ingen primærkildedokumentasjon i dekningsgrunnlaget.
- OpenAIs sammenligning av regnekostnader – i gjennomsnitt rundt tre timer med ChatGPT Pro per løsning i den nye utgivelsen, mot 10 000 agenter og millioner av dollar for Navier–Stokes – er en selskapspåstand gjengitt via Globes, ikke et uavhengig funn.
Det skal også sies at all kunnskap om saken i denne rapporten stammer fra sekundær dekning – TechCrunch, New Scientist, Globes og The New York Times – uten at OpenAIs database, AGMAI-retningslinjene, Fields-brevet eller Shashuas innlegg er direkte tilgjengelige for verifisering.
Hva som skal til før dette teller som matematikk
Det er fristende å lese saken som en kamp mellom rask AI og langsom akademia. Men kritikken fra fagmiljøet er mer presis: matematikk skiller ikke mellom å finne et argument og å sertifisere det. Lean-formalisering uten diskrepanser, navngitte modeller, offentliggjorte resonnementkjeder, og utgivelsespraksis som gir fagmiljøet tid til å fordøye og kredittere arbeid – det er kriteriene Buzzard, Wood, Tao, Fields-medaljene og AGMAI i praksis peker på. Inntil noen av dem er innfridd, er det mest korrekte å si at OpenAI har publisert hundrevis av påstander, ikke hundrevis av bevis.