AI-agenten formaliseren Fermats laatste stelling in elf dagen

Fermats laatste stelling zegt dat er geen gehele getallen a, b en c bestaan die voldoen aan de vergelijking a hoogte n plus b hoogte n is c hoogte n, als n groter is dan 2. Wiskundige Pierre de Fermat beweerde in de zeventiende eeuw een bewijs te hebben, maar schreef er nooit een op. Pas in 1995 kwam de Britse wiskundige Andrew Wiles met een sluitend bewijs, na zeven jaar in het geheim werken. Zelfs dat bewijs bevatte aanvankelijk een fout, die Wiles samen met collega Richard Taylor pas na ongeveer een jaar herstelde.

Dat soort fouten is precies het probleem met traditionele wiskundige bewijzen: ze bestaan uit lange ketens van logische stappen, en als er ergens één schakel breekt, valt het hele bouwwerk om. Een oplossing hiervoor is formalisering: het omzetten van een bewijs in computercode die een machine regel voor regel kan controleren. Wiskundige Kevin Buzzard van Imperial College London werkte al aan een project van vijf jaar om Wiles' honderd pagina's tellende bewijs om te zetten naar de programmeertaal Lean. Volgens Buzzard overtuigden recente ontwikkelingen in AI hem ervan dat dit sneller zou gaan dan gedacht.

Elf dagen non-stop rekenen

Anthropic, bekend van het AI-model Claude, heeft dat project nu ingehaald. Het bedrijf zette meerdere AI-agents tegelijk aan het werk, elk verantwoordelijk voor een apart onderdeel van de stelling. Zo'n zwerm samenwerkende AI-modellen werkte elf dagen lang vrijwel autonoom door, met af en toe bijsturing van menselijke wiskundigen. Volgens Anthropic verloren de agents onderweg meerdere keren de grip op de voortgang van het project en moesten ze weer op één lijn worden gebracht. De doorbraak kwam toen de agents gebruik gingen maken van Prove2Me, een hulpmiddel dat oorspronkelijk is ontworpen om menselijke wiskundigen te laten samenwerken aan bewijzen.

Grootste bewijs ooit in Lean

Het resultaat is indrukwekkend van omvang: 13 miljoen regels code in Lean, opgebouwd uit ruim 29.500 tussenliggende deelstellingen. Daarmee is dit formele bewijs meer dan vijf keer zo groot als alle wiskunde die tot nu toe in de centrale formaliseringsbibliotheek Mathlib stond, en het grootste bewijs dat ooit in Lean is geschreven. Het werk raakt bovendien meerdere wiskundige vakgebieden, waaronder algebraïsche meetkunde, harmonische analyse en getaltheorie. Buzzard noemt het resultaat in een verklaring van Anthropic een bewijs dat 'geen andere aannames bevat dan de axioma's van de wiskunde zelf' — kortom, het probleem is definitief opgelost. Volgens hem is de automatische formalisering van Fermats laatste stelling een belangrijke stap richting het automatisch formaliseren van de moderne wiskundige literatuur als geheel.