Certifikatet i koden: veckan då AI slutade be oss lita på den

Den 1 augusti lade OpenAI upp ett kodarkiv på GitHub. I det låg tio matematiska bevis, ett manuskript på 249 sidor och en samling filer skrivna i Lean 4, ett språk för så kallade bevisassistenter. Den siffra som fick matematiker att sätta kaffet i halsen var ingen av dem. Den var en nolla.

I Lean heter kommandot som markerar ett hål i ett bevis sorry. Den som formaliserar ett resonemang och kör fast skriver sorry, går vidare och återkommer senare. Antalet sorry i ett arkiv talar därför om exakt hur mycket som fortfarande är önsketänkande. I OpenAI:s arkiv stod räknaren på noll. Varje steg i alla tio bevisen var genomfört och maskinellt kontrollerat.

Vad som faktiskt löstes

Bakom resultaten står en intern version av Astra, den modellfamilj OpenAI beskriver som sitt nästa stora steg och som är byggd för uppgifter som löper över timmar eller dygn. Problemen den tog sig an hade alla stått olösta i tio år eller mer, och de ligger spridda över gruppteori, von Neumann-algebror, högdimensionell geometri, kodningsteori, kvantkomplexitet, gitterkryptografi och extremal kombinatorik.

Huvudnumret är en explicit konstruktion av en icke-sofisk grupp. Begreppet soficitet formulerades av Mikhail Gromov 1999, och frågan om det över huvud taget finns grupper som inte uppfyller villkoret har varit öppen sedan dess. Den är nu besvarad. Därutöver motbevisades Connes rigiditetsförmodan, Ehrharts volymförmodan bevisades, och tre problem ur Paul Erdős katalog över öppna frågor ströks från listan.

Varför nollan är själva nyheten

Ett år av AI-nyheter har handlat om påståenden. En modell sägs klara ett prov, en annan sägs ha slagit ett rekord, och läsaren får lita på den som håller i måttbandet. Här är det annorlunda. Lean är ett program vars kärna gör en enda sak: den accepterar ett bevis eller förkastar det. Något däremellan finns inte. Den som är skeptisk behöver alltså inte lita på OpenAI, inte på en benchmark och inte på en pressrelease. Det räcker att ladda ner arkivet och köra kompilatorn.

Den som har köpt en sten hos en juvelerare känner igen mekanismen. Ett GIA-certifikat är inte säljarens ord, det är ett intyg från tredje part som går att kontrollera oberoende av vem som står bakom montern. En kronometerstämpel från COSC fungerar likadant. Lyxbranschen löste förtroendefrågan för över hundra år sedan genom att flytta beviset från personen till dokumentet. Augusti 2026 är första gången ett stort AI-resultat kommer med samma sorts intyg, och till skillnad från stenens certifikat kostar det ingenting att kontrollera.

Vad certifikatet inte lovar

Här tar de goda nyheterna slut för den som hoppats på en ren maskinseger. Ett Lean-certifikat garanterar att varje logiskt steg håller. Det säger ingenting om huruvida en människa förstår varför satsen är sann. De två sakerna är inte samma sak, och skillnaden visade sig omedelbart.

Nio matematiker, bland dem Fields-medaljören Timothy Gowers och Noga Alon, publicerade kort därefter en följeskrift vars enda syfte var att förklara beviset så att andra matematiker kan följa det. Gowers har sagt att han utan tvekan hade rekommenderat resultatet för publicering i en ledande tidskrift. Att nio personer ändå behövde skriva om det säger en del om avståndet mellan maskinellt kontrollerat och mänskligt begripligt.

Thomas Bloom vid University of Manchester, som förvaltar katalogen över Erdős problem, kallade resultaten stora nyheter och lade till den viktigaste reservationen: systemet vilar på över ett sekel av matematisk teori, det byggdes av matematiker och det tränades på i stort sett allt matematiker någonsin skrivit. Människor var med hela vägen även den här gången, bland annat med att formalisera bevisen och färdigställa manuskriptet, och exakt var gränsen går mellan modellens och forskarnas bidrag har OpenAI inte redovisat. Kvar står också ett arbete som ingen kompilator utför åt någon: att kontrollera att den formella satsen verkligen motsvarar det problem man trodde var öppet, och att avgöra hur mycket resultatet flyttar sitt fält.

Prislappen

En siffra återstår. OpenAI uppskattar att de tokens som krävdes för att hitta samtliga tio lösningar hade kostat omkring 2 000 dollar till API-priserna för företagets modell Sol. Ungefär vad ett par ordentliga skor går på.

Noam Brown, forskaren bakom modellernas förmåga att tänka längre innan de svarar, tillade två saker. Den ena: inga Millennieproblem, ännu. Den andra är mer intressant. Man lade inte särskilt mycket beräkningskraft på varje enskilt problem, och det går att skruva upp den siffran rejält.

Det är den meningen värd att fästa sig vid. Det som blev billigt den här veckan var inte att lösa svåra problem, utan att kontrollera om lösningen håller. Det dyra flyttade uppåt: att veta vilken fråga som är värd att ställa, och att förstå svaret när det väl ligger på bordet. Precis som med stenen i montern är certifikatet en förutsättning, inte en förklaring.