TU/e-wiskundige lost zestig jaar oud probleem op met AI

In dit artikel:

De gepensioneerde wiskundige en informaticus Verhoeff heeft met hulp van verschillende AI-systemen een oud vermoeden uit de combinatoriek bewezen. Het probleem draait om een rij dansers, van wie sommigen dezelfde kleur kleding dragen. Door steeds twee naast elkaar staande dansers van plaats te laten wisselen, moet elke mogelijke opstelling precies één keer worden doorlopen. De Amerikaanse wiskundige D.H. Lehmer vermoedde in 1965 dat dit, op enkele kleine uitzonderingen na, altijd mogelijk is.

Verhoeff bewees in 2017 al het geval met twee kleuren. Zijn nieuwe bewijs geldt ook voor meerdere kleuren en verschillende aantallen dansers per kleur. De eerste versie was ongeveer 150 pagina’s lang en werd formeel gecontroleerd met Lean, dat meer dan 100.000 regels naliep. Claude Opus 5.5 kwam vervolgens binnen enkele uren met nieuwe ideeën, waarmee het bewijs tot minder dan dertig pagina’s kon worden teruggebracht; de Lean-controle omvat nu circa 35.000 regels. DeepSeek V4.1 Flash en Aristotle hielpen bij respectievelijk berekeningen en de formele controle op de supercomputer Spike-1 van de TU Eindhoven.

Verhoeff waarschuwt dat AI de beoefening en het onderwijs in de wiskunde ingrijpend verandert. Zijn nog niet officieel beoordeelde bewijs staat als preprint op arXiv, zodat andere wiskundigen het kunnen controleren.