Lean godkender Claudes Fermat-bevis

Lean, som matematikere verden over bruger til at kontrollere formelle beviser, har godkendt en fuldstændig formel version af Fermats sidste sætning. Formaliseringen er udarbejdet af Anthropics Claude-system og offentliggjort i et åbent arkiv. Den indeholder hverken uløste pladsholdere, ekstra aksiomer eller beregningsmæssige genveje ud over Leans standardfundament (repository). Kevin Buzzard, matematiker ved Imperial College London og leder af sit eget formaliseringsprojekt, har uafhængigt kompileret projektet og bekræftet, at kontrollen går igennem. Han kalder resultatet »en ekstraordinær præstation inden for automatisk formalisering« (Buzzard).

Selve matematikken har været afklaret længe. Andrew Wiles beviste sætningen i 1995, og resultatet har ikke siden været alvorligt bestridt blandt matematikere. Den resterende opgave var at omskrive beviset til instruktioner for en bogstavelig kontrollør, som kræver samtlige definitioner og mellemregninger, også dér hvor en matematiker uden videre kan springe flere skridt over. Ifølge Anthropic gennemførte snesevis af AI-agenter arbejdet på 11 dage i august. De arbejdede parallelt gennem platformen Prove2Me (Anthropic).

De 11 dage beskriver dog et forløb, som udenforstående ikke kan gentage. Hverken den interne model, infrastrukturen til at koordinere agenterne, operatørernes beslutninger eller regneforbruget indgår i offentliggørelsen. Slutproduktet kan derimod efterprøves: Enhver med tilstrækkelig computerkapacitet kan kompilere Lean-projektet og kontrollere, at beviset består. Anthropic har desuden verificeret det samme formelle materiale med et særskilt kontrolprogram skrevet i Rust, som fandt alle 1.052.234 deklarationer konsistente (technical report). Det er en ekstra kontrol af den færdige tekst, ikke en uafhængig gentagelse af det 11 dage lange arbejde.

Sådan arbejdede agenterne

At formalisere et bevis vil sige at omskrive matematikerens argument, så et program uden matematisk intuition kan kontrollere hvert logisk skridt. Selve sætningen er enkel at formulere: For enhver heltallig eksponent på mindst tre findes der ingen tre positive hele tal, som opfylder aⁿ + bⁿ = cⁿ. Beviset bevæger sig imidlertid gennem dybe dele af talteorien og strækker sig over flere hundrede sider.

Claude fandt ikke frem til ny matematik. Systemet formaliserede den kendte kæde af resultater frem mod Wiles’ bevis med udgangspunkt i en fremstilling af matematikerne Henri Darmon, Fred Diamond og Richard Taylor (Anthropic, technical report). Den matematiske nytænkning kom fra Wiles og hans forgængere. Claudes bidrag var at omsætte deres arbejde til omtrent 10,5 millioner linjer kode, som en maskine kan kontrollere (technical report).

Prove2Me-platformen, som er udviklet af Anthropic-forskeren Tianyi Peng sammen med forskere fra Columbia University, opdelte beviset i en afhængighedsgraf med omkring 29.511 selvstændige påstande (technical report). Agenterne valgte påstande, hvor de nødvendige forudsætninger allerede var på plads, skrev beviserne i Lean og kontrollerede hinandens formuleringer. Dermed kunne mange dele løses samtidig. Arbejdet brugte omtrent seks milliarder outputtokens fra en intern forskningsmodel (technical report).

Ifølge Anthropic skrev de menneskelige operatører ingen Lean-kode under kørslen. De valgte dog sætningen og den kendte vej til beviset, byggede infrastrukturen omkring agenterne og justerede lejlighedsvis prioriteringen (Anthropic). Anthropic har hverken offentliggjort hele operatørloggen eller oplyst omkostningerne til computerkraft.

Bygger på års menneskeligt forarbejde

Resultatet bygger på Mathlib, det store fællesskabsdrevne bibliotek over formaliseret matematik, og anvender direkte materiale fra to tidligere projekter. Buzzards hold ved Imperial begyndte i slutningen af 2023 at opbygge en Lean-formalisering af Fermats sidste sætning med støtte fra en EPSRC-bevilling på 1 million pund, som efter planen løber til 2029 (EPSRC award). Et andet fællesskabsprojekt havde allerede formaliseret sætningen for en del af tilfældene. Anthropics oversigt over bidrag angiver 106 filer med materiale, der er hentet eller bearbejdet fra disse projekter (attribution).

Den parallelle arbejdsform betyder, at de 11 kalenderdage ikke kan sammenlignes direkte med det antal arbejdstimer, Buzzards hold har lagt i projektet. Da Claudes arbejde begyndte, havde holdet været finansieret i omkring 22 måneder (EPSRC award). Anthropic har hverken oplyst antallet af GPU-timer eller energiforbruget.

Før offentliggørelsen var Fermats sidste sætning det eneste udestående punkt på Freek Wiedijks liste over 100 vigtige sætninger, som endnu ikke var formaliseret. Listen har i to årtier fungeret som målestok for udviklingen på området (Buzzard).

Den afgørende prøve bliver, om metoden også virker på nyere og dårligere dokumenteret matematik, hvor der hverken findes en detaljeret køreplan, modne biblioteker eller tidligere formaliseringsarbejde. Her var opgaven en berømt sætning med en betydelig infrastruktur på plads. Resultatet viser, at AI-agenter med adgang til en kendt bevisvej og menneskeligt forarbejde kan levere en fuldstændig formalisering, som Lean godkender, og som andre kan kontrollere. Det offentliggjorte materiale gør fortsat ikke selve fremstillingsprocessen reproducerbar.