AI vindt zelfstandig korter bewijs voor zestig jaar oud wiskundig probleem
Een gepensioneerde wiskundige van de TU Eindhoven heeft met behulp van AI een aanzienlijk korter bewijs gevonden voor een vermoeden dat in 1965 werd geformuleerd. Het oorspronkelijke bewijs besloeg ongeveer 150 pagina’s en meer dan 100.000 regels code; het nieuwe blijft onder de dertig pagina’s en ongeveer 35.000 regels. Het kortere bewijs werd door het model zelfstandig gevonden, zonder dat het het lange bewijs had gezien.
De TU Eindhoven publiceerde het verhaal op 8 oktober 2026. Het gaat om Tom Verhoeff, gepensioneerd wiskundige en informaticus aan de universiteit, en om het permutatievermoeden van de Amerikaanse wiskundige D.H. Lehmer uit 1965. Verhoeff bewees het binaire geval in 2017; het algemene geval lukte nu met AI.
Drie modellen deden verschillend werk. Claude Opus 5.5 leverde de kernideeën van het kortere bewijs, DeepSeek V4.1 Flash zette bewijsstappen om in een controleprogramma, en Aristotle van Harmonic verzorgde de formele verificatie in Lean.
Het opvallendste is hoe snel dat ging. Binnen enkele uren kwam het model met twee kernideeën: het opdelen van het probleem in gestructureerde blokken en het verbinden van die blokken. Verhoeff vat het verschil zelf samen: “The long proof emerged in close collaboration with me, the shorter proof was produced autonomously.”
Formele verificatie maakt het verschil
Voor ondernemers is niet het wiskundige resultaat het leerzame deel, maar de werkwijze. Het bewijs is niet geloofd omdat het overtuigend klonk, maar in Lean formeel geverifieerd: een computerprogramma controleerde elke stap.
Dat is het ontbrekende stuk bij veel AI-toepassingen in het bedrijfsleven. Een model dat een plausibel antwoord geeft, is pas bruikbaar wanneer er een onafhankelijke controle op kan. In de wiskunde bestaat die controle; in de meeste zakelijke toepassingen niet.
De preprint staat op arXiv onder nummer 2610.01240. Op 12 oktober 2026 voegde Verhoeff een visualisatie van het bewijs toe op zijn eigen site.
Van assistent naar zelfstandige bijdrage
Het verschil tussen de twee bewijzen is het verhaal. Het lange bewijs kwam tot stand in nauwe samenwerking tussen de onderzoeker en de modellen; het korte kwam vanaf nul, zonder dat het model het eerdere resultaat kreeg.
Dat is een ander soort claim dan de gebruikelijke productiviteitswinst. Hier gaat het niet om sneller werken aan een bekende taak, maar om een oplossing die de mens niet had bedacht.
Duiding: zoek naar taken die een controleerbaar antwoord hebben
Een concrete kans voor Nederlandse bedrijven zit in het selecteren van het juiste type probleem. AI presteert het best waar het antwoord achteraf te controleren is: een berekening die klopt of niet, code die een test haalt of niet, een configuratie die werkt of niet. Wie zoekt naar toepassingen, kan beginnen bij taken met zo’n controle, in plaats van bij taken waarin de kwaliteit een kwestie van smaak is. Daarbij hoort ook dat drie verschillende modellen voor drie verschillende stappen werden gebruikt, niet één model voor alles.
Het risico is overdracht naar het verkeerde domein. Een zelfstandig gevonden wiskundig bewijs zegt niets over de betrouwbaarheid van een model bij een commercieel of juridisch vraagstuk, juist omdat daar de formele verificatiestap ontbreekt. De les zit in het controlemechanisme, niet in de prestatie. Dit is redactionele duiding.
Meer informatie
Primaire bron: TU Eindhoven over het onderzoek van Tom Verhoeff