A nejem a mai napig rosszallóan emlegeti, hogy egyszer, egy hajnali órán berontottam a hálószobába, és lelkesülten kiabáltam: megvan, megtalálták a Higgs-bozont! Ma reggel már óvatosabb voltam, megvártam, amíg felébred, és akkor osztottam meg vele azt az információt, hogy a nagy Fermat-tételt AI-ügynökök matematikailag ellenőrizhető módon vezették le, és bizonyították, ráadásul mindezt 11 nap alatt. (Nem mellesleg, lövésem sincs a matekhoz, csak csodálom…)
Forrás: Anthropic Egy mesterségesintelligencia-ügynökökből álló rendszer 11 nap alatt készítette el Fermat utolsó tételének teljes, számítógéppel ellenőrizhető formalizálását. A Claude több tízmillió sor kódot és csaknem harmincezer köztes bizonyítást állított elő – miközben egy hasonló emberi projektet eredetileg évekre terveztek.
A matematika történetének egyik leghíresebb problémáját nem fedezték fel újra, hanem a számítógép számára is minden részletében ellenőrizhetővé tették. Az Anthropic szeptember 4-én jelentette be, hogy Claude mesterségesintelligencia-rendszere 11 nap alatt elkészítette Fermat utolsó tételének első teljes, géppel ellenőrzött formalizálását.
A teljesítmény azért különösen figyelemre méltó, mert a projekt során az AI 13 millió sor Lean kódot írt, és mintegy 30 300 matematikai tételt bizonyított számítógéppel, amelyek közül 29 500 került be a végső bizonyításba. A kész bizonyítás több mint ötször akkora, mint a matematikai bizonyítások egyik legfontosabb közösségi könyvtára, a Mathlib.
Mi Fermat utolsó tétele?
Fermat utolsó tétele első pillantásra szinte gyermekien egyszerűnek tűnik. Azt állítja, hogy ha n nagyobb 2-nél, akkor nincs három olyan pozitív egész szám, amelyekre igaz lenne: aⁿ + bⁿ = cⁿ
A legegyszerűbb esetben, amikor n = 2, természetesen vannak megoldások. Ilyen például a jól ismert 3² + 4² = 5², vagyis 9 + 16 = 25. Ezek a pitagoraszi számhármasok. Fermat azt állította, hogy amint a kitevőt 2-ről 3-ra vagy annál nagyobbra emeljük, a dolog lehetetlenné válik: nincs olyan nem nulla egész számokból álló a, b és c hármas, amely kielégíti az egyenletet.
Ez nem azt jelenti, hogy néhány számmal nem sikerül megoldást találni. A tétel ennél sokkal erősebb: azt mondja, hogy semmilyen számmal nem létezik ilyen megoldás, bármilyen nagy számokat is próbálunk.
Egy 350 éves matematikai rejtély
A tétel névadója, a francia matematikus Pierre de Fermat 1637 körül egy ókori matematikai mű, Diophantosz Arithmetikája egyik példánya széljegyzetében írta le az állítást. Azt is megjegyezte, hogy talált rá egy „csodálatos bizonyítást”, amely azonban nem fért el a könyv margóján. A bizonyítást soha nem találta meg senki.
A matematikusok évszázadokon keresztül próbálták megfejteni Fermat állítását. A probléma végül a modern számelmélet egyik legfontosabb hajtóerejévé vált. A megoldásra egészen 1994-ig kellett várni.
Andrew Wiles és a bizonyítás, amely majdnem összeomlott
A brit matematikus Andrew Wiles 1993-ban jelentette be, hogy bizonyította Fermat utolsó tételét. A bizonyítás azonban az ellenőrzés során komoly hibába ütközött: a matematikusok egy olyan rést találtak benne, amelyet nem lehetett egyszerűen áthidalni. Wiles több mint egy évig dolgozott a probléma megoldásán, végül Richard Taylor közreműködésével sikerült kijavítaniuk a bizonyítást. A teljes, helyes bizonyítás 1995-ben jelent meg.
Itt válik igazán érdekessé az AI mostani teljesítménye. A Claude nem fedezte fel újra Fermat tételét, és nem talált új bizonyítást. Wiles bizonyítása évtizedek óta elfogadott a matematikai közösségben. A gép azt csinálta, ami bizonyos szempontból még nehezebb: Wiles bizonyítását és az ahhoz szükséges teljes matematikai apparátust olyan precíz formába öntötte, amelyet egy számítógép minden egyes logikai lépésében ellenőrizni tud.
Mit jelent az, hogy „formalizálta” a bizonyítást?
A matematikusok számára egy bizonyítás lehet több száz oldalas, és bizonyos lépéseket természetesnek vesznek. Egy emberi szakértő elolvassa például azt, hogy egy következtetés „triviális”, és többnyire érti, miért következik az előző lépésekből.
Egy számítógép azonban nem működik így. A formalizált bizonyításban minden szükséges logikai lépést olyan formában kell megadni, amelyet egy úgynevezett bizonyításellenőrző rendszer képes mechanikusan ellenőrizni.
Az Anthropic ehhez a Lean nevű formális matematikai rendszert használta. A Lean nem egyszerűen „elhiszi”, amit az AI állít. Ellenőrzi, hogy a megadott bizonyítás valóban következik-e a megengedett matematikai axiómákból és korábban bizonyított állításokból.
Ez lényeges különbség a hagyományos chatbotokhoz képest. Egy nyelvi modell képes meggyőzőnek tűnő, ám hibás matematikai magyarázatot is generálni. Egy formális bizonyításnál viszont a végső ellenőrzést nem a nyelvi modell végzi. A gépnek bizonyítania kell, hogy igaza van.
Nem egyetlen AI dolgozott rajta
A projekt egyik legérdekesebb része éppen az, hogy nem egyetlen Claude „ült le” Fermat problémája elé.
Több tucat AI-ügynök dolgozott párhuzamosan: egyesek fogalmakat definiáltak, mások résztételeket bizonyítottak, megint mások a már elkészült eredményeket használták fel újabb, nehezebb állítások bizonyítására.
A fordulópontot egy közös, irányított gráf, úgynevezett DAG (directed acyclic graph) alkalmazása jelentette. Ez lényegében közös memóriaként szolgált: nyilvántartotta, milyen tételeket kell még bizonyítani, melyek készültek el, és hogyan kapcsolódnak egymáshoz az egyes matematikai eredmények. A rendszert a Columbia Egyetem kutatóival együttműködésben fejlesztett Prove2Me platform segítette.
Tizenegy nap kontra öt év
A teljesítmény különösen azért látványos, mert a matematikai közösség már korábban megkezdte Fermat bizonyításának formalizálását.
Kevin Buzzard, az Imperial College London matematikusa 2024-ben többéves közösségi projektet indított azzal a céllal, hogy Wiles bizonyítását Leanben teljes egészében formalizálják. A munkát ötéves, 1 millió fontos brit kutatási támogatás is segítette. Ehhez képest Claude 11 nap alatt jutott el a teljes, géppel ellenőrzött bizonyításig.
A különbség azonban nem egyszerűen az, hogy „AI gyorsabb, mint az ember”. Az emberi kutatók munkája közben ugyanis maga a formalizálás módszertana és a szükséges matematikai infrastruktúra is épült. Claude már egy jelentős részben előkészített matematikai ökoszisztémára támaszkodhatott.
Nem a matematika végét, hanem egy új korszak kezdetét jelentheti
A Fermat-projekt legfontosabb következménye ezért nem az, hogy egy AI „legyőzte” a matematikusokat. A valódi jelentősége az lehet, hogy megváltozik a matematikai eredmények ellenőrzésének sebessége. Egy új, rendkívül bonyolult matematikai bizonyítás szakértői ellenőrzése hónapokig vagy akár évekig tarthat. A formalizálás során viszont a számítógép végső soron nem azt vizsgálja, hogy a bizonyítás szerzője mennyire tekintélyes matematikus, hanem azt, hogy minden egyes következtetés logikailag helyes-e.
Az Anthropic szerint a cél éppen ezért egy olyan jövő, amelyben a matematikai eredmények sokkal könnyebben és gyorsabban ellenőrizhetők. Ez különösen fontos lehet a matematikán túl is. Ha az AI képes bonyolult tudományos érveléseket formalizálni, akkor idővel más tudományterületeken is megjelenhetnek hasonló rendszerek. A nagy kérdés az, hogy képes lesz-e a tudomány egyre nagyobb részét olyan formába önteni, amelyet a gépek folyamatosan, automatikusan és megbízhatóan ellenőrizhetnek.
Fermat több mint három évszázadon át várt a bizonyítására. Wilesnek évek kellettek hozzá. Az AI-nak pedig most 11 napra volt szüksége ahhoz, hogy ugyanezt a bizonyítást a számítógép számára minden részletében ellenőrizhetővé tegye. A matematika ettől még nem lett egyszerűbb. Csak a bizonyítására állt be egy újfajta „digitális kutatócsapat”.
A cikk az AI segítségével készült
