Lean hyväksyi Clauden Fermat-todistuksen

Matemaatikkojen käyttämä todistustentarkistusohjelmisto Lean on hyväksynyt täydellisen formaalin version Fermat’n suuresta lauseesta. Anthropic-yhtiön Claude-järjestelmän tuottama ja avoimena tietovarastona julkaistu työ ei sisällä ratkaisemattomia välivaiheita, ylimääräisiä aksioomia eikä Leanin vakioperustan ulkopuolisia laskennallisia oikoteitä (repository). Imperial College Londonin matemaatikko Kevin Buzzard käänsi projektin itsenäisesti ja vahvisti tarkistuksen onnistuvan. Buzzard, joka johti omaa lauseen formalisointihankettaan, kutsui tulosta "poikkeukselliseksi autoformalisoinnin saavutukseksi" (Buzzard).

Matemaattinen kysymys ratkaistiin jo kauan sitten. Andrew Wiles todisti lauseen vuonna 1995, eikä tuloksen paikkansapitävyyttä ole vakavasti epäilty. Keskeneräistä oli todistuksen kirjoittaminen kirjaimellista tarkistusohjelmaa varten: jokainen määritelmä ja välivaihe piti ilmaista täsmällisesti, vaikka alkuperäinen todistus saattoi jättää ne lukijan pääteltäviksi. Anthropicin mukaan kymmenet tekoälyagentit tekivät työn elokuussa 11 päivässä. Agentit työskentelivät rinnakkain Prove2Me-alustalla (Anthropic).

Aikataulu kuvaa kuitenkin prosessia, jota ulkopuoliset eivät pysty toistamaan. Sisäistä mallia, agenttien koordinointijärjestelmää, operaattorien ratkaisuja ja laskentaresurssien käyttöä ei julkaistu. Lopputulos sen sijaan on toistettavissa: riittävällä laitteistolla kuka tahansa voi kääntää Lean-projektin ja tarkistaa todistuksen. Anthropicin Rust-kielellä kirjoittama erillinen tarkistin kävi läpi saman formaalin aineiston ja vahvisti kaikkien 1 052 234 määrittelyn olevan keskenään johdonmukaisia (technical report). Kyse on saman tekstin toisesta tarkistuksesta, ei 11 päivän työprosessin riippumattomasta toisinnosta.

Näin agentit työskentelivät

Todistuksen formalisoinnissa matemaatikon päättely kirjoitetaan muotoon, jossa vailla matemaattista intuitiota toimiva ohjelma pystyy tarkistamaan jokaisen loogisen askeleen. Fermat’n suuri lause on helppo esittää: kun kokonaislukueksponentti on vähintään kolme, yhtälöllä aⁿ + bⁿ = cⁿ ei ole ratkaisua, jossa a, b ja c ovat positiivisia kokonaislukuja. Todistus kulkee silti satojen sivujen ja useiden syvän lukuteorian kerrosten kautta.

Claude ei keksinyt uutta matematiikkaa. Se formalisoi Wilesin todistukseen johtavan tunnetun tulosketjun matemaatikkojen Henri Darmonin, Fred Diamondin ja Richard Taylorin esityksen pohjalta (Anthropic, technical report). Matemaattinen oivallus kuului Wilesille ja hänen edeltäjilleen. Clauden osuus oli muuntaa päättely noin 10,5 miljoonaksi riviksi koneellisesti tarkistettavaa koodia (technical report).

Anthropicin tutkijan Tianyi Pengin ja Columbia Universityn tutkijoiden kehittämä Prove2Me jakoi todistuksen riippuvuusverkoksi, johon kuului noin 29 511 itsenäistä väitettä (technical report). Agentit poimivat työjärjestyksessä valmiiksi tulleita väitteitä, kirjoittivat niille Lean-todistukset ja tarkistivat toistensa ehdottamia muotoiluja. Rinnakkainen työ kulutti sisäiseltä tutkimusmallilta arviolta kuusi miljardia tulostokenia (technical report).

Anthropicin mukaan ihmisoperaattorit eivät kirjoittaneet ajon aikana Lean-koodia. He kuitenkin valitsivat todistettavan lauseen, antoivat järjestelmälle tunnetun todistusreitin, rakensivat agentti-infrastruktuurin ja muuttivat ajoittain työn painotuksia (Anthropic). Operaattorien koko toimintalokia ja laskennan kustannuksia ei julkistettu.

Tulos rakentui vuosien ihmistyölle

Työ nojasi Mathlibiin, yhteisön ylläpitämään laajaan formalisoidun matematiikan kirjastoon, sekä kahteen aiempaan hankkeeseen. Buzzardin ryhmä oli rakentanut Imperialissa Fermat’n suuren lauseen Lean-formalisointia vuoden 2023 lopulta lähtien. Hanke sai miljoonan punnan EPSRC-rahoituksen, jonka oli määrä jatkua vuoteen 2029 (EPSRC award). Toinen yhteisöhanke oli jo formalisoinut lauseen osalle tapauksista. Anthropicin lähdetiedosto nimeää 106 tiedostoa, joissa on näistä hankkeista otettua tai niiden pohjalta muokattua aineistoa (attribution).

Rinnakkainen suoritus tekee 11 kalenteripäivän vertaamisen Buzzardin ryhmän henkilötyötunteihin harhaanjohtavaksi. Clauden työn alkaessa ryhmä oli käyttänyt hankkeeseen noin 22 rahoitettua kuukautta (EPSRC award). Anthropic ei kertonut grafiikkasuoritintuntien määrää eikä energiankulutusta.

Ennen julkaisua Fermat’n suuri lause oli viimeinen formalisoimaton kohta Freek Wiedijkin sadan tärkeän lauseen luettelossa. Kaksikymmentä vuotta käytössä ollut luettelo toimii formaalin matematiikan etenemisen vertailukohtana (Buzzard).

Menetelmän yleistettävyyttä mittaa paremmin tuoreen ja niukasti dokumentoidun matematiikan formalisointi, kun käytettävissä ei ole valmista etenemisreittiä, kypsiä kirjastoja eikä aiempaa formalisointityötä. Nyt kohteena oli kuuluisa lause, jonka ympärille oli jo rakennettu huomattava infrastruktuuri. Tulos osoittaa, että tekoälyagentit pystyvät tunnetun todistusreitin ja aiemman formalisointityön avulla tuottamaan täydellisen, Leanin hyväksymän ja ulkopuolisten tarkistettavissa olevan todistuksen. Julkaistu aineisto ei silti riitä itse tuotantoprosessin toistamiseen.