Et bevis en maskin kan kontrollere
Anthropic meldte 4. september at en intern forskningsmodell har laget det første beviset for Fermats siste sats som en datamaskin kan kontrollere fra ende til annen. Formaliseringen er på rundt 13 millioner linjer Lean, bevisverktøyet matematikere bruker for å tvinge hvert steg i et resonnement inn i en form en maskin kan verifisere. Arbeidet tok elleve dager, opplyser selskapet.
Fermats siste sats sier at ingen tre positive heltall oppfyller a^n + b^n = c^n for noe heltall n større enn to. Andrew Wiles beviste den i 1995 i en artikkel på omtrent 129 sider, bygget på maskineri utviklet gjennom hele 1900-tallet. Å gå gjennom et slikt bevis for hånd tar spesialister år. Å formalisere det ble ventet å ta omtrent like lang tid.
Hva modellen faktisk gjorde
Ifølge Anthropic var systemet en intern forskningsmodell for generelle formål, omtrent på linje med Claude Fable 5.1, ikke en spesialbygd matematikkmotor. Flere dusin agenter arbeidet parallelt, genererte rundt seks milliarder tokens og beviste 30 300 setninger, hvorav 29 500 inngår i sluttresultatet. Den menneskelige innsatsen var begrenset til overordnet styring.
Anthropic opplyser at de første forsøkene mislyktes helt. Kjøringen som lyktes, hvilte på en intern plattform selskapet kaller Prove2Me, som holder orden på hvilke setninger som avhenger av hvilke, og lar mange agenter arbeide på ulike greiner av samme bevis uten å miste tråden. Rundt sju prosent av de ikke-rutinemessige linjene i sluttfilen kom fra de mislykkede forsøkene.
Det menneskelige forarbeidet under resultatet
Resultatet oppsto ikke av ingenting. Det følger en forenklet versjon av Wiles’ resonnement lagt fram av Henri Darmon, Fred Diamond og Richard Taylor, og hviler på Mathlib, matematikkbiblioteket tusenvis av bidragsytere har bygget i Lean i mer enn et tiår, og på formaliseringsprosjektet Kevin Buzzard leder ved Imperial College London. Buzzard, som gikk gjennom resultatet, oppsummerte betydningen som et spørsmål om pålitelighet: artefaktene er nå robuste nok til å bygge videre på, sa han.
Anthropic pekte selv på begrensninger. Beviset hviler bare på Leans tre standardaksiomer, og en sammenligner bekreftet at påstanden som bevises stemmer med Mathlibs formulering av satsen — kontrollen som hindrer et system i å bevise noe som er litt svakere enn det utgir seg for. Men selskapet sier også at beviset trolig er langt lengre enn nødvendig, noe som betyr noe for den som vil gjenbruke delene.
Hvorfor formaliseringen er det interessante
Matematikken har i tiår hatt en flaskehals i kontrollen: bevis i forskningsfronten er så lange at bare en håndfull mennesker kan vurdere dem, og feil har overlevd publisering. Formalisering fjerner vurdererproblemet, til prisen av en enorm mengde tålmodighetsarbeid. Den avveiningen har holdt den sjelden.
Kan den tålmodighetskrevende halvdelen automatiseres i denne skalaen, endrer regnestykket seg. Det føyer seg også inn i en rekke lignende utspill: Anthropic publiserte i august arbeid om at Claude fant nye resultater rundt Riemanns zetafunksjon, og OpenAI har opplyst at modellen Astra løste flere åpne Erdős-problemer.
Det som er verdt å følge, er uavhengig gjenbruk. En Lean-fil på 13 millioner linjer er verifiserbar allerede i kraft av konstruksjonen — det er hele poenget med Lean — men verdien for arbeidende matematikere avhenger av om mellomsetningene kan løftes inn i Mathlib og brukes andre steder. Anthropic har ikke sagt når, eller om, hele artefakten slippes til det formålet.
