Microsoftforskare och samarbetspartner bevisar 31 år gammal KLS-förmodan

Microsoft Research meddelade den 21 oktober 2026 att Xinzhi Zhang, seniorforskare i organisationens grupp för maskininlärning och optimering, och samarbetspartnern Zhao Song har bevisat Kannan–Lovász–Simonovits-förmodan, ett 31 år gammalt problem inom högdimensionell geometri och sannolikhetsteori, med hjälp av en människostyrd AI-forskningsprocess med agenter.

Förmodan och den nya gränsen

Beviset presenteras i den 140 sidor långa artikeln En O(1)-gräns för KLS-konstanten, som anges vara författad av Zhao Song och Xinzhi Zhang. Den skickades först in till arXiv den 1 oktober 2026 och reviderades den 4 oktober 2026, med Zhang som insändande författare. I sammanfattningen står det att författarna bevisar att KLS-konstanten ψ_n är begränsad uppåt av en universell konstant C, vilket löser förmodan, och att de också bevisar en universell gräns för Poincarékonstanten hos varje isotropiskt log-konkavt sannolikhetsmått.

Formellt frågar förmodan, som lades fram 1995, om varje isotropiskt log-konkavt sannolikhetsmått på ett n-dimensionellt rum har en Cheegerkonstant som är begränsad nedåt av en universell positiv konstant. Enklare uttryckt frågar den, enligt inlägget från Microsoft Research, om det för en bred klass av högdimensionella sannolikhetsfördelningar alltid är nästan lika effektivt att skära genom fördelningen med ett plan eller hyperplan som med den bästa möjliga skärningen av vilken form som helst, där skillnaden mellan dem inte överstiger en universell konstant oavsett antalet dimensioner. Eftersom skärningarnas geometri avgör hur snabbt slumpvandringar kan utforska en fördelning spelar förmodan en central roll inom teorin för högdimensionell sampling.

Före detta arbete var det bästa kända resultatet den 21 sidor långa artikeln KLS-konstanten är O(log^{1/4} n) av Brayden Letwin, som skickades in den 27 juli 2026. Den visade att ψ_n är högst en konstant gånger log^{1/4} n, en gräns som, enligt inlägget från Microsoft Research, fortfarande ökade långsamt när antalet dimensioner blev större. Det nya resultatet gäller med en fast gräns som inte varierar med dimensionen.

Förmodans betydelse hade uppmärksammats långt innan den löstes. I inlägget noteras att Mathematical Sciences Research Institutes årsrapport för 2017–18 kallade KLS ett centralt olöst problem inom högdimensionell konvex geometri, att Simons Institute beskrev det som ett av de viktigaste olösta problemen inom konvex geometri och att Ronen Eldan framhöll dess breda konsekvenser i konferensbidragen från 2022 års International Congress of Mathematicians.

En människostyrd agentbaserad forskningsprocess

Enligt inlägget började författarna med att försöka förbättra resultatet från juli 2026. Genom en strukturerad, människostyrd process med AI-agenter undersökte de mer än 100 möjliga angreppssätt, varav många innefattade långa beräkningar med tensorer av högre ordning, och tog fram ett nytt matematiskt kriterium som blev grunden för det slutliga beviset.

Författarna upptäckte sedan att kriteriet kunde tillämpas rekursivt: varje förbättrad gräns fördes tillbaka in i samma argument för att ge en ännu snävare gräns. I artikelversionen från den 1 oktober 2026 minskade detta beroendet av dimensionen till den itererade logaritmen, som växer ytterst långsamt men ändå ökar med dimensionen och därför ännu inte löste förmodan. Det sista steget var att upprepa hela den rekursiva förfiningen i stället för att tillämpa den bara en gång. Enligt inlägget inspirerades idén av författarnas tidigare arbete med snabba algoritmer för linjär programmering. Författarna bevisade att de små fel som uppstår i varje steg avtar tillräckligt snabbt för att deras sammanlagda storlek ska förbli begränsad av en universell konstant som är oberoende av dimensionen. Därmed blev beviset fullständigt i artikelversionen från den 4 oktober 2026.

I inlägget står det att den rekursiva metoden, dess upprepade tillämpning och argumentet om begränsade fel är forskarnas egna bidrag. AI-verktyg hjälpte till att utforska möjliga angreppssätt, genomföra detaljerade härledningar, förbereda manuskriptet och utföra interna kontroller av beviset. Forskarna bestämde däremot den matematiska inriktningen, valde ut de lovande idéerna, fogade samman dem till det slutliga argumentet och verifierade beviset. Inlägget beskriver metoden som agentsökning med iterativ, människostödd gallring: medan flera agenter utforskade olika varianter av en idé parallellt granskade forskaren delresultaten, valde bort mindre lovande spår och förde det mest lovande resultatet vidare till nästa omgång. Ungefär hundra forskningsspår undersöktes innan det avgörande genombrottet kom.

I ett separat spår inom projektet gjorde författarna upprepade, ostyrda försök att lösa samma problem med flera ledande AI-modeller och använde ungefär samma sammanlagda tokenbudget som i huvudprocessen. Enligt inlägget nådde försöken inte målet. Framgången till slut byggde, enligt inlägget, på både AI-systemens förmåga och forskarnas matematiska omdöme. I inlägget tackas Song för sina bidrag till arbetet samt Victor Reis och Ishai Menache för diskussioner under projektets gång.

Oberoende bevis och maskinverifiering

Den 4 oktober 2026, samma dag som det fullständiga beviset lades ut, publicerade Pierre Bizeul, Boaz Klartag och Joseph Lehec ett parallellt framtaget bevis på 32 sidor med titeln En presentation av ett bevis för Kannan–Lovász–Simonovits-förmodan. I artikelns sammanfattning står det att ”det avgörande steget i beviset är det mycket nyligen framlagda kriteriet från Song och Zhang, som involverar derivator av högre ordning av tiltade medelvärden”, och i kommentarerna på arXiv nämns att artikeln innehåller ett stycke som beskriver användningen av AI. I sammanfattningen lyfts KLS fram tillsammans med Bourgains skärningsproblem och variansförmodan som drivkrafter bakom den matematiska utvecklingen inom högdimensionell geometri under de senaste decennierna.

Krishnakumar Balasubramanian och Shiva Kasiviswanathan lade upp ett separat bevis, En dimensionsoberoende övre gräns för Poincaré-konstanten hos isotropa logkonkava mått, som först skickades in den 6 oktober 2026 och reviderades den 8 oktober 2026. I sammanfattningen beskrivs ett deterministiskt variationsbevis med en explicit övre gräns på 25 för Poincaré-konstanten hos varje isotrop logkonkav sannolikhetsfördelning.

Därefter följde en formalisering i Lean 4 med namnet KLS500, som formaliserar att Poincaré-konstanten är högst 500, oberoende av dimensionen, för varje isotrop logkonkav sannolikhetsfördelning. Enligt kodförrådet bygger utvecklingen främst på Bizeuls, Klartags och Lehecs kumulant- och suspensionsansats, med Song och Zhangs tiltningsspektralkriterium som en del av den. Verifieringen byggde om 1 710 matematiska moduler med kärnans tillitsnivå noll. Lean-verifieringen godkändes också för den exakta formuleringen av KLS-förmodan som OpenAI definierat, med den universella Poincaré-konstanten 500. Projektet är licensierat under Apache 2.0.

Inlägget från Microsoft Research beskriver oberoende bevis som en av matematikens starkaste former av validering, eftersom de visar att ett resultat inte vilar på en enda beviskedja. Nu när förmodan har lösts kan resultat som tidigare byggde på den som ett antagande, enligt inlägget, i stället formuleras utan förbehåll. Författarna har kortat sitt bevis och verifierat det förenklade resonemanget i Lean. Inlägget uppger att de planerar att publicera båda efter den slutliga granskningen.