Astra löste tio matematikproblem – men experter vill se mer än OpenAI:s bevis

Det som gör presentationen särskilt intressant är att resultaten inte bara publicerades som vanlig text. OpenAI formaliserade bevisen i Lean 4, ett verktyg som kan kontrollera matematiska argument steg för steg. Ett 249-sidigt manuskript och Lean-certifikat publicerades på GitHub .

Vilka problem tog Astra sig an?

Resultaten täcker ett ovanligt brett spektrum: högdimensionell geometri, kodteori, aritmetisk kretsteori, gruppteori, operatoralgebror, kvantkomplexitet, gitterkryptografi och extremal kombinatorik .

1. Packning av sfärer i höga dimensioner – nya övre gränser för packningstätheten, ned till Cohn–Elkies-tröskeln .
2. Binära och sfäriska koder – kraftigt förbättrade gränser för hur många koder som kan få plats vid ett givet minimiavstånd .
3. Icke-sofiska grupper – en explicit konstruktion som visar att icke-sofiska grupper existerar, en central öppen fråga inom gruppteori .
4. Connes rigiditetsförmodan – ett motbevis till en långvarig förmodan om von Neumann-algebror .
5. Aritmetisk kretsteori – nya undre gränser för att beräkna permanenten, bland annat en gräns av storleksordningen n⁴/log n för aritmetiska formler .
6. Parallell upprepning i kvantspel – en exponentiell parallellupprepningssats för allmänna kvantspel mellan två spelare .
7. Problemet med närmaste vektor – svårighet att approximera lösningen inom en polynomiell faktor, ett resultat med koppling till postkvantkryptografi .
8. Ehrharts volymförmodan – den största möjliga volymen hos en konvex kropp vars tyngdpunkt är dess enda inre heltalspunkt .
9. Ramseytal med flera färger – en superexponentiell undre gräns som löser Erdős problem 183 .
10. Förmodanden om extremala tal – resultat om kompakthet och degenerering som löser Erdős problem 146 och 180 .

Ett av de mest uppmärksammade resultaten är konstruktionen av en icke-sofisk grupp. Frågan har varit öppen sedan Mikhail Gromov introducerade begreppet soficitet 1999 .

Lean 4: ett viktigt kontrollsteg

OpenAI släppte inte själva Astra. I stället publicerade företaget Lean 4-certifikat under Apache 2.0-licensen. Kodförrådet rapporterades ha noll förekomster av sorry, vilket i Lean-sammanhang innebär att de formaliserade bevisen inte innehåller ofullständiga steg .

Det här skiljer sig från ett vanligt AI-svar som en människa måste läsa och bedöma. En proof assistant som Lean kontrollerar om varje formellt steg följer av de föregående. Det säger däremot inte i sig hur Astra hittade argumenten, hur urvalet gjordes eller hur stor roll människor spelade i problemformuleringen och den slutliga presentationen. OpenAI uppgav att mänskliga forskare tog fram de slutliga manuskripten med hjälp av samma modell .

Därför är forskarvärlden fortfarande försiktig

Mottagandet har varit delat. Forskare som Noam Brown har beskrivit beskedet som ett viktigt steg för vetenskapligt resonerande . Samtidigt har skeptiker pekat på flera begränsningar.

Det handlar inte om Millennieproblemen. Inget av de tio problemen är ett av Clay Mathematics Institutes sju Millennieproblem, som Riemannhypotesen eller frågan om P kontra NP . Problemen Astra tog sig an kan ändå vara seriösa och mycket svåra, men de har inte samma igenkänning eller symboliska tyngd.

Resultaten är ännu inte sakkunniggranskade. OpenAI presenterade arbetet direkt, utan föregående publicering i en granskad matematiktidskrift eller konferens . Därför återstår det för oberoende experter att kontrollera både nyheten och den matematiska betydelsen i resultaten.

Matematik är ett specialfall. Kognitionsforskaren Gary Marcus har argumenterat för att framgång i formell matematik inte automatiskt överförs till bredare vetenskapligt tänkande. Matematiska påståenden kan ofta kontrolleras symboliskt och träningsdata kan skapas billigt med garanterat korrekta svar – något som inte gäller för de flesta andra vetenskapsområden .

Astra går inte att återskapa ännu. Eftersom modellen inte är släppt och OpenAI inte har redovisat hela prompt- och arbetsmetoden, kan utomstående inte upprepa själva upptäcktsprocessen . Lean gör de publicerade bevisen möjliga att kontrollera, men ersätter inte full reproducerbarhet av hur resultaten kom till.

Tidpunkten väcker frågor. Presentationen sammanföll med att OpenAI positionerar Astra som sin nästa stora modellfamilj. Det har fått vissa bedömare att fråga sig om kommunikationen främst var vetenskaplig eller också utformad för att skapa kommersiell uppmärksamhet .

Vad betyder det här egentligen?

Om argumenten håller vid en noggrann expertgranskning skulle flera av resultaten stänga frågor som har varit öppna i årtionden. OpenAI har dessutom gjort betydligt mer material tillgängligt för inspektion än vad som är vanligt i ett företagsdrivet AI-utspel .

Men den större slutsatsen är fortfarande obekräftad. Astra kan ha visat imponerande förmåga inom formaliserbar matematik – utan att det ännu bevisar att modellen kan bedriva generell vetenskaplig forskning. Den mest försiktiga bedömningen är därför: potentiellt ett genombrott inom vissa delar av matematiken, men ännu inget bevis på att AI har löst vetenskapligt resonerande i bred bemärkelse.