AI mot AI: Astra hevder å ha løst ti matteproblemer – for rundt 2 000 dollar

Jacobian-formodningen ble først formulert av Ott-Heinrich Keller i 1939. Den er et åpent problem i algebraisk geometri og står som nummer 16 på Fields-medaljevinner Stephen Smales liste over problemer for det 21. århundret . Grovt forklart spør formodningen om en polynomavbildning fra C³ til C³, med en jacobideterminant som er en konstant ulik null overalt, nødvendigvis må være globalt inverterbar.

I 87 år hadde ingen funnet et moteksempel – eller et bevis. Alpöge arbeidet sammen med Anthropic-modellen Claude Fable 5 og fant en avbildning F = (P, Q, R): C³ → C³ med konstant jacobideterminant på −2. Samtidig sendte avbildningen tre ulike utgangspunkter til samme resultat. Det avkreftet formodningen direkte .

Resultatet ble formalisert i Lean 4, et system som gjør matematiske bevis maskinlesbare og kontrollerbare. Matematikere, blant andre Kevin Buzzard ved Imperial College London, verifiserte resultatet innen et døgn . Det ble omtalt som det vanskeligste matematiske problemet som til da var løst med hjelp av AI .

OpenAI: Ti resultater for rundt 2 000 dollar

1. august 2026 publiserte OpenAI et forskningsinnlegg om en intern versjon av Astra, selskapets «neste store modell». Ifølge OpenAI hadde modellen produsert nye resultater på ti åpne problemer i matematikk og teoretisk informatikk. Problemene hadde hatt liten eller ingen fremgang på hovedresultatet i minst ti år .

OpenAI publiserte et manuskript på 249 sider, modellens egne gjennomganger av resonnementene og Lean 4-sertifikater som kan kontrolleres av en maskin . Selskapet beregnet at den samlede tokenkostnaden for å finne løsningene ville vært rundt 2 000 dollar etter API-priser .

Dette er problemene Astra ifølge OpenAI ga resultater på:

• Ikke-sofiske grupper: En første eksplisitt konstruksjon av en ikke-sofisk gruppe, et spørsmål som har stått åpent siden Mikhail Gromov introduserte sofisitet i 1999 .
• Kretsgrenser for permanenten: Nye nedre grenser innen kretskompleksitet .
• Pakking av kuler i høy dimensjon: Nye øvre grenser for tettheten ved kulepakking, ned til Cohn–Elkies-terskelen .
• Binære og sfæriske koder: Eksponentielle forbedringer av klassiske øvre grenser .
• Operatoralgebraer: Et moteksempel til Connes’ rigiditetsformodning for gruppe-von Neumann-algebraer .
• Kvante-parallell repetisjon: Et resultat for kvantebasert parallell repetisjon i alle sammenfiltrede spill .
• Gitterkryptografi: Et nytt resultat om problemet med å finne den nærmeste vektoren .
• Ekstremal kombinatorikk: Løsninger på Erdős-problemene nummer 146, 180 og 183 .
• Geometri i høy dimensjon: En ny geometrisk konstruksjon .
• Ehrharts formodning: En løsning på et problem om opptelling av gitterpunkter .

GitHub-arkivet oppga en «sorry»-telling på null. I Lean betyr dette at ingen trinn i de formaliserte bevisene er stående som et ubekreftet hull . Det innebærer likevel ikke at alle resultatene allerede er faglig akseptert av matematikkmiljøet.

Anthropic svarer: Fable gjenskapte fem

Innen 24 timer etter OpenAIs kunngjøring skrev Levent Alpöge på X at han hadde brukt den offentlig tilgjengelige Claude Fable – ikke en uutgitt modell – til å løse fem av de samme ti problemene uavhengig .

Ifølge Alpöge:

• brukte han generelle instruksjoner og ingen internettilgang
• ble det lagt inn sikkerhetstiltak for å hindre at Fable kunne se OpenAIs løsninger
• produserte modellen resultatene selvstendig i løpet av noen timer
• omfattet arbeidene blant annet kretskompleksitet, kvante-parallell repetisjon, gitterkryptografi og problemet med nærmeste vektor
• brukte bare ett av de fem resultatene i hovedsak samme argument som Astra; de fire andre kan være uavhengige bevis

Alpöge hevdet ikke at Fable hadde løst alle ti. Poenget var at en modell som allerede var tilgjengelig for offentligheten, ifølge ham kunne gjenskape en betydelig del av Astras resultater med svært lite menneskelig veiledning . Den fullstendige koblingen mellom Fables fem resultater og Astras ti er imidlertid ikke offentlig dokumentert i detalj .

Hvorfor prislappen på 2 000 dollar er viktig

OpenAIs kostnadsanslag gjør pris til en ny konkurransefaktor i AI-kappløpet . Dersom modeller faktisk kan produsere nye matematiske resultater for noen hundre dollar per problem, kan flaskehalsen flyttes fra selve oppdagelsen til kontroll, forklaring og tolkning.

Samtidig sier beløpet ikke nødvendigvis alt om den reelle forskningskostnaden. Det beskriver den oppgitte tokenkostnaden ved modellens beregning etter API-priser, ikke nødvendigvis kostnadene ved modellutvikling, utvelgelse av problemer, menneskelig etterarbeid eller faglig kontroll. Selve Astra-modellen er dessuten ikke offentlig tilgjengelig.

Lean-bevis kan endre hvordan resultater kontrolleres

Både Jacobian-resultatet og Astras arbeider ble formalisert i Lean 4 . Et Lean-sertifikat tvinger frem en detaljert, maskinlesbar versjon av argumentet. Det kan gjøre kontrollen langt raskere enn tradisjonell gjennomgang alene, særlig når bevisene er lange eller teknisk krevende.

Det betyr ikke nødvendigvis at fagfellevurdering blir overflødig. Matematikere må fortsatt vurdere om problemene er formulert riktig, om resultatene faktisk er nye, og hvilken betydning de har. Men maskinverifiserte bevis kan bli et stadig viktigere supplement – og i enkelte typer arbeid den tekniske grunnmuren for godkjenningen .

Hvem er egentlig forfatteren?

Jacobian-resultatet reiste også et mer grunnleggende spørsmål: Hvem skal krediteres når en matematiker styrer en AI-modell mot et problem, modellen finner et mulig gjennombrudd, og mennesker kontrollerer og formaliserer det?

Er forfatteren forskeren som formulerte oppgaven? Modellen som foreslo konstruksjonen? Selskapet som bygde modellen? Eller alle som bidro til resultatet på ulike måter?

Alpöge krediterte både en menneskelig kollega og Claude Fable 5 i innlegget sitt . Akademiske tidsskrifter har foreløpig ingen standardisert praksis for AI som medforfatter, mens disse resultatene først ble spredt gjennom X og GitHub, snarere enn gjennom en vanlig publiseringsprosess .

Fortsatt grunn til varsomhet

Påstandene bør leses som foreløpige. Den nøyaktige listen over hvilke fem av Astras ti problemer Claude Fable skal ha gjenskapt, er ikke publisert i full detalj . Og selv om Lean-sertifikater gir en sterk, maskinell kontroll av formaliserte trinn, gjenstår den bredere faglige vurderingen av nyhetsgrad, formulering og betydning .

Likevel er utviklingen vanskelig å avfeie. På kort tid har AI gått fra å foreslå mellomregninger til å finne moteksempler og nye konstruksjoner i fagområder der mennesker har stått fast i tiår. For matematikerne kan det bety et kraftig nytt verktøy. For AI-selskapene betyr det at forskningsgjennombrudd, kostnad per resultat og spørsmålet om hvem som fortjener æren nå er blitt deler av den samme konkurransen.