EnglishAI-agents zetten 7.500 pagina's wiskunde om in bewijzen die een computer kan controleren
Het Amerikaanse bedrijf Axiom Math heeft met AI-agents een wiskundig naslagwerk van zo'n 7.500 pagina's omgezet in 16 miljoen regels code die een computer kan controleren. Onderweg vonden de agents tientallen punten die verfijnd moesten worden. Mensen kijken het werk nu verder na.
Een wiskundig bewijs is pas betrouwbaar als iemand elke stap heeft nagelopen. Bij lange bewijzen is dat veel werk, en ook wiskundigen maken fouten. Daarom schrijven steeds meer onderzoekers bewijzen als computercode. Een programma, een zogeheten bewijsassistent, controleert die code dan regel voor regel. Lean is zo'n programma; het bedrijf Physical Superintelligence liet er eerder ook vijf quantumbewijzen mee controleren.
Het Amerikaanse bedrijf Axiom Math maakte op 4 november bekend dat zijn AI-agents dit hebben gedaan voor een compleet naslagwerk: het Stacks Project. Dat is een open verzameling van zo'n 7.500 pagina's over algebraïsche meetkunde, de tak van de wiskunde die vormen beschrijft met vergelijkingen. Johan de Jong van Columbia University begon eraan in 2005. Zijn collega Peter Woit schrijft dat er niets anders echt mee te vergelijken is.
Het resultaat is ongeveer 16 miljoen regels Lean-code. Volgens Axiom is dit de grootste samenhangende verzameling wiskunde in deze vorm die ooit is gebouwd.
Zo pakten de agents het aan
Stellingen in zo'n naslagwerk steunen op elkaar. De agents werkten daarom tegelijk aan verschillende stukken van dat netwerk. Ze vertaalden stellingen naar code, zochten in Mathlib, de grote gezamenlijke Lean-bibliotheek van wiskundigen, wat er al bestond, en bouwden de bewijzen. Axiom trainde daarvoor eigen AI-modellen.
Lean controleert of een bewijs klopt, maar niet of de stelling in de code hetzelfde zegt als in de oorspronkelijke tekst. Axiom noemt dat zelf zelfs het belangrijkste onderdeel. Het liet agents daarom de code vergelijken met de tekst en deed extra controles op de basisbegrippen en de belangrijkste stellingen.
Daarbij kwamen tientallen uitspraken in het naslagwerk boven die verfijnd moesten worden, bijvoorbeeld omdat er een voorwaarde ontbrak of omdat een bewering niet zo algemeen gold als er stond. De agents bouwden dan een tegenvoorbeeld. Bij een onjuiste hulpstelling zochten ze een andere route naar hetzelfde hoofdresultaat.
Mensen kijken nu verder na
De bibliotheek bestaat uit twee delen. StacksCore is door mensen vergeleken met het naslagwerk en voldoet aan de eisen van Mathlib. StacksFrontier is door agents geschreven en heeft die controle nog niet gehad. Lean controleert de bewijzen in beide delen. De code is openbaar, en vier beheerders beoordelen elke nieuwe bijdrage.
De bewering dat het hele werk nu is omgezet, komt van Axiom zelf. Johan de Jong vroeg op 21 oktober om AI-bijdragen voorlopig niet rechtstreeks naar het Stacks Project zelf te sturen. Axiom houdt de omgezette versie daarom in een eigen project.
Waarom dit belangrijk is
Wie nieuwe resultaten in dit vakgebied met Lean wil controleren, had tot nu toe weinig om op voort te bouwen, zegt Axiom. Onderzoekers en AI-agents kunnen de stellingen nu rechtstreeks gebruiken in nieuwe bewijzen.
Dat komt op een moment dat AI steeds meer wiskunde produceert. OpenAI bracht vorige maand 719 manuscripten uit met oplossingen voor zware wiskundige vraagstukken, meldt TechCrunch, die nog niet aan de eisen van het vakgebied bleken te voldoen. Gecontroleerde bewijzen maken zulk werk beter te beoordelen.
Axiom denkt verder dan wiskunde. Het bedrijf verwacht dat ook software straks moet rusten op zulke gecontroleerde fundamenten, nu AI steeds meer code schrijft. Topvrouw Carina Hong, die het bedrijf in 2025 oprichtte, daagde codeerbedrijven tegenover TechCrunch uit om op deze schaal aan formele controle te werken.
Wat betekent dit voor de weg naar de singulariteit?
Hoe meer AI zelf schrijft, hoe minder mensen alles kunnen nalezen. Een computer die het werk stap voor stap controleert, kan dan veel van dat nakijken overnemen. Dit project is een grote proef daarmee: AI-agents bouwen een fundament waarop andere agents en onderzoekers verder kunnen werken. Het menselijk nakijken van het AI-deel is de volgende stap. Blijkt de aanpak ook elders te werken, dan kan AI straks wiskunde en software leveren waarvan de bewijzen vanzelf meekomen.
