Microsoft-onderzoekers bewijzen KLS-vermoeden met hulp van AI
Een wiskundig probleem dat sinds 1995 openstond, is opgelost. Microsoft Research meldde op 21 oktober dat senior onderzoeker Xinzhi Zhang en co-auteur Zhao Song het zogeheten KLS-vermoeden hebben bewezen. Opvallend is de werkwijze: een groep AI-agents deed het zoekwerk, de onderzoekers bepaalden de koers.
Waar gaat het KLS-vermoeden over?
Het vermoeden is genoemd naar Ravi Kannan, László Lovász en Miklós Simonovits, die het in 1995 opstelden. Volgens de uitleg op het blog van Microsoft Research gaat het om het doorsnijden van hoogdimensionale kansverdelingen. De bewering: de beste vlakke snede is bijna even goed als de beste snede van willekeurige vorm. Het verschil blijft onder een vaste constante, hoeveel dimensies je ook toevoegt.
Dat klinkt abstract. Het raakt echter aan de vraag hoe snel een random walk een verdeling verkent, en daar draait het bemonsteren van data in hoge dimensies om. Het Simons Institute noemde KLS eerder “een van de belangrijkste open problemen in de convexe meetkunde”. Resultaten die tot nu toe alleen golden als het vermoeden klopte, kunnen nu zonder dat voorbehoud worden opgeschreven, schrijft Microsoft.
Honderd zoekpaden, de mens kiest
Het bewijs staat in het artikel “An O(1) Bound for the KLS Constant” van 140 pagina’s, dat op 1 oktober op arXiv verscheen en op 4 oktober in een herziene versie werd afgerond. Volgens Microsoft verkenden meerdere AI-agents tegelijk varianten van een idee. Na elke ronde bekeek een onderzoeker de tussenresultaten, schrapte zwakke richtingen en gaf de beste door aan de volgende ronde. In totaal ging het om zo’n honderd onderzoekstrajecten.
De AI hielp bij het verkennen van benaderingen, het uitwerken van afleidingen, het opmaken van het manuscript en interne bewijscontroles. De recursieve methode en het afschatten van de fouten rekent Microsoft tot het eigen werk van de onderzoekers. Welke AI-modellen zijn gebruikt, vermeldt de publicatie niet.
Een detail dat opvalt: in een apart spoor kregen “meerdere toonaangevende AI-modellen” ongeveer hetzelfde tokenbudget, maar zonder menselijke sturing. Die pogingen kwamen niet tot een bewijs.
Gecontroleerd door vakgenoten
Bij een wiskundige claim telt vooral wat andere wiskundigen ervan vinden. Volgens Unite.AI publiceerden Bizeul, Klartag en Lehec een eigen bewijs van 32 pagina’s, waarin zij het criterium van Song en Zhang “de cruciale stap” noemen. Er verscheen ook een formalisering in de bewijsassistent Lean 4, KLS500, die dat criterium gebruikt. De auteurs hebben zelf een ingekorte versie van hun bewijs in Lean laten controleren. Die versie publiceren ze na een laatste review.
Wat betekent dit?
AI levert vaker bijdragen aan echte wiskunde. Eerder publiceerde OpenAI 722 wiskundepapers van een intern model en liet Meta zien hoe Muse Spark wiskundigen helpt bij open problemen. Het KLS-bewijs gaat een stap verder. Het betreft een bekend probleem van 31 jaar oud, onafhankelijk nagerekend en deels machinaal geverifieerd.
De les gaat vooral over taakverdeling. Zonder menselijke selectie strandden de modellen. Je ziet dat patroon ook buiten de wiskunde, bijvoorbeeld bij AI-codereviews die bugs in PostgreSQL 19 vonden of toen Claude quantumcircuits met minder gates ontwierp. De machine zoekt breed, de mens beslist wat telt. Voor organisaties die met AI-agents experimenteren is dat een bruikbaar model: laat agents veel varianten proberen, maar zet iemand met vakkennis aan het stuur.
