Lean elfogadta Claude 10.5 millió soros Fermat-bizonyítását

A matematikusok világszerte használt bizonyításellenőrző szoftvere, a Lean elfogadta Fermat utolsó tételének teljes formális bizonyítását. Az Anthropic Claude rendszere által készített és nyilvános repozitóriumban közzétett változatban nincsenek kidolgozatlan lépések, új axiómák vagy a Lean szabványos alapjain túlmutató számítási kerülőutak (repository). Kevin Buzzard, az Imperial College London matematikusa, aki saját csapatával ugyanezen a feladaton dolgozott, külön is lefordította a projektet, és megerősítette, hogy a Lean elfogadja. Az eredményt „rendkívüli autoformalizációs teljesítménynek” nevezte (Buzzard).

Maga a matematikai kérdés már régen eldőlt: Andrew Wiles 1995-ben bizonyította a tételt, amelynek helyességét azóta sem vitatták komolyan. A formális bizonyítás azonban más feladat. Wiles érvelését egy szó szerint értelmező ellenőrzőprogram utasításaivá kellett átírni, minden definícióval és köztes lépéssel együtt, amelyet egy matematikus magától értetődőnek vehet. Az Anthropic szerint augusztusban több tucat mesterségesintelligencia-ügynök tizenegy nap alatt végezte el ezt a munkát, párhuzamosan dolgozva a Prove2Me nevű platformon (Anthropic).

A tizenegy napos folyamatot ugyanakkor kívülállók nem tudják megismételni. A nyilvános csomag nem tartalmazza a belső modellt, az ügynököket összehangoló infrastruktúrát, az operátorok döntéseit és a felhasznált számítási kapacitás adatait. A végeredmény viszont ellenőrizhető: megfelelő hardverrel bárki újrafordíthatja a Lean-projektet, és meggyőződhet arról, hogy a bizonyítás átmegy az ellenőrzésen. Az Anthropic külön, Rust nyelven írt ellenőrzője ugyanerre jutott mind az 1 052 234 deklaráció esetében (technical report). Ez ugyanannak a formális szövegnek egy második ellenőrzése, nem pedig a tizenegy napos munka független megismétlése.

Hogyan dolgoztak az ügynökök

Egy bizonyítás formalizálásakor a matematikus érvelését úgy írják át, hogy annak minden logikai lépését egy matematikai intuíció nélküli program is igazolni tudja. Fermat utolsó tétele könnyen megfogalmazható: három vagy annál nagyobb egész kitevő esetén nincs három pozitív egész szám, amelyre aⁿ + bⁿ = cⁿ teljesül. A bizonyítás azonban a számelmélet több mély területén vezet keresztül, és több száz oldalnyi matematikára támaszkodik.

A Claude nem fedezett fel új matematikai összefüggést. A Wiles bizonyításához vezető, már ismert eredménysort formalizálta Henri Darmon, Fred Diamond és Richard Taylor matematikusok kifejtése alapján (Anthropic, technical report). Az alkotó matematikai felismerések Wileshoz és elődeihez kötődnek; a Claude mintegy 10,5 millió sornyi, géppel ellenőrizhető kóddá alakította át ezeket (technical report).

Az Anthropic kutatója, Tianyi Peng és a Columbia University munkatársai által fejlesztett Prove2Me nagyjából 29 511 önálló állításból felépülő függőségi gráfra bontotta a bizonyítást (technical report). Az ügynökök kiválasztották azokat az állításokat, amelyek előfeltételei már rendelkezésre álltak, megírták hozzájuk a Lean-bizonyításokat, majd egymás megfogalmazásait is ellenőrizték. A párhuzamos munka során egy belső kutatási modell mintegy hatmilliárd kimeneti tokent állított elő (technical report).

Az Anthropic közlése szerint a futtatás alatt az emberi operátorok nem írtak Lean-kódot. Ők választották ki a tételt és az ismert bizonyítási útvonalat, megtervezték az ügynöki infrastruktúrát, valamint időnként módosították a feladatok sorrendjét (Anthropic). A vállalat sem az operátori munka teljes naplóját, sem a felhasznált számítási kapacitás költségét nem hozta nyilvánosságra.

Több évnyi emberi munkára épült

Az eredményhez szükség volt a Mathlibre, a közösség által fenntartott, formalizált matematikai könyvtárra, továbbá két korábbi projekt eredményeire. Buzzard csapata 2023 vége óta dolgozott Fermat utolsó tételének Lean-formalizálásán az Imperial College-ban, egy 2029-ig tervezett, 1 millió fontos EPSRC-támogatással (EPSRC award). Egy másik közösségi projekt korábban már formalizálta a tételt az esetek egy részére. Az Anthropic forrásmegjelölési dokumentuma 106 olyan fájlt sorol fel, amely e két kezdeményezésből átvett vagy azok alapján módosított anyagot tartalmaz (attribution).

A párhuzamos végrehajtás miatt a tizenegy napos átfutási idő közvetlenül nem vethető össze a Buzzard-csapat munkájával: mire a Claude futtatása elkezdődött, a kutatók már körülbelül 22 támogatott hónapot fordítottak a projektre (EPSRC award). Az Anthropic nem közölte sem a felhasznált GPU-órák számát, sem az energiaigényt.

A mostani eredmény előtt Fermat utolsó tétele volt az utolsó formalizálásra váró tétel Freek Wiedijk száz fontos matematikai tételt tartalmazó listáján. A két évtizede használt lista a formális matematika fejlődésének egyik viszonyítási pontja (Buzzard).

A módszer általánosíthatóságát olyan újabb, kevésbé részletesen dokumentált matematikai eredmények formalizálása mutathatná meg, amelyekhez nincs kész bizonyítási útvonal, kiforrott könyvtári háttér vagy korábbi formális munka. Ebben az esetben egy híres, már alaposan feldolgozott tételhez jelentős infrastruktúra állt rendelkezésre. Az eredmény azt bizonyítja, hogy az MI-ügynökök ismert bizonyítási útvonalra és korábbi formalizációkra támaszkodva képesek teljes, a Lean által elfogadott és kívülállók által is ellenőrizhető bizonyítást készíteni. A létrehozás tizenegy napos folyamatát azonban a közzétett anyagok alapján nem lehet reprodukálni.