Axiom laat AI-agents het grootste wiskundebewijs controleren

Het grootste bewijs uit de wiskunde is nu door een computer gecontroleerd. Het Amerikaanse AI-bedrijf Axiom meldde op 26 oktober dat het de classificatie van eindige enkelvoudige groepen volledig heeft omgezet naar de bewijsassistent Lean. Het oorspronkelijke bewijs beslaat zo’n 15.000 pagina’s, verspreid over meer dan 500 artikelen van ongeveer honderd wiskundigen. Axiom deed er met een zwerm AI-agents 24 dagen over.

Wat is er bewezen?

Eindige enkelvoudige groepen zijn de bouwstenen van symmetrie, vergelijkbaar met priemgetallen bij gewone getallen. De classificatie, in vakkringen ook wel het “Enormous Theorem” genoemd, zegt dat elke zo’n groep in een van 18 oneindige families valt, of een van de 26 sporadische uitzonderingen is. De grootste daarvan is de Monster-groep, met ongeveer 8 x 10⁵³ elementen.

Volgens de technische verantwoording van Axiom telt de formalisering ongeveer 43,1 miljoen regels Lean-code. Daarin zit ook circa 1,2 miljoen regels uit het eerdere project Qiuzhen-CFSG, en het geheel bouwt voort op de open bibliotheek Mathlib. Het werk was opgeknipt in 108 mijlpalen en zo’n 380 kleinere taken. Op 10 oktober was de enkelvoudigheid van de Monster al rond.

Fouten in de literatuur gevonden

Interessanter dan het aantal regels is wat de agents onderweg tegenkwamen. Axiom documenteert 34 opvallende afwijkingen van de gepubliceerde bewijzen. De meeste zijn klein: typefouten, foute tabellen of een vergeten aanname. Eén probleem was serieus. In het bewijs van de Unbalanced Group Theorem uit 1986 van John Walter vonden de agents tegenvoorbeelden voor een tussenstap, met de groep PSL₂(49) als boosdoener. Het team verving dat stuk door een route via werk van Ron Solomon uit 1976 en schreef er een apart artikel over.

Wiskundige Vasily Ilin, een van de kernleden van het project, schreef op X dat de meeste mensen die het bewijs echt begrepen inmiddels met pensioen zijn of niet meer leven. Juist daarom is een machinecontrole waardevol: de kennis zit nu in code die iedereen opnieuw kan draaien.

Nog niet onafhankelijk getoetst

De claim komt van Axiom zelf. Lean controleert elke stap, maar mensen moeten nog nagaan of de formele stelling precies zegt wat de klassieke classificatie zegt. Axiom wijst daar zelf op en vraagt buitenstaanders om de controle opnieuw uit te voeren. De errata worden nog bijgewerkt met een adviesraad waarin onder anderen Richard Lyons en Ron Solomon zitten. The Neuron zette het nieuws in zijn dagoverzicht naast een BBC-stuk over twijfels bij AI-ontdekkingen in de wiskunde, en dat is precies de discussie die hier speelt.

Het past in een reeks. Eerder dit najaar formaliseerde Claude het bewijs van Fermat in Lean, en OpenAI claimde AI-bewijzen voor onder meer Yang-Mills. Ook in software rukt formele verificatie op: Anthropic liet Claude bewijzen dat 123 codebibliotheken niet crashen.

“Wat mij opvalt: de AI wijst ons aan waar mensen veertig jaar geleden een steek lieten vallen. Wie AI aanstuurt met heldere opdrachten en harde controlepunten, krijgt er een kritische collega bij.”

Leon Tindemans, AI-expert en Copilot- & ChatGPT-trainer. Hij geeft onder meer de training prompts schrijven voor AI bij TTM Communicatie.

Wat betekent dit?

Voor de wiskunde is dit vooral een archiefkwestie die opgelost lijkt: een bewijs dat bijna niemand meer volledig overzag, is nu controleerbaar door een computer. Voor de AI-wereld laat het zien dat agents lang en zelfstandig aan een groot project kunnen werken, zolang een strenge controleur als Lean elke stap afkeurt die niet klopt. Dat principe (AI laten werken, een machine laten controleren) is ook bruikbaar buiten de wiskunde, bijvoorbeeld bij code en contracten. Of het bewijs echt compleet is, moet de komende maanden blijken uit onafhankelijke controle.