Lean keurt Fermat-bewijs van Claude goed

Lean, software waarmee wiskundigen formele bewijzen controleren, heeft een volledige formalisering van de laatste stelling van Fermat aanvaard. De door Anthropic’s Claude gemaakte uitwerking is openbaar beschikbaar en bevat geen onopgeloste tussenstappen, aanvullende axioma’s of rekenkundige sluiproutes buiten de standaardgrondslagen van Lean (repository). Kevin Buzzard, de wiskundige van Imperial College London die leidinggaf aan een eigen formalisering, compileerde het project onafhankelijk en bevestigde dat het klopt. Hij noemt het ‘een buitengewone prestatie op het gebied van automatische formalisering’ (Buzzard).

Over de wiskunde bestond al lang geen twijfel meer. Andrew Wiles bewees de stelling in 1995. Wat nog ontbrak, was een versie voor een letterlijke controleur: software die iedere definitie en tussenstap moet krijgen aangereikt, ook waar een wiskundige die zonder uitleg begrijpt. Volgens Anthropic voltooiden tientallen AI-agenten die omzetting in augustus binnen elf dagen. Via het platform Prove2Me werkten zij parallel aan verschillende onderdelen (Anthropic).

Die elf dagen zeggen weinig over de reproduceerbaarheid van het productieproces. Het interne model, de infrastructuur voor de aansturing van de agenten, de beslissingen van menselijke operators en het rekenverbruik zijn niet openbaar gemaakt. Het eindproduct is wél reproduceerbaar: met voldoende rekenkracht kan iedereen het Lean-project opnieuw compileren en controleren. Een afzonderlijke, door Anthropic in Rust geschreven controleur onderzocht hetzelfde formele bestand en stelde vast dat alle 1.052.234 declaraties onderling consistent zijn (technical report). Dat is een tweede lezing van hetzelfde werkstuk, geen onafhankelijke herhaling van de elf dagen durende productie.

Hoe de agenten te werk gingen

Bij het formaliseren wordt een wiskundig betoog herschreven voor een programma zonder wiskundige intuïtie, dat elke logische stap afzonderlijk moet kunnen verifiëren. De stelling zelf oogt eenvoudig: bij iedere gehele exponent van drie of hoger bestaan er geen drie positieve gehele getallen waarvoor aⁿ + bⁿ = cⁿ. Het bewijs voert echter over honderden pagina’s door verscheidene diepere lagen van de getaltheorie.

Claude ontdekte daarbij geen nieuwe wiskunde. Het systeem formaliseerde de bekende reeks resultaten waarop Wiles’ bewijs rust en volgde daarvoor een uiteenzetting van de wiskundigen Henri Darmon, Fred Diamond en Richard Taylor (Anthropic, technical report). Het oorspronkelijke inzicht kwam van Wiles en zijn voorgangers. Claude zette dat denkwerk om in ongeveer 10,5 miljoen regels code die een machine stap voor stap kan controleren (technical report).

Prove2Me, ontwikkeld door Anthropic-onderzoeker Tianyi Peng en medewerkers van Columbia University, verdeelde het bewijs in een afhankelijkheidsnetwerk van ongeveer 29.511 zelfstandige beweringen (technical report). De agenten kozen onderdelen waarvoor alle voorafgaande stappen gereed waren, schreven daarvoor bewijzen in Lean en controleerden elkaars voorgestelde formuleringen. Zo konden veel taken tegelijk worden uitgevoerd. De operatie vergde ongeveer zes miljard uitvoertokens van een intern onderzoeksmodel (technical report).

Volgens Anthropic schreven menselijke operators tijdens het proces geen Lean-code. Zij kozen wel de stelling en de bestaande bewijsroute, ontwierpen de infrastructuur voor de agenten en stelden af en toe de prioriteiten bij (Anthropic). Het volledige logboek van hun ingrepen en de kosten van de gebruikte rekenkracht zijn niet bekendgemaakt.

Gebouwd op jarenlang mensenwerk

Het resultaat steunt op Mathlib, de omvangrijke bibliotheek met geformaliseerde wiskunde die door een gemeenschap wordt onderhouden, en put rechtstreeks uit twee eerdere projecten. Sinds eind 2023 werkte Buzzards team bij Imperial aan een Lean-formalisering van de laatste stelling van Fermat. Daarvoor ontving het een EPSRC-subsidie van £ 1 miljoen, met een looptijd tot 2029 (EPSRC award). Een ander gemeenschapsproject had de stelling al voor een deel van de mogelijke gevallen geformaliseerd. In het bronbestand met vermeldingen van Anthropic staan 106 bestanden die materiaal uit deze projecten bevatten of daarop zijn gebaseerd (attribution).

Door de parallelle werkwijze laten de elf kalenderdagen zich niet vergelijken met het aantal mensuren van Buzzards team. Toen Claude aan de opdracht begon, liep dat gefinancierde project immers al ongeveer 22 maanden (EPSRC award). Anthropic maakte noch het aantal GPU-uren, noch het energieverbruik bekend.

Voor deze publicatie was de laatste stelling van Fermat het enige resterende onderdeel op Freek Wiedijks lijst van honderd belangrijke stellingen die nog moesten worden geformaliseerd. Die lijst dient al twintig jaar als graadmeter voor de voortgang op dit terrein (Buzzard).

De bruikbaarheid van deze aanpak buiten dit project zal vooral blijken bij recente, minder goed beschreven wiskunde waarvoor geen uitgewerkte route, volwassen bibliotheken of eerder formaliseringswerk beschikbaar zijn. Hier ging het om een beroemde stelling waarvoor al veel infrastructuur klaarlag. De proef laat zien dat AI-agenten met een bekende bewijsroute en eerder formeel werk een volledige formalisering kunnen produceren die Lean aanvaardt en buitenstaanders opnieuw kunnen controleren. Hoe Anthropic dat eindproduct in elf dagen voortbracht, valt met het gepubliceerde materiaal echter niet te reproduceren.