Et bevis, en maskine kan kontrollere
Anthropic meddelte 4. september, at en intern forskningsmodel har lavet det første bevis for Fermats sidste sætning, som en computer kan kontrollere fra ende til anden. Formaliseringen fylder omkring 13 millioner linjer Lean, det bevisværktøj matematikere bruger til at tvinge hvert skridt i et ræsonnement ind i en form, en maskine kan verificere. Arbejdet tog elleve dage, oplyser selskabet.
Fermats sidste sætning siger, at ingen tre positive heltal opfylder a^n + b^n = c^n for noget heltal n større end to. Andrew Wiles beviste den i 1995 i en artikel på omkring 129 sider, bygget på maskineri udviklet gennem hele 1900-tallet. At gennemgå et sådant bevis i hånden tager specialister år. At formalisere det ventedes at tage omtrent lige så lang tid.
Hvad modellen faktisk gjorde
Ifølge Anthropic var systemet en intern forskningsmodel til almene formål, omtrent på niveau med Claude Fable 5.1, ikke en specialbygget matematikmotor. Flere dusin agenter arbejdede parallelt, genererede omkring seks milliarder tokens og beviste 30.300 sætninger, hvoraf 29.500 indgår i slutresultatet. Den menneskelige indsats var begrænset til overordnet styring.
Anthropic oplyser, at de første forsøg mislykkedes helt. Den kørsel, der lykkedes, hvilede på en intern platform, selskabet kalder Prove2Me, som holder styr på, hvilke sætninger der afhænger af hvilke, og lader mange agenter arbejde på forskellige grene af samme bevis uden at miste tråden. Omkring syv procent af de ikke-rutinemæssige linjer i slutfilen kom fra de mislykkede forsøg.
Det menneskelige forarbejde under resultatet
Resultatet opstod ikke ud af ingenting. Det følger en forenklet udgave af Wiles’ ræsonnement fremlagt af Henri Darmon, Fred Diamond og Richard Taylor, og hviler på Mathlib, det matematikbibliotek tusindvis af bidragydere har bygget i Lean i mere end et årti, og på det formaliseringsprojekt, Kevin Buzzard leder ved Imperial College London. Buzzard, der gennemgik resultatet, sammenfattede betydningen som et spørgsmål om pålidelighed: artefakterne er nu robuste nok til at bygge videre på, sagde han.
Anthropic pegede selv på begrænsninger. Beviset hviler alene på Leans tre standardaksiomer, og en sammenligner bekræftede, at den påstand, der bevises, svarer til Mathlibs formulering af sætningen — den kontrol, der forhindrer et system i at bevise noget lidt svagere, end det giver sig ud for. Men selskabet siger også, at beviset formentlig er langt længere, end det behøver at være, hvilket betyder noget for den, der vil genbruge delene.
Hvorfor formaliseringen er det interessante
Matematikken har i årtier haft en flaskehals i kontrollen: beviser i forskningsfronten er så lange, at kun en håndfuld mennesker kan bedømme dem, og fejl har overlevet publicering. Formalisering fjerner bedømmerproblemet, til prisen af en enorm mængde tålmodighedsarbejde. Den afvejning har holdt den sjælden.
Kan den tålmodighedskrævende halvdel automatiseres i denne skala, ændrer regnestykket sig. Det føjer sig også til en række lignende udmeldinger: Anthropic offentliggjorde i august arbejde om, at Claude fandt nye resultater omkring Riemanns zetafunktion, og OpenAI har oplyst, at modellen Astra løste flere åbne Erdős-problemer.
Det, der er værd at følge, er uafhængigt genbrug. En Lean-fil på 13 millioner linjer er verificerbar allerede i kraft af sin konstruktion — det er hele pointen med Lean — men værdien for arbejdende matematikere afhænger af, om mellemsætningerne kan løftes ind i Mathlib og bruges andre steder. Anthropic har ikke sagt hvornår, eller om, hele artefakten frigives til det formål.
