Newsletter Subscribe
Enter your email address below and subscribe to our newsletter
[forminator_form id="25163"]

qz+1garymarcus.substackcacm.acm+1OpenAI kunngjorde 1. august at deres uutgitte Astra-modellfamilie produserte løsninger på 10 langvarige uløste problemer innen matematikk og teoretisk informatikk, og publiserte et 249-siders manuskript samt fullstendig verifiserte Lean 4-bevis på GitHub. Resultatene spenner over felt som høydimensjonal geometri, kodeteori, gruppeteori, kvantekompleksitet og ekstremalkombinatorikk, der selskapet rapporterer at den totale beregningskostnaden var omtrent 2 000 dollar basert på GPT-5.6 Sol API-rater.ndtv+2
Ifølge OpenAIs blogginnlegg genererte Astra fremskritt innen kulepakking, feilkorrigerende koder og konstruksjonen av den første eksplisitte ikke-sofiske gruppen, en struktur som hadde forblitt et åpent spørsmål siden 1999. Modellen beviste også teoremet om kvanteparallell repetisjon for generelle tospillers sammenfiltrede spill og leverte resultater knyttet til Ehrharts volumformodning og Connes stivhetsformodning. Tre ytterligere problemer fra Paul Erdős katalog ble også løst, ifølge rapportering fra Quartz.qz+2
OpenAI uttalte at deres KI genererte de matematiske hovedargumentene, mens forskere deretter formaliserte hvert bevis ved hjelp av Lean-bevisassistenten. GitHub-repositoriets "sorry"-teller, en indikator på uverifiserte trinn, står på null, noe som betyr at hvert logiske trinn på tvers av alle ti bevisene er maskinkontrollert.qz
Til tross for den formelle verifiseringen, har kritikere stilt spørsmål ved om resultatene representerer et reelt sprang i KI-kapasitet. Gary Marcus, en fremtredende KI-forsker, skrev at en matematiker hos Anthropic, Levent Alpöge, var i stand til å delvis reprodusere halvparten av OpenAIs resultater i løpet av 24 timer ved bruk av Fable, en allerede offentlig tilgjengelig modell. Marcus argumenterte for at dette reiser tvil om hvorvidt Astra i seg selv er gjennombruddet, eller om fremskrittet ligger i å identifisere hvilke problemer som er egnet for søk-og-verifiser-teknikker.garymarcus.substack
"OpenAI rapporterer ikke hvilke problemer de prøvde og feilet på. De har gitt oss en teller uten nevner, alltid et bekymringsfullt tegn," skrev Marcus. Han bemerket også at OpenAI ennå ikke har bestemt om de skal betegne Astra som GPT-6 eller GPT-5.7, noe som antyder at spranget internt kan bli ansett som inkrementelt.garymarcus.substack
ACMs Communications-blogg publiserte en analyse 4. august som beskrev Astra som "fantastisk, men sterkt oversolgt". I mellomtiden har Leiden-erklæringen om KI i matematikk, signert av hundrevis av matematikere i juni 2026, flagget bredere bekymringer om upålitelige KI-genererte bevis og attribusjon.analyticsinsight+1
OpenAI har ikke kunngjort en utgivelsesdato for Astra, og modellen må gjennomgå føderal sikkerhetsvurdering for KI før den når brukere. Selskapet anerkjente debatten og uttalte at de har "dyp respekt og forståelse for de som er bekymret for konsekvensene" og planlegger å publisere metodikken sin. OpenAI lanserte også nylig ChatGPT for akademiske forskere, som gir 100 000 vitenskapsfolk gratis tilgang til deres nyeste modeller.analyticsinsight+1
Matematikeren Terence Tao trakk i en forelesning 26. juli, referert av Marcus, et skille mellom å løse isolerte åpne problemer, hvor KI virker sterk, og det å bygge matematisk teori, hvor det ennå ikke finnes bevis for KI-kapasitet.garymarcus.substack