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

09/10 08:15 - TU/e-wiskundige lost zestig jaar oud probleem op met AI
Een wiskundig raadsel uit 1965 is opgelost. Tom Verhoeff van de TU Eindhoven bewees het met hulp van kunstmatige intelligentie (AI). Een nieuwer AI-model vond daarna zelfstandig een veel korter en duidelijker bewijs. Volgens Verhoeff laat dat zien hoe snel AI zich ontwikkelt. Verhoeff is gepensioneerd wiskundige en informaticus. Stel je een rij dansers voor van wie sommigen dezelfde kleur kleding dragen. Steeds wisselen twee buren van plek. Kun je zo elke mogelijke opstelling precies één keer langs laten komen? De Amerikaanse wiskundige D.H. Lehmer vermoedde in 1965 dat dat kan, op een paar kleine omwegen na. Een bewijs bleef uit. In 2017 loste Verhoeff al het geval met twee kleuren op. Nu bewees hij met hulp van AI dat het ook lukt met meer kleuren en verschillende aantallen dansers per kleur, meldt de TU Eindhoven. Van 150 naar minder dan 30 pagina'sZijn eerste bewijs besloeg zo'n 150 pagina's. Verhoeff liet het controleren door Lean, een computerprogramma dat elke stap van een wiskundig bewijs nakijkt. Die controle telde ruim 100.000 regels. In september vroeg hij Claude Opus 5.5 van het AI-bedrijf Anthropic om helemaal opnieuw te beginnen, zonder het lange bewijs als uitgangspunt. Binnen een paar uur kwam het model met twee nieuwe ideeën. Het nieuwe bewijs is korter dan dertig pagina's, en de controle in Lean telt nog ongeveer 35.000 regels. Ook andere AI-systemen werkten mee. DeepSeek V4.1 Flash zette de stappen van het bewijs om in een programma dat de redeneringen met concrete voorbeelden controleert. Dat rekenwerk gebeurde op Spike-1, de supercomputer van de TU Eindhoven. Het systeem Aristotle van Harmonic schreef daarna de formele controle in Lean. Ingrijpend voor onderwijsVolgens Verhoeff ontwikkelen de wiskundige vaardigheden van AI zich in razend tempo. Hij vindt de verandering veel ingrijpender dan de komst van de rekenmachine in de jaren zeventig of van computeralgebrasystemen (software die formules uitrekent) in de jaren tachtig. De TU Eindhoven en andere universiteiten moeten daarom opnieuw nadenken over hoe ze wiskunde onderwijzen en onderzoeken. "We kunnen het ons niet veroorloven om het maar op z'n beloop te laten", zegt hij. Hoe snel het gaat, blijkt ook uit het nieuws dat OpenAI een intern model gebruikte om honderden wiskundige vraagstukken op te lossen of dichter bij een oplossing te brengen. Verhoeff is daar kritisch over. Volgens hem zijn die problemen nauwelijks bekend, ook niet bij wiskundigen, en is het werk niet erg toegankelijk opgeschreven. Verhoeff heeft zijn bewijs als preprint op arXiv gezet. Een preprint is een wetenschappelijk artikel dat nog niet officieel is beoordeeld. Andere wiskundigen kunnen het bewijs nu bestuderen en controleren....