AI helpt Eindhovense wiskundige een zestig jaar oud vermoeden bewijzen.

Stel dat je een rij voorwerpen hebt en telkens twee buren van plek mag laten wisselen. Kun je zo alle mogelijke volgordes doorlopen zonder een volgorde te herhalen, ook als sommige voorwerpen identiek zijn? De Amerikaanse wiskundige D.H. Lehmer vermoedde in 1965 dat dit in het algemeen kan, maar een bewijs bleef uit.

De gepensioneerde TU/e-wiskundige Tom Verhoeff heeft nu een bewijs voor het algemene geval gepubliceerd. Hij werkte daarbij met AI-modellen. Volgens TU/e hielp een nieuwer model om een veel kortere oplossing te vinden dan de eerdere uitwerking. De redenering is ook formeel vastgelegd in Lean, een programma waarmee wiskundige bewijzen controleerbaar worden gemaakt.

Het manuscript staat op arXiv als preprint. Dat maakt het publiek controleerbaar, maar betekent ook dat een wetenschappelijk tijdschrift het nog niet heeft beoordeeld. De ontwikkeling is dus een opvallend onderzoeksresultaat, geen afgeronde peer-reviewed publicatie. TU/e beschrijft ook hoe AI in de loop van het project veranderde van hulpmiddel naar een systeem dat zelfstandig een korter bewijs kon vinden. Dat maakt de samenwerking nieuwswaardig, maar de wiskundige controle blijft de kern: de uitkomst moet als bewijs standhouden, ongeacht welk hulpmiddel eraan bijdroeg. Verhoeff werkt al langer aan varianten van het probleem; volgens TU/e had hij in 2017 al een eenvoudiger, binair geval opgelost.