OpenAI Astra løste ti matematiske opgaver der ikke har været løst i over 20 år

Den 1. august offentliggjorde OpenAI ti resultater, som en intern version af den kommende model Astra har genereret. Med i pakken fulgte et manuskript på 249 sider og et offentligt kodearkiv med maskinkontrollerbare Lean-beviser.

Historien er både større og mindre, end overskrifterne siger, og forskellen ligger i to ting: hvad Lean-beviserne faktisk garanterer, og hvad de 2.000 dollars faktisk dækker. Her er gennemgangen af, hvad der er dokumenteret, og hvad der stadig kun er en påstand.

Nyheden kort

OpenAI skriver, at en intern version af Astra, virksomhedens betegnelse for sin næste store model, har produceret løsninger på ti åbne problemer i matematik og teoretisk datalogi. Flere af dem har stået uløste i 20 til 30 år.

Listen indeholder blandt andet den første eksplicitte konstruktion af en såkaldt non-sofic gruppe, et modeksempel til Connes' rigidity conjecture, den første generelle forbedring af den øvre grænse for kuglepakning i høje dimensioner siden 1978, nye nedre grænser for beregning af permanenten og en sætning om eksponentielt fald ved parallel gentagelse af kvantespil. Tre af resultaterne knytter sig til problemer fra Paul Erdős' berømte samling.

Selve listen er svær at bedømme udefra, hvis man ikke er specialist i hvert enkelt felt. Det, der gør udmeldingen usædvanlig, er materialet, OpenAI lagde ved siden af den.

Tre lag af materiale, og hvorfor det tredje er det interessante

Sammen med meddelelsen offentliggjorde OpenAI et matematisk manuskript på 249 sider, et separat dokument med gennemgange af, hvordan argumenterne kom i stand, og et offentligt GitHub-arkiv med formaliseringer i Lean 4.

Lean er både et programmeringssprog og en interaktiv bevisassistent. Når et matematisk bevis skrives i Lean, oversættes det til et objekt, som en lille og velgennemgået kerne kan typetjekke maskinelt. Går tjekket igennem, har du en meget stærk garanti for, at konklusionen følger af de forudsætninger og aksiomer, der er skrevet ind.

Arkivet er låst til Lean 4.32.0 med tilsvarende faste versioner af standardbiblioteket mathlib. Metadatafilen angiver nul forekomster af sorry, som er Leans markør for et hul i et bevis, og kun de tre standardaksiomer propext, Classical.choice og Quot.sound, der bruges bredt i biblioteket. En optælling af de ti hovedmoduler ved det offentliggjorte commit giver omkring 548.000 linjer Lean-kode.

Der følger desuden en opskrift på at kontrollere formaliseringerne med Comparator, et værktøj der eksporterer bevisobjektet, afspiller det med en uafhængig checker og kontrollerer, at det beviste udsagn matcher en på forhånd fastlagt opgavebeskrivelse. Det er en usædvanlig høj grad af falsificerbarhed. OpenAI har i praksis stillet en offentlig prøve op, som enhver med tid og hardware kan gå til.

Hvad de ti resultater handler om, uden matematikstudier

Tre eksempler er nok til at forstå kalibret.

Non-sofic gruppe. Soficitet er en teknisk egenskab, som matematikere har kunnet påvise for enorme klasser af grupper. Spørgsmålet, om der overhovedet findes en gruppe uden egenskaben, har stået åbent siden omkring 1999. Ingen havde konstrueret et eksempel. Hvis konstruktionen holder, er svaret nu ja, og et helt delområde skal tænkes om.

Kuglepakning i høje dimensioner. Hvor tæt kan man pakke ens kugler, når rummet har mange dimensioner? Der findes en øvre grænse fra 1978, som ingen har kunnet forbedre generelt. Manuskriptet leverer en ny og skarpere grænse. Det betyder ikke, at man nu ved, hvordan man pakker kuglerne bedst. En øvre grænse fortæller, hvad der ikke kan lade sig gøre, ikke hvordan man gør det bedre.

Nærmeste vektor i et gitter. Her leveres et hårdhedsresultat for en klassisk gitteropgave. Nogle har straks koblet det til post-kvantekryptografi. Den kobling holder ikke: resultatet handler om worst case for en generel opgave, mens de udbredte krypteringsstandarder hviler på strukturerede gennemsnitsantagelser. Manuskriptet markerer selv den afstand.

Mønsteret gentager sig for de øvrige syv. Resultaterne er reelle fremskridt i afgrænsede, dybe delområder. Ingen af dem er en genvej til et produkt, en hurtigere algoritme eller en ny standard. Ingen af dem er "matematik løst".

Lean beviser noget meget præcist, og noget andet end du tror

De fleste omtaler går galt netop her, og pointen er værd at have med, uanset hvor teknisk du er.

Lean kan attestere, at det formaliserede udsagn følger logisk af de formaliserede definitioner og de registrerede aksiomer. Det er en anden og på nogle måder stærkere kontrol end almindelig fagfællebedømmelse, fordi en menneskelig læser kan overse et lokalt spring i et argument. Det gør maskinen ikke.

Lean kan derimod ikke afgøre fire ting, som er væsentlige for, om nyheden er sand som fortalt:

• Om den formaliserede sætning er den samme som den uformelle påstand i pressemeddelelsen. Et perfekt bevis af den forkerte formalisering er stadig et perfekt bevis.
• Om resultatet er nyt. En grøn kerne er ikke en litteratursøgning.
• Om resultatet er vigtigt, og hvor bredt det gælder.
• Om definitionerne modellerer det fænomen, matematikerne faktisk mener.

De fire spørgsmål kræver mennesker med specialviden i hvert enkelt felt. Pr. 2. august 2026 findes der ikke en offentlig, kapitel-for-kapitel gennemgang af hele pakken fra navngivne uafhængige specialister. Det er ikke en anklage. 249 sider på tværs af operatoralgebra, kombinatorik, kvantekompleksitet og gitterteori tager måneder at læse ordentligt, ikke timer. Men det betyder, at den præcise formulering lige nu er "ti offentliggjorte kandidater med usædvanligt stærk dokumentation", ikke "ti problemer er løst".

En detalje for dem, der selv vil kigge i koden: en hurtig søgning efter sorry i hele arkivet giver træffere. De ligger i Comparator-filerne, hvor hullerne er tilsigtede. Det er selve opgavebeskrivelserne, der bevidst mangler et bevis. Hovedresultaterne har dem ikke.

De 2.000 dollars, alle citerer

OpenAI skriver, at det samlede tokenforbrug, der skulle til for at finde løsningerne, ville koste omkring 2.000 dollars ud fra deres listepriser.

Tallet er efter alt at dømme rigtigt. Det bliver bare brugt forkert i næsten alle omtaler, vi har set.

De 2.000 dollars dækker de tokens, der førte til de ti resultater, du får at se. De dækker ikke træningen af Astra, som er hele forudsætningen. De dækker ikke de forsøg, der ikke førte nogen vegne. De dækker ikke de mennesker, der valgte problemerne, skrev manuskriptet færdigt og godkendte den endelige version. Og de dækker ikke den bedømmelse, som fagmiljøet nu skal levere gratis.

Der er også én nævner, vi ikke kender. OpenAI kalder selv materialet et "udvalg" af ti resultater. Vi får ikke at vide, hvor mange problemer der blev forsøgt, hvor mange spor der blev opgivet, eller hvornår. Uden det tal kan ti succeser ikke omregnes til en succesrate. Det er forskellen på "modellen løser åbne problemer" og "modellen løste ti problemer, vi valgte at vise jer".

Den forsvarlige gengivelse er: OpenAI estimerer den marginale tokenpris for selve løsningssøgningen til cirka 2.000 dollars.

Alt derudover kræver dokumentation, der ikke er offentliggjort.

Det, releasen ikke indeholder

Astra er ikke tilgængelig. Der er intet model-ID, ingen API-adgang, intet systemkort, ingen priser og ingen offentlig lanceringsdato. Du kan kontrollere artefakterne, men du kan ikke genskabe processen, der frembragte dem.

Dokumentet med gennemgange af ræsonnementet er heller ikke en rå tankeprotokol, altså modellens egen chain of thought. Det er ifølge sit eget resumé skrevet af en AI-model, der har læst de oprindelige spor og de færdige tekster og derefter rekonstrueret, hvordan beviset kom i stand. Det er nyttigt som forklaring, men en efterrationalisering bliver næsten altid pænere og mere lineær end den faktiske søgning.

Der er også et kildespørgsmål. Artiklen, manuskriptet og kodearkivet er tre stærke artefakter, men de kommer fra samme organisation. Tre OpenAI-links er ikke tre uafhængige bekræftelser.

Hvorfor skepsis er rimelig, og hvorfor kynisme ikke er

I oktober 2025 blev OpenAI-medarbejdere kritiseret for at omtale GPT-5 som den der løste de ti Erdős-problemer. Modellen havde i flere tilfælde fundet eksisterende litteratur, ikke fundet nye beviser. Matematikeren Thomas Bloom, der driver databasen over Erdős-problemer, kaldte fremstillingen dramatisk misvisende, og opslagene blev slettet eller præciseret. TechCrunch dækkede sagen grundigt.

Den historik beviser ingenting om Astra-pakken. Den begrunder en højere barre for ordene "løst", "nyt" og "billigt". Værd at bemærke: samme Thomas Bloom har ifølge The Next Web kaldt de nye resultater "big news".

Der er også en institutionel ramme nu. Leiden-erklæringen om AI og matematik, offentliggjort i juni 2026 og bakket op af Den Internationale Matematiske Union, anbefaler gennemsigtighed, uafhængig verifikation, korrekt kreditering og fastholdt menneskeligt ansvar, og kritiserer netop den praksis at annoncere resultater via pressemeddelelse frem for gennem fagfællebedømmelse. OpenAI henviser selv til erklæringen og tager eksplicit ansvar for korrektheden, men vælger organisatorisk forfatterskab og krediterer idéerne til modellen. Fields-medaljemodtageren Tim Gowers har skrevet indgående om, hvorfor det spørgsmål er svært at afgøre principielt.

Den modsatte refleks, at det hele bare er PR, er lige så doven. En offentlig tekst på 249 sider og en halv million linjer formalisering skaber reelle angrebspunkter. Hvis noget er galt, bliver det fundet, og det bliver dyrt for afsenderen. Den rimelige position er høj interesse kombineret med høj verifikationsstandard.

Hvad du kan bruge det til

Bruger du ChatGPT eller Claude til dit daglige arbejde, ændrer nyheden ingenting i dag. Der er ikke kommet en ny knap, og Astra kan ikke vælges nogen steder. Forvent, at metoderne gradvist forbedrer research- og kodeværktøjer, men der ligger ingen funktionsløfter i denne udmelding.

Den brugbare læring er en anden, og den er ret konkret. Astra-resultaterne er værd at tage alvorligt, fordi modellens output kunne køres gennem en billig, uafhængig kontrol, der ikke deler modellens fejl. Matematik er et af de få felter, hvor den kontrol allerede findes færdigbygget.

Det peger på et arkitekturvalg, der allerede er tilgængeligt for almindelige virksomheder: giv AI-output en maskinel gate, før et menneske bruger tid på det. Compileren, testsuiten, valideringsreglen, afstemningen, kontraktreglen, budgetkontrollen. Alt, hvad der kan afvise et forkert svar uden at spørge en model, om svaret er rigtigt. Det er kernen i det, der ofte kaldes troværdig og verificerbar AI, og det er den samme logik, der ligger bag arbejdet med verifikation af AI-agenters output.

Det praktiske spørgsmål lyder: hvilke af jeres dyre vidensopgaver har et output, som kan valideres maskinelt eller med en billig, uafhængig test? Er svaret kompilering, kontraktregler, balancesummer eller formelle sikkerhedskrav, er casen relevant. Er svaret brandtone eller juridisk rimelighed, er analogien svag, og I er henvist til at måle på noget andet, i praksis rigtige benchmarks på jeres egne opgaver frem for leverandørens.

Bottom Line

Det her er sandsynligvis det mest konkrete offentlige eksempel til dato på AI-assisteret matematisk forskning, netop fordi annonceringen er skruet sammen, så den kan modbevises.

Historien er ikke "ti umulige problemer løst for 2.000 dollars". Den er: en virksomhed med en klar interesse i sagen har lagt en stor, kontrollerbar forskningspakke frem. Lean fjerner risikoen for lokale logiske fejl. Adgangen til modellen mangler, den samlede økonomi er ukendt, og fagmiljøet er kun lige begyndt at læse.

Det er stadig en stor nyhed. Den bliver bare mere holdbar, hvis den fortælles præcist.