OpenAI har offentliggjort de første resultatene Astra, deres neste modell for kunstig intelligensSelskapet har gjort fremskritt på ti åpne problemer innen matematikk og teoretisk informatikk. Ifølge selskapet har noen av disse problemene vært uløste i over et tiår uten noen betydelig fremgang. Kunngjøringen, publisert 1. august 2026, har skapt betydelig begeistring i det vitenskapelige miljøet, selv om mange forskere oppfordrer til forsiktighet inntil resultatene er gjennomgått av uavhengige eksperter.
Det som skiller denne annonsen fra andre lignende er at OpenAI har ikke bare publisert resultatene, men også de formaliserte demonstrasjonene i Lean-verifiseringssystemet. Dette lar enhver matematiker automatisk sjekke om argumentene er riktige. Videre har selskapet detaljert oppdagelsesprosessen, inkludert 249 sider med argumenter og 62 sider med begrunnede notater, noe som gir uvanlig åpenhet i denne typen kommunikasjon.
De ti problemene og deres relevans
Problemene som Astra tar opp dekker svært ulike områder innen moderne matematikk. Blant dem er: tilbakevisningen av Connes' rigiditetsformodningDette resultatet har stor innvirkning på operatoralgebraer, og den eksplisitte konstruksjonen av ikke-sofiske grupper er et grunnleggende problem i gruppeteori. Nye øvre grenser er også oppnådd for sfærepakking i høye dimensjoner, et problem med direkte anvendelser i informasjonsteori og feilrettingskoder.
Innen kombinatorikk har Astra løst tre problemer stilt av den ungarske matematikeren Paul Erdős: problemer 146, 180 og 183. Det siste av disse, relatert til flerfargede Ramsey-tall, har blitt beskrevet av eksperten Thomas Bloom som «det mest overraskende på hele listen». Andre fremskritt inkluderer nye nedre grenser for aritmetiske kretser, en parallell repetisjonsteorem for kvantespill og resultater om tilnærmingshardheten til nærmeste vektorproblem, relevant for postkvantekryptografi.
Kostnad og metodikk
OpenAI har avslørt at Den totale tokenkostnaden for å finne disse løsningene var omtrent 2.000 dollar.I følge Sols API-rater inkluderer ikke dette tallet modelltrening eller arbeidet til menneskelige forskere. Prosessen kombinerte argumentgenerering fra Astra med ekspertinnspill som bidro til å konvertere disse argumentene til klare manuskripter og deretter til automatisk verifiserbare Lean-sertifikater.
Formalisering er nøkkelen i Lean: det lar alle med tilgang til programvaren bekrefte trinn for trinn at demonstrasjonen er logisk korrekt. Imidlertid, Matematikere må fortsatt bekrefte at definisjonene og antagelsene som brukes samsvarer med det opprinnelige problemet.Dette er noe en maskin ikke kan gjøre på egenhånd. OpenAI har tatt ansvar for å korrigere arbeidet, men har ikke identifisert noen uavhengig gruppe som har offentlig evaluert alle ti resultatene.
Sammenligning med Deep Blue og nødvendig forsiktighet
Flere medier har sammenlignet denne milepælen med Deep Blues seier over Garry Kasparov i 1997, men eksperter påpeker at Matematikk er mer komplekst enn sjakkI et spill er resultatet umiddelbart; i matematikk kan et bevis kreve måneder med fagfellevurdering før det blir akseptert. Dessuten er ikke Astra offentlig tilgjengelig, så eksterne forskere kan ikke reprodusere prosessen eller bestemme modellens feilrate.
OpenAI har tidligere erfaringer der tilsynelatende korrekte resultater viste seg å være feil etter gjennomgang av eksperter. I februar 2026 sendte selskapet inn løsninger for First Proof-utfordringen og erkjente senere at en av dem var feil. Derfor, Det vitenskapelige samfunnet insisterer på at disse ti fremskrittene bør behandles som lovende, men ikke som definitive.inntil de er uavhengig verifisert.
I Europa har forskere fra universiteter som Polytekniske Universitet i Madrid og Universitetet i Cambridge uttrykt interesse for å analysere Lean-sertifikatene som publiseres av OpenAI. Muligheten for at kunstig intelligens kan samarbeide i genereringen av ny matematisk kunnskap åpner en debatt om hvilken rolle menneskelige forskere kan spille i fremtiden, selv om selskapet understreker at valideringen og kontekstualiseringen av resultatene vil fortsette å avhenge av eksperter i mange år fremover.
Likevel markerer Astras kunngjøring et vendepunkt: kunstig intelligens er ikke lenger begrenset til å løse problemer med kjente svar, men begynner å foreslå originale argumenter om spørsmål som er i kunnskapens forkant. Det sanne «Deep Blue-øyeblikket» i matematikk kommer kanskje ikke med et eneste spektakulært resultat, men snarere gradvis, ettersom disse modellene blir samarbeidspartnere som er i stand til å utforske tusenvis av veier og formalisere resultater som ingen forsker tidligere har testet.
