Anthropic: Claude-líkan sannaði síðustu setningu Fermats með tölvuaðstoð

Anthropic tilkynnti á fimmtudag að gervigreindarlíkanið Claude hafi lokið fyrstu tölvustaðfestu sönnuninni á síðustu setningu Fermats, einni frægustu niðurstöðu stærðfræðinnar. Claude vann að mestu sjálfstætt í 11 daga og skrifaði sönnunina í Lean-forritunarmálinu, þar sem það framleiddi 13 milljónir línur af kóða og sannaði 29.500 millistigasetningar á leiðinni.anthropic+1

11 daga sprettur í gegnum aldir stærðfræðinnar

Síðasta setning Fermats segir að engar jákvæðar heiltölur a, b og c uppfylli jöfnuna aⁿ + bⁿ = cⁿ fyrir neina heiltölu n stærri en 2. Pierre de Fermat setti fram tilgátuna um 1637, en hún var ekki sönnuð fyrr en 1995 þegar Andrew Wiles birti 129 blaðsíðna sönnun sem tók sérfræðinga mánuði að yfirfara.anthropic

Gert var ráð fyrir að formfesting þeirrar sönnunar, það er að endurskrifa hana svo tölva geti yfirfarið hvert rökrétt skref, tæki mörg ár. Kevin Buzzard, stærðfræðingur við Imperial College London sem hefur leitt sjálfstætt verkefni við að formfesta setninguna með Lean, staðfesti að kóðinn keyri og sé réttur. Í bloggfærslu á föstudag kallaði Buzzard þetta "ótrúlegt afrek í sjálfvirkri formfestingu" og benti á að sönnunin væri marglaga og spannaði algebru, harmoníska greiningu, rúmfræði og talnafræði.xenaproject.wordpress+1

Sönnun Claude fylgir Darmon-Diamond-Taylor útskýringunni á Wiles-Taylor-Wiles röksemdafærslunni, sem er einfölduð útgáfa af upprunalegu sönnuninni. Mannleg íhlutun takmarkaðist við einstaka leiðbeiningar frá Tianyi Peng, rannsakanda hjá Anthropic, en teymi hans við Columbia-háskóla smíðaði Prove2Me-vettvanginn sem gerði verkefnið mögulegt.anthropic+1

Hvernig sönnunin var byggð

Nokkrar fyrstu tilraunir mistókust þar sem umboðsmenn Claude misstu sjónar á stöðu verkefnisins og hættu að vinna saman á áhrifaríkan hátt. Vendipunkturinn kom þegar teymið skipti yfir í Prove2Me, opinn samvinnuvettvang sem heldur utan um stýrðan graf af setningum, sem gerir mörgum umboðsmönnum kleift að vinna samhliða og ákveða hvaða sannanir eigi að reyna næst. Með því að nota Claude Code-undirstaða fjölumboðskerfi unnu tugir umboðsmanna úr um sex milljörðum úttakstákna frá innra rannsóknarlíkani sem Anthropic lýsir sem sambærilegu við Claude Fable 5.1.siliconangle+1

Fullgerð sönnun var staðfest af Lean með því að nota aðeins þrjár staðlaðar frumsendur þess, og samanburðartæki staðfesti að setningin passi við eigin formfestingu Mathlib á síðustu setningu Fermats. Með 13 milljónum lína er hún yfir fimm sinnum stærri en Mathlib, helsta safn samfélagsins fyrir formfesta stærðfræði.anthropic+1

Hvað þetta þýðir fyrir stærðfræði

Buzzard, sem fékk tölvupóst um niðurstöðuna á tónlistarhátíð og taldi sendandann vera rugludall, skrifaði að afrekið boði nýja tíma: "Ef sjálfvirk formfesting á síðustu setningu Fermats er möguleg núna, þá höfum við tekið stórt skref í átt að sjálfvirkri formfestingu nútíma stærðfræðirita". Hann benti á að slík tækni gæti upprætt villur í núverandi stærðfræðiritum og létt álagi á ritrýna sem fara yfir ný verk.anthropic+1

Þessi áfangi fylgir röð framfara í stærðfræði sem knúnar eru áfram af gervigreind. Anthropic notaði Claude í síðasta mánuði til að uppgötva nýjar upplýsingar um Riemann-zeta fallið, á meðan keppinauturinn OpenAI notaði nýjasta líkan sitt til að leysa nokkur Erdős-vandamál. Anthropic notaði einnig Claude nýlega til að hrekja Jacobian-tilgátuna í þremur víddum og fleiri. Buzzard tók á málinu á sinn dæmigerða þurra hátt: "Ég fékk eina milljón punda til að reka verkefnið mitt í 5 ár; Anthropic tók aðeins 11 daga en ég velti því fyrir mér hvort þeir hafi eytt meiri peningum".xenaproject.wordpress+2