EnglishDuizend Claude-agents reproduceren formeel bewijs van Fermats laatste stelling
Duizend AI-agents met een vroege versie van Claude Fable 5.2 zetten het bewijs van Fermats laatste stelling in 28,7 uur om in code die een computer kan controleren. Volgens Anthropic ging het sneller en zuiniger dan in september, met meer voorbereid werk als start.
Anthropic heeft na de introductie van Claude Fable 5.2 en Mythos 5.2 beschreven hoe duizend AI-agents met een vroege versie van Fable 5.2 een formeel bewijs van Fermats laatste stelling opnieuw opbouwden. Volgens het bedrijf duurde dat 28,7 uur, zonder dat een onderzoeker het werk inhoudelijk stuurde.
Fermats laatste stelling zegt dat er geen positieve hele getallen a, b en c bestaan waarvoor a tot de macht n plus b tot de macht n gelijk is aan c tot de macht n, als n groter is dan 2. Pierre de Fermat schreef het rond 1637 in de kantlijn van een boek. Pas in 1995 kwam Andrew Wiles met een bewijs van 129 pagina's.
Het gaat hier dus niet om een nieuw bewijs. De agents zetten het bestaande bewijs om in Lean, een programmeertaal waarin een computer elke stap van een wiskundig bewijs kan nalopen. Zo'n formeel bewijs laat geen ruimte voor een vergeten tussenstap.
Sneller dan in september
Anthropic maakte in september al zo'n formele versie. Daar werkten tientallen agents met een intern onderzoeksmodel aan, vergelijkbaar met Claude Fable 5.1, samen met het wiskundeplatform Prove2Me en af en toe aanwijzingen van onderzoeker Tianyi Peng. Dat duurde elf dagen en leverde dertien miljoen regels Lean-code op. Wiskundige Kevin Buzzard beoordeelde dat bewijs.
Volgens Anthropic schreven de agents deze keer een derde van de hoeveelheid tekst van september, en is het bewijs een zevende zo lang. De start was wel anders: de agents kregen zestig uitspraken om te bewijzen (de stelling zelf en 59 tussenstappen), de bijbehorende definities, een beschrijving van de klassieke route in één zin en 47 hulpstellingen die in september al waren bewezen. Over de aanpak of de taakverdeling kregen ze geen aanwijzingen.
Hoe duizend agents samenwerkten
Eén leidende agent verdeelde het werk over 999 helpers. Elke agent werkte in een eigen afgeschermde computer zonder internet. Ze deelden hun code via versiebeheer en een gezamenlijke database, waarin de leider vijf lijsten aanmaakte: mededelingen, wie waaraan werkt, notities, openstaande taken en afgerond werk.
Het lastigste deel werd opgesplitst in 2.418 taken, tot tien niveaus diep. Rond het achttiende uur viel de activiteit stil. De onderzoekers startten de ronde opnieuw vanaf de laatste opslag en gaven de agents twaalf uur extra. Uiteindelijk waren 54 van de 60 uitspraken bewezen; de rest bleek niet meer nodig of viel af.
Het eindresultaat is gecontroleerd door de officiële controleur van Lean. Een vergelijking met de bedoelde stelling of een beoordeling door een onafhankelijke wiskundige, zoals bij de versie van september, is voor deze nieuwe versie nog niet gemeld.
Wat betekent dit voor de weg naar de singulariteit?
Dit experiment laat zien dat een groot team van AI-agents zichzelf kan organiseren en ruim een dag lang samen aan één moeilijke wiskundige klus kan werken, met een gedeelde database als werkvloer. Wat in september nog elf dagen en sturing door een mens kostte, lukte nu in iets meer dan een dag. De stap zit in het samenwerken en het foutloos uitwerken van bestaande wiskunde, met voorbereid werk als start. Lukt dat straks ook bij wiskunde die nog niemand heeft bewezen, dan kan AI een echte rol krijgen in het vinden van nieuwe kennis.
