Anthropic julkaisi perjantaina ensimmäisen täydellisen, koneellisesti tarkistetun todistuksen Fermat'n suuresta lauseesta. Todistuksen kirjoitti Claude, joka työskenteli pääosin itsenäisesti 11 vuorokautta. Työn tuloksena syntyi 13 miljoonaa riviä Lean-kieltä ja 29 500 välilausetta.
Kyse ei ole uudesta matematiikasta. Andrew Wiles todisti lauseen jo vuonna 1995. Uutta on se, että todistus on nyt muodossa, jonka tietokone tarkistaa askel askeleelta. Tätä vaihetta kutsutaan formalisoinniksi, ja siihen oli varauduttu vuosilla.
Kolme ja puoli vuosisataa avointa ongelmaa
Pierre de Fermat kirjoitti väitteensä noin vuonna 1637 Diofantoksen Arithmetican marginaaliin. Yhtälölle a^n + b^n = c^n ei löydy positiivisia kokonaislukuratkaisuja, kun n on suurempi kuin kaksi. Fermat lisäsi reunaan huomautuksen, jonka mukaan hänellä oli todistus, mutta marginaali oli sille liian kapea.
Väite osoittautui poikkeuksellisen sitkeäksi. Vuonna 1908 oikeasta todistuksesta luvattiin 100 000 kultamarkan palkinto, joka vastaa nykyrahassa miljoonaa tai kahta dollaria. Pelkästään ensimmäisen vuoden aikana palkintoa tavoiteltiin 621 virheellisellä yrityksellä.
Wiles esitteli oman todistuksensa kolmen päivän luentosarjassa kesäkuussa 1993. Kaksi kuukautta myöhemmin tarkastaja löysi siitä kriittisen aukon. Wiles korjasi sen vuoden työn jälkeen yhdessä entisen oppilaansa Richard Taylorin kanssa, ja lopullinen 129-sivuinen todistus julkaistiin toukokuussa 1995.
Elementaarista todistusta ei ole löytynyt vuosisatojen etsinnästä huolimatta. Matemaatikkojen enemmistö pitää siksi todennäköisenä, että Fermat'n oma marginaaliin viittaama todistus oli virheellinen.
Kymmeniä agentteja ja kuusi miljardia tokenia
Kokeen käynnisti Anthropicin tutkija Tianyi Peng, jonka ryhmä Columbian yliopistossa rakentaa työkaluja tekoälyavusteiseen formalisointiin. Tavoitteena oli selvittää, pääseekö Claude edes alkuun. Tulos ylitti odotukset selvästi.
Työtä teki kymmeniä rinnakkaisia Claude-agentteja. Ne määrittelivät käsitteitä, todistivat välituloksia ja käyttivät niitä yhä vaativampien väitteiden todistamiseen. Agentit tuottivat kaikkiaan 30 300 konetarkistettavaa lausetta, joista 29 500 päätyi lopulliseen todistukseen.
Kokoluokka on poikkeuksellinen. Clauden tuottama 13 miljoonan rivin todistus on yli viisi kertaa laajempi kuin Mathlib, matemaattisten todistusten keskeinen yhteisökirjasto, jonka päälle koko työ rakentuu.
Ensimmäiset yritykset epäonnistuivat. Agentit pääsivät liikkeelle, mutta menettivät pian otteen projektin tilasta eivätkä enää tehneet yhteistyötä. Näistä hylätyistä yrityksistä jäi jäljelle noin seitsemän prosenttia lopullisen todistuksen varsinaisista riveistä.
Ratkaisu löytyi Prove2Me-alustasta, jonka Peng ja hänen kollegansa ovat kehittäneet. Alusta ylläpitää suunnattua syklitöntä verkkoa lauseiden välillä, jolloin agentit näkevät mitä kannattaa todistaa seuraavaksi. Claude Codeen pohjautuva moniagenttiratkaisu kulutti noin kuusi miljardia ulostulotokenia sisäisellä tutkimusmallilla, joka vastaa suunnilleen Claude Fable 5.1:tä.
Tarkistaminen on eri asia kuin keksiminen
Aiemmat tekoälyn matemaattiset saavutukset, kuten työ Riemannin hypoteesin parissa, tuottivat uutta matematiikkaa. Tässä uutta on nimenomaan varmistaminen. Todistus tarkistetaan kuin laskutoimitus, koneellisesti ja ilman tulkinnanvaraa.
Ero on käytännössä suuri. Todistus on ketju loogisia askelia, ja yksikin katkennut lenkki voi kaataa kaiken sen jälkeen tulevan. Uuden tuloksen ymmärtäminen niin hyvin, että sen oikeellisuuteen uskaltaa luottaa, vie usein kuukausia.
Lean-todistusavustin vaatii jokaisen askeleen kirjoitettuna auki, olipa se kuinka ilmeinen tahansa. Ihmiselle kirjoitettu todistus hyppää itsestäänselvyyksien yli ja nojaa vuosisatojen julkaistuun kirjallisuuteen. Formalisointi taas lähtee liikkeelle siitä pienestä osasta matematiikkaa, joka on jo ehditty formalisoida.
Lopputulos läpäisi tarkistuksen. Todistus nojaa vain Leanin kolmeen vakioaksioomaan, ja erillinen vertailuohjelma varmisti, että todistettu väite vastaa Mathlib-kirjaston omaa muotoilua Fermat'n suuresta lauseesta. Ihmisen panos rajoittui satunnaisiin ylätason ohjeisiin, kuten kehotukseen priorisoida tietty osatulos.
Seuraukset matematiikan arkeen
Anthropic näytti todistuksen Kevin Buzzardille, joka johtaa Imperial College Londonissa vuonna 2024 käynnistettyä yhteisöhanketta Fermat'n lauseen formalisoimiseksi. Buzzardin mukaan todistus nojaa pelkkiin matematiikan aksioomiin eikä oleta mitään muuta. Hän piti merkittävänä myös sitä, että koneellisesti tuotetut formalisoinnit ovat nyt riittävän kestäviä, jotta niiden päälle voi rakentaa.
Buzzard arvioi, että jos Fermat'n lauseen automaattinen formalisointi onnistuu nyt, askel modernin matemaattisen kirjallisuuden automaattiseen formalisointiin on lyhyt. Tällaiset menetelmät voisivat paljastaa virheitä nykyisestä tutkimusaineistosta ja keventää vertaisarvioijien taakkaa.
Mittakaavaa kuvaa se, että yhteisön käyttämä suunnitelma pelkälle hankkeen alkuvaiheelle on 86 sivua pitkä. Anthropic teki myös pienemmän kokeen kolmella tavallisella Claude Max -tilauksella. Agentit formalisoivat Vinogradovin kolmen alkuluvun lauseen kolmessa päivässä tehden yhteistyötä pelkästään Prove2Men kautta.
Yhteenveto
Fermat'n suuri lause on nyt ensimmäistä kertaa kokonaan koneellisesti tarkistettu. Anthropicin mukaan Claude kirjoitti todistuksen 11 päivässä, kun ihmisyhteisö oli varautunut vuosien urakkaan. Merkittävintä ei ole uusi tulos vaan nopeus, jolla vanha tulos saatiin koneen tarkistettavaan muotoon.
Jos sama onnistuu laajemmin, matematiikan julkaisukäytännöt voivat muuttua. Virheiden löytäminen ei enää riippuisi yksin siitä, kuinka monta tuntia arvioija ehtii käyttää. Toistaiseksi kyse on kuitenkin yhdestä hankkeesta, jonka toistettavuus muissa ongelmissa on vielä osoittamatta.