Anthropics AI-modell Claude bevisade Fermats stora sats – helt själv

Anthropic uppger att bolagets AI-modell Claude under elva dagars i det närmaste autonomt arbete har tagit fram det första fullständiga, datorverifierade beviset för Fermats stora sats. Det skriver AI Weekly, som rapporterar att körningen skedde via plattformen Prove2Me och resulterade i 13 miljoner rader kod skriven i programmeringsspråket Lean.

Det här är Fermats stora sats

Fermats stora sats formulerades av matematikern Pierre de Fermat på 1600-talet och förblev obevisad i över 350 år. Satsen säger att ekvationen x^n + y^n = z^n saknar heltalslösningar för n större än 2. Den brittiske matematikern Andrew Wiles presenterade 1994 ett bevis som räknas som ett av de största genombrotten i modern matematik – men det byggde på decennier av mänskligt arbete och krävde omfattande granskning innan det accepterades.

Det Anthropic nu beskriver är något annat: att en AI-modell på egen hand konstruerat ett formellt, maskinverifierbart bevis i Lean – ett programmeringsspråk som används för att skriva matematiska bevis så att en dator kan kontrollera varje logiskt steg. Enligt AI Weekly bevisade Claude under processen över 30 000 delteorem på vägen mot slutresultatet.

Elva dagar utan mänsklig inblandning

Det som sticker ut i rapporteringen är hur lite mänsklig styrning som ska ha krävts. Claude arbetade i princip självständigt under elva dagar, byggde upp bevisstrukturen steg för steg och lät varje delsteg verifieras automatiskt av Lean-systemet innan modellen gick vidare. Det gör att beviset, till skillnad från många tidigare matematiska genombrott, är verifierat rad för rad av en dator snarare än enbart av mänskliga granskare.

Att en modell kan hålla ihop ett resonemang av den här längden och komplexiteten under så lång tid, utan att tappa tråden eller bygga in logiska fel, är i sig en signal om hur AI-modellers förmåga till uthålligt, självständigt arbete har utvecklats. Vi har tidigare skrivit om hur Claude presterar i vår jämförelse mellan ChatGPT, Claude och Gemini, och den här typen av långa, agentiska arbetspass är precis det område där Anthropics modeller ofta lyfts fram som starka.

Vad betyder det för svenska utvecklare och forskare?

För svenska universitet, tekniska högskolor och forskningsmiljöer som jobbar med formell verifiering är nyheten intressant av flera skäl. Formella bevissystem som Lean används redan inom både matematik och datavetenskap för att garantera att kod och algoritmer är korrekta – något som är särskilt relevant inom säkerhetskritisk mjukvara, kryptografi och AI-säkerhet. Om AI-modeller kan avlasta en stor del av det manuella, tidskrävande arbetet med att skriva formella bevis kan det påskynda forskning som annars tar år.

Det har också en praktisk koppling till utvecklarvärlden. Anthropics verktyg för autonomt kodande, som vi gått igenom i vår recension av Claude Code, bygger på samma typ av förmåga att arbeta självständigt över långa sekvenser av uppgifter. Att modellen nu visat sig klara av ett så pass krävande matematiskt projekt stärker bilden av att den här typen av agentiska AI-verktyg är på väg att bli allt mer kapabla, inte bara som kodassistenter utan som verktyg för avancerad forskning.

Vad vet vi inte än?

AI Weekly är hittills den källa som beskriver händelsen, och flera detaljer är fortfarande oklara – bland annat exakt hur mycket mänsklig vägledning som gavs innan och under processen, samt hur beviset kommer att granskas av den bredare matematikforskarvärlden. Det återstår att se om resultatet publiceras och genomgår samma typ av oberoende granskning som Wiles bevis en gång gjorde.

Oavsett hur den granskningen faller ut är själva demonstrationen tydlig: AI-modeller börjar klara av att hålla ihop extremt långa, logiskt krävande resonemang helt på egen hand. Det är samma typ av utveckling som ligger bakom den snabba framväxten av "vibe coding" och autonom mjukvaruutveckling – och något svenska forskare, utvecklare och företag gör klokt i att hålla ögonen på.