Anthropic sier Claude har skrevet det første datamaskinkontrollerte beviset for Fermats siste teorem

Anthropic kunngjorde torsdag at deres AI-modell Claude har fullført det første ende-til-ende, datamaskinkontrollerte beviset for Fermats siste teorem, et av de mest berømte resultatene i matematikken. Ved å jobbe i stor grad autonomt over 11 dager, skrev Claude beviset i programmeringsspråket Lean, noe som resulterte i 13 millioner linjer med kode og 29 500 mellomliggende teoremer.anthropic+1

En 11 dagers spurt gjennom århundrer med matematikk

Fermats siste teorem sier at ingen positive heltall a, b og c tilfredsstiller ligningen aⁿ + bⁿ = cⁿ for noe heltall n større enn 2. Det ble først foreslått av Pierre de Fermat rundt 1637, og ble ikke bevist før i 1995, da Andrew Wiles publiserte et 129 siders bevis som krevde måneder med ekspertvurdering for å verifisere.anthropic

Å formalisere dette beviset, altså skrive det om slik at en datamaskin kan sjekke hvert logiske steg, var forventet å ta år. Kevin Buzzard, en matematiker ved Imperial College London som har ledet et uavhengig arbeid for å formalisere FLT ved bruk av Lean, bekreftet at koden kompilerer og er korrekt. I et blogginnlegg på fredag kalte Buzzard det en ekstraordinær prestasjon innen autoformalisering og bemerket at beviset er flerlags, og spenner over algebra, harmonisk analyse, geometri og tallteori.xenaproject.wordpress+1

Claudes bevis følger Darmon-Diamond-Taylor-fremstillingen av Wiles-Taylor-Wiles-argumentet, en forenklet versjon av det opprinnelige beviset. Menneskelig input var begrenset til sporadiske instruksjoner på høyt nivå fra Anthropic-forsker Tianyi Peng, hvis team ved Columbia University bygde Prove2Me-plattformen som muliggjorde arbeidet.anthropic+1

Hvordan beviset ble bygget

Flere tidlige forsøk mislyktes da Claudes agenter mistet oversikten over prosjektets tilstand og sluttet å samarbeide effektivt. Gjennombruddet kom da teamet byttet til Prove2Me, en åpen samarbeidsplattform som opprettholder en rettet graf av teoremutsagn, noe som tillater flere agenter å jobbe parallelt og bestemme hvilke bevis som skal forsøkes neste gang. Ved bruk av et Claude Code-basert multi-agent-system, konsumerte dusinvis av agenter omtrent seks milliarder utdatatokens fra en intern forskningsmodell som Anthropic beskriver som omtrent sammenlignbar med Claude Fable 5.1.siliconangle+1

Det ferdige beviset ble verifisert av Lean ved bruk av kun de tre standardaksiomene, og en komparator bekreftet at teoremutsagnet samsvarer med Mathlibs egen formulering av FLT. Med 13 millioner linjer er det over fem ganger så stort som Mathlib, det viktigste fellesskapsbiblioteket for formalisert matematikk.anthropic+1

Hva det betyr for matematikken

Buzzard, som opprinnelig fikk e-post om resultatet mens han var på en musikkfestival og avfeide avsenderen som en tulling, skrev at prestasjonen signaliserer en ny æra: Hvis automatisk formalisering av FLT er mulig nå, har vi tatt et stort skritt mot automatisk formalisering av moderne matematisk litteratur. Han bemerket at slike teknikker kan luke ut feil i den eksisterende matematiske korpusen og lette arbeidsbyrden for fagfeller som vurderer nytt arbeid.anthropic+1

Milepælen følger en rekke AI-drevne fremskritt innen matematikk. Anthropic brukte Claude forrige måned til å oppdage ny informasjon om Riemanns zeta-funksjon, mens rivalen OpenAI brukte sin nyeste modell til å løse flere Erdős-problemer. Anthropic brukte også nylig Claude til å motbevise Jacobian-formodningen i tre dimensjoner og oppover. Buzzard, på sin side, kom med en karakteristisk tørr kommentar: Jeg fikk 1 million pund for å drive prosjektet mitt over 5 år; Anthropic brukte bare 11 dager, men jeg lurer på om de brukte mer penger.xenaproject.wordpress+2