Deze wiskundige werkte jarenlang aan één probleem en zag AI uitgroeien van assistent tot grootmeester

Stel je zes dansers voor in een rij. Telkens wisselen twee buren van plek. Kun je zo elke mogelijke opstelling één keer laten passeren zonder eerdere opstellingen te herhalen? Ja, dat kan, weten wiskundigen al sinds de 17^de eeuw. Maar wat als sommige dansers er hetzelfde uitzien, bijvoorbeeld twee in het groen, twee in het blauw en twee in het geel? De Amerikaanse wiskundige D.H. Lehmer vermoedde in 1965 dat ook dan zo'n rondgang mogelijk is, op een paar kleine, vooraf bepaalde omwegen na. Een bewijs bleef echter zestig jaar uit.

Tom Verhoeff, gepensioneerd wiskundige en informaticus aan de TU/e, loste in 2017 al het binaire geval op, met twee verschillende soorten symbolen (‘kleuren’). Nu heeft hij met behulp van AI ook het algemene geval opgelost: zelfs wanneer meerdere soorten symbolen in allerlei verschillende aantallen voorkomen, kan de gewenste rondgang worden gemaakt. Daarmee bewijst hij het permutatievermoeden van Lehmer, zoals Verhoeff het zelf heeft gedoopt. De grootste doorbraak kwam pas een paar weken geleden.

100.000 regels teruggebracht tot 35.000

Bij een wiskundig bewijs gaat het niet alleen om de vraag óf iets waar is, maar ook om de manier waarop je dat aantoont. Een bewijs van honderden pagina's kan correct zijn, maar een veel korter bewijs kan laten zien dat de onderliggende structuur beter wordt begrepen.

Verhoeff’s eerst oplossing bestond uit zo'n 150 pagina's. Daarnaast werd het bewijs formeel gecontroleerd in Lean, een computersysteem dat iedere stap van een wiskundig bewijs automatisch verifieert. Die controle omvatte ruim 100.000 regels.

Verhoeff vroeg afgelopen september het nieuwe model Claude Opus 5.5 van AI-bedrijf Anthropic om helemaal opnieuw te beginnen. Binnen een paar uur kwam het met twee nieuwe kernideeën: alle volgordes verdelen in nette blokken en die blokken slim aan elkaar koppelen. Het bewijs is nu korter dan 30 pagina's en de Lean-controle is teruggebracht tot ongeveer 35.000 regels.

‘Bewijs dat AI zich in razend tempo ontwikkelt’

Het nieuwe bewijs is geen ingekorte versie van het oude. Verhoeff gaf het model niet het lange bewijs als uitgangspunt, maar alleen de uitdaging om het probleem vanaf nul op te lossen. "Het lange bewijs is in nauwe samenwerking met mij ontstaan, het kortere bewijs is autonoom geleverd", zegt hij. "Overigens had ik dat in maart ook geprobeerd, maar dat leverde toen niets bruikbaars op."

“Dat toont aan dat de wiskundige vaardigheden van AI-modellen zich in razend tempo ontwikkelen”, zegt Verhoeff daarover. “Dit verandert het veld veel ingrijpender dan de komst van de rekenmachine in de jaren zeventig of computeralgebrasystemen in de jaren tachtig. Het dwingt ons om opnieuw na te denken over hoe we wiskunde aan de TU/e en elders onderwijzen en onderzoek doen. We kunnen het ons niet veroorloven om het maar op z’n beloop te laten.”

Wie deed wat?

De kernideeën voor het eenvoudige bewijs kwamen van Claude Opus 5.5. Vervolgens zette het AI-model DeepSeek V4.1 Flash de verschillende stappen van het bewijs om in een programma dat de redeneringen uitvoert en aan de hand van concrete voorbeelden controleert.

Dat rekenwerk werd uitgevoerd op Spike-1, de supercomputer van de TU/e. “Die rekenkracht heeft ervoor gezorgd dat we de cyclus van AI-output naar menselijke controle naar nieuwe vraag aan het model en opnieuw controleren snel genoeg konden doorlopen om het bewijs af te ronden”, zegt Verhoeff daarover. Het systeem Aristotle van Harmonic schreef vervolgens de formele controle in Lean.

Volgens Verhoeff was het in december vorig jaar nog niet mogelijk voor geavanceerde AI-modellen om serieuze wiskunde te bedrijven. “GPT-5.2 (van OpenAI -red.) maakte nog hele basale fouten. In mei lag het al anders, toen Opus 4.7 van Anthropic een volwassen begrip toonde en als assistent op geavanceerd niveau kon fungeren. Maar Opus 5.5 heeft me echt verrast, die wist het probleem autonoom op te lossen.”

Berg oplossingen

Het gaat hier om algemeen beschikbare modellen. De modellen waar AI-bedrijven intern over beschikken, zijn al verder. Dat blijkt onder meer uit het nieuws dat OpenAI een intern model heeft gebruikt om honderden wiskundige vraagstukken op te lossen of in elk geval dichter bij een oplossing te komen. Daar zit het permutatievermoeden van Lehmer overigens niet tussen.

Verhoeff: “Als je de lijst met problemen bekijkt die OpenAI zegt te hebben opgelost, dan zit er vrijwel niets tussen dat mij als wiskundige bekend voorkomt, laat staan dat begrijpelijk is voor een breder publiek. Een probleem uit de combinatoriek waar ik me mee bezig heb gehouden is misschien lastig te doorgronden voor een leek, maar de OpenAI-lijst komt op mij écht esoterisch over. De vraag is hoe zo’n enorme berg de wiskunde verder brengt. En naar ik verneem, is het ook niet erg toegankelijk opgeschreven.”

Verhoeff heeft de oplossing voor ‘zijn’ probleem als preprint ingediend op arXiv, zodat anderen het bewijs kunnen bestuderen.