AI-agents zetten het langste wiskundige bewijs ooit in 24 dagen om in controleerbare code
Het Amerikaanse bedrijf Axiom Math liet tientallen AI-agents het bewijs van 'de enorme stelling' over symmetrie, zo'n 15.000 pagina's, omzetten in code die een computer kan controleren. Onderweg vonden ze 34 afwijkingen in het gepubliceerde werk, die nu zijn gerepareerd.
Wiskundigen noemen het al decennia "de enorme stelling": de classificatie van eindige enkelvoudige groepen. Het bewijs is het langste uit de geschiedenis van de wiskunde. Het telt ongeveer 15.000 pagina's, verspreid over meer dan 500 artikelen van zo'n honderd wiskundigen. Geen mens kan dat in zijn eentje helemaal nalopen. Het AI-bedrijf Axiom Math meldde op 26 oktober dat het dat werk nu door een computer heeft laten controleren, stap voor stap.
In 24 dagen vertaalden tientallen AI-agents het hele bewijs naar Lean. Ingenieurs en wiskundigen van Axiom stuurden ze aan. Lean is een programmeertaal voor wiskunde: elke definitie en elke stap wordt zo precies opgeschreven dat software kan nagaan of hij klopt. Het resultaat is ongeveer 43,1 miljoen regels code. Axiom zet die code openbaar op GitHub, zodat iedereen hem zelf kan laten controleren.
Wat de stelling zegt
Groepen zijn in de wiskunde de taal van symmetrie. Een vierkant tegeltje kun je bijvoorbeeld een kwartslag draaien of omklappen zonder dat het er anders bij ligt. Al die bewegingen samen vormen een groep. Eindige enkelvoudige groepen zijn de bouwstenen waaruit alle eindige groepen zijn opgebouwd, zoals moleculen uit atomen. De stelling zegt dat er maar een paar soorten van die bouwstenen bestaan: een handvol families die eindeloos doorlopen, plus precies 26 buitenbeentjes. Het grootste buitenbeentje heet de Monstergroep. Die heeft ongeveer 8 × 10^53 elementen, een getal van 54 cijfers.
Het bewijs heeft een lange geschiedenis. In 1983 werd de classificatie als klaar aangekondigd. Toch bleef er een gat, dat pas in 2004 werd gedicht met een stuk van 1.221 pagina's van Michael Aschbacher en Stephen Smith. Wiskundigen werken ook al jaren aan een nieuwe, overzichtelijkere versie van het bewijs. Daarvan waren in 2023 tien van de minstens twaalf delen verschenen.
Fouten opgespoord en gerepareerd
Omdat de computer niets aanneemt, kwamen ook plekken boven waar het gepubliceerde bewijs niet helemaal klopte. Axiom telt 34 opvallende afwijkingen van wat er in de vakliteratuur staat. De belangrijkste zat in een bewijs uit 1986 dat deel uitmaakt van de classificatie. De agents vonden daar concrete tegenvoorbeelden voor één bewering. Om dat gat te dichten was een nieuw stukje wiskunde nodig, dat Axiom als apart artikel uitbrengt. Met die reparaties is het hele bewijs nu door de computer goedgekeurd.
Axiom overlegde daarbij met Richard Lyons en Ronald Solomon, twee groepentheoretici die aan de oorspronkelijke classificatie werkten en in de adviesraad van het bedrijf zitten. Het bedrijf publiceert ook een lijst met correcties, zodat andere wiskundigen ermee verder kunnen.
Het werk was opgedeeld in 108 mijlpalen en ongeveer 380 kleinere taken. De resultaten komen van Axiom zelf. Omdat de code openbaar is, kunnen andere wiskundigen nu nagaan of alles klopt. Daarbij kijken ze vooral of de definities in Lean precies hetzelfde zeggen als in het menselijke bewijs.
Nieuwe bewijzen en oude bewijzen
Deze maand meldden ook OpenAI en Anthropic dat hun AI-modellen grote wiskundige vraagstukken hebben opgelost, met bewijzen die een computer al heeft nagelopen. Daar vond de AI zelf iets nieuws. Axiom laat zien dat AI ook het omgekeerde kan: een bestaand menselijk bewijs dat te groot is om met de hand te controleren, helemaal nalopen en waar nodig verbeteren.
Wat betekent dit voor de weg naar de singulariteit?
AI kan nu werk leveren op een schaal waar geen menselijk team doorheen komt, en een computer kan dat werk tot in de kleinste stap controleren. Dat is belangrijk: hoe meer AI zelf bedenkt, hoe belangrijker het wordt dat we kunnen nagaan of het klopt zonder alles te hoeven geloven. De enorme stelling laat zien dat dat ook werkt bij een bewijs van 15.000 pagina's, en dat AI daarbij bestaande menselijke kennis niet alleen controleert, maar ook beter maakt. De volgende stap is dat wiskundigen de openbare code zelf nalopen.
