Kevin Buzzard on käyttänyt vuosia siihen, että Fermat'n suuri lause saataisiin muotoon, jonka tietokone pystyy tarkistamaan rivi riviltä. Syyskuun 4. päivä Imperial College Londonin matematiikan professori julkaisi blogiinsa merkinnän otsikolla ”FLT: Anthropic has beaten me to it”. Joku ehti ensin.
Anthropic kertoi samana päivänä, että sen sisäinen tutkimusmalli oli tuottanut täydellisen, Lean-järjestelmällä tarkistetun todistuksen Fermat'n suuresta lauseesta. Yhtiön ilmoittamat luvut ovat isoja: 11 päivää, noin 13 miljoonaa riviä koodia, 29 500 lopulliseen todistukseen päätynyttä välilausetta ja noin kuusi miljardia tokenia. Malli on Anthropicin mukaan suunnilleen Claude Fable 5.1:n tasoinen.
Otsikkoa kannattaa silti lukea varovasti. Uutta matematiikkaa ei syntynyt.
Mikä Fermat'n suuri lause on
Ranskalainen Pierre de Fermat raapusti vuonna 1637 kirjansa marginaaliin väitteen, ettei yhtälöllä xⁿ + yⁿ = zⁿ ole positiivisia kokonaislukuratkaisuja, kun n on suurempi kuin kaksi. Todistus ei mahtunut marginaaliin, kuten hän itse huomautti. Seuraavat 358 vuotta matemaatikot etsivät sitä.
Andrew Wiles esitti todistuksen vuonna 1993 ja paikkasi siitä löytyneen aukon Richard Taylorin kanssa 1995. Sitä ei ole sen jälkeen vakavasti kyseenalaistettu. Anthropicin malli seurasi Darmonin, Diamondin ja Taylorin samana vuonna julkaisemaa esitystä, ei sitä uudempaa lähestymistapaa, jota Buzzard on omassa hankkeessaan formalisoinut.
Mitä koneellisesti tarkistettu todistus tarkoittaa
Lean on todistusavustin: ohjelmointikieli, jossa matemaattinen päättely kirjoitetaan niin pieninä askelina, että kone pystyy tarkistamaan jokaisen niistä logiikan perusaksioomia vasten. Ihmisen kirjoittama todistus vetoaa lukijan ymmärrykseen. Lean-todistus ei vetoa mihinkään.
Käytännössä tämä tarkoittaa, että jos koodi kääntyy, todistus pitää. Anthropicin mukaan lopputulos nojaa vain Leanin kolmeen vakioaksioomaan, ja erillinen vertailuohjelma varmisti, että todistettu väite on sama kuin Leanin Mathlib-kirjaston oma muotoilu Fermat'n lauseesta. Työ tehtiin Prove2Me-alustalla, jonka on kehittänyt Anthropicin tutkija Tianyi Peng kollegoineen Columbian yliopistossa.
“Huomatkaa, että matemaattisesti tämä Anthropicin työ ei kerro meille käytännössä mitään: olen sanonut julkisesti olevani 99,9-prosenttisen varma siitä, että Fermat'n lauseen todistus on kunnossa.”
Yksi arvioija, ei riippumatonta toistoa
Buzzard ei ole tässä pelkkä sivustakatsoja. Hän kertoo kääntäneensä koodikannan itse ja ajaneensa sille vertailuohjelman: ”se menee läpi”. Se on selvästi enemmän kuin kohtelias kommentti tiedotteeseen. Silti hän on ainoa nimetty ulkopuolinen arvioija, eikä kukaan ole toistanut itse ajoa riippumattomasti.
Väite tulee siis tekoäly-yhtiöltä itseltään, ja sen tueksi on yksi ulkopuolinen tarkistus. Anthropic myöntää myös, että todistus on todennäköisesti pidempi kuin sen tarvitsisi olla ja että noin seitsemän prosenttia riveistä on peräisin epäonnistuneista yrityksistä. Buzzardin mukaan koodikannan kääntäminen kestää lähes kaksikymmenkertaisesti sen ajan, jonka Leanin koko matematiikkakirjasto vaatii.
Miksi tällä on väliä muillekin kuin matemaatikoille
Kiinnostavinta ei ole lause vaan menetelmä. Kun tekoälymalli tuottaa tuhansia sivuja tekstiä tai koodia, jota kukaan ihminen ei ehdi lukea läpi, koneellinen tarkistus on ainoa tapa luottaa siihen ilman uskonvaraisuutta. Sama koskee ohjelmistoja: formaalia verifiointia käytetään jo lentokoneiden ohjausjärjestelmissä ja sirusuunnittelussa, mutta sen hinta on rajannut käytön pieniin, kriittisiin osiin.
Anthropicin luvut kertovat myös hinnasta. Kuusi miljardia tokenia paloi asiaan, joka on tiedetty vuodesta 1995.
