Tom Verhoeff, wiskundige van de TU/e, heeft een wiskundig vermoeden uit 1965 bewezen, met flinke hulp van kunstmatige intelligentie. Opvallend is vooral wat er daarna gebeurde: een nieuw AI-model vond in een paar uur zelfstandig een bewijs dat vele malen korter is dan het oorspronkelijke. Volgens Verhoeff laat dat zien hoe snel AI zich ontwikkelt tot een serieuze speler in de wiskunde. Hij vindt dat universiteiten, ook de TU/e, hun onderwijs en onderzoek daarop moeten aanpassen.
Het probleem is het makkelijkst uit te leggen met dansers. Zet zes dansers in een rij en laat telkens twee buren van plek wisselen. Dat je zo elke mogelijke opstelling precies één keer kunt laten langskomen, weten wiskundigen al sinds de zeventiende eeuw. Maar wat als een aantal dansers er hetzelfde uitziet, bijvoorbeeld twee in het groen, twee in het blauw en twee in het geel? De Amerikaanse wiskundige D.H. Lehmer vermoedde in 1965 dat zo’n rondgang dan ook bestaat, op een paar kleine, vooraf vast te stellen omwegen na. In het voorbeeld met drie kleuren zijn dat er zes: na 96 stappen zijn alle opstellingen gepasseerd en sta je weer aan het begin.
Zestig jaar zonder bewijs
Een bewijs liet zestig jaar op zich wachten. Verhoeff, gepensioneerd wiskundige en informaticus van de TU/e, liet het probleem al decennia niet los. In 2017 loste hij het geval met twee soorten dansers op. Nu heeft hij met hulp van AI ook het algemene geval bewezen, met willekeurig veel kleuren in willekeurige aantallen. Het bewijs staat sinds begin oktober als preprint op arXiv, het online archief waar wetenschappers hun werk delen voordat vakgenoten het officieel hebben beoordeeld. Die beoordeling moet dus nog volgen.
Een kortere route, zelfstandig gevonden
Verhoeffs eerste bewijs, dat het afgelopen jaar in nauwe samenwerking met AI-modellen ontstond, besloeg zo’n 150 pagina’s. Het werd bovendien gecontroleerd in Lean, software die elke stap van een wiskundig bewijs automatisch verifieert. Die controle telde ruim 100.000 regels. In september vroeg Verhoeff het nieuwe model Claude Opus 5.5 van het Amerikaanse AI-bedrijf Anthropic om helemaal opnieuw te beginnen, zonder het lange bewijs als vertrekpunt. Binnen een paar uur kwam het model met twee kernideeën: verdeel alle opstellingen in overzichtelijke blokken en koppel die slim aan elkaar. Het resultaat is een bewijs van minder dan dertig pagina’s, met een Lean-controle van ongeveer 35.000 regels.
Voor wiskundigen is dat meer dan een cosmetische verbetering. Een korter bewijs laat doorgaans zien dat de onderliggende structuur beter wordt begrepen. “Het lange bewijs is in nauwe samenwerking met mij ontstaan, het kortere bewijs is autonoom geleverd”, zegt Verhoeff. In maart had hij hetzelfde geprobeerd, toen zonder bruikbaar resultaat.
Modellen en een supercomputer
Opus 5.5 leverde de ideeën, maar het bewijs kwam tot stand via een hele keten. Het Chinese model DeepSeek V4.1 Flash zette de stappen om in een programma dat de redeneringen uitvoert en aan concrete voorbeelden toetst. Dat rekenwerk draaide op Spike-1, de AI-supercomputer van de TU/e, die overigens in een datacenter in het Finse Kajaani staat. Volgens Verhoeff maakte die rekenkracht het mogelijk om snel genoeg te schakelen tussen AI-uitvoer, menselijke controle en nieuwe vragen aan het model. Het systeem Aristotle van het Amerikaanse bedrijf Harmonic schreef ten slotte de formele controle in Lean.
Ingrijpender dan de rekenmachine
Verhoeff zag de ontwikkeling van dichtbij versnellen. In december vorig jaar maakte GPT-5.2 van OpenAI volgens hem nog “hele basale fouten”. In mei werkte Anthropics Opus 4.7 al als assistent op geavanceerd niveau, en Opus 5.5 loste het probleem zelfstandig op. “Dit verandert het veld veel ingrijpender dan de komst van de rekenmachine in de jaren zeventig of computeralgebrasystemen in de jaren tachtig”, zegt hij. “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.”
Kanttekening bij OpenAI
De publicatie valt samen met een opvallende stap van OpenAI. Dat bedrijf bracht begin oktober 722 wiskundige manuscripten naar buiten, gegenereerd met een intern model dat niet publiek beschikbaar is. Lehmers vermoeden zit daar niet tussen. Verhoeff is kritisch: “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.” Hij vraagt zich af hoe zo’n berg resultaten de wiskunde verder helpt, temeer omdat ze volgens hem weinig toegankelijk zijn opgeschreven. Of zijn eigen bewijs overeind blijft, moet nu blijken nu vakgenoten het kunnen bestuderen.
