Microsoft-forsker og samarbejdspartner beviser 31 år gammel KLS-formodning

Microsoft Research meddelte den 21. oktober 2026, at Xinzhi Zhang, seniorforsker i virksomhedens gruppe for maskinlæring og optimering, og samarbejdspartneren Zhao Song har bevist Kannan–Lovász–Simonovits-formodningen, et 31 år gammelt problem inden for højdimensionel geometri og sandsynlighedsteori, ved hjælp af en menneskestyret, agentbaseret AI-forskningsproces.

Formodningen og den nye øvre grænse

Beviset fremlægges i artiklen på 140 sider, En O(1)-grænse for KLS-konstanten, som er krediteret Zhao Song og Xinzhi Zhang. Den blev første gang indsendt til arXiv den 1. oktober 2026 og revideret den 4. oktober 2026, med Zhang som indsendende forfatter. I resuméet står der, at forfatterne beviser, at KLS-konstanten ψ_n er begrænset opad af en universel konstant C, hvilket løser formodningen, og at de også beviser en universel grænse for Poincaré-konstanten for ethvert isotropisk log-konkavt sandsynlighedsmål.

Formelt spørger formodningen, der blev fremsat i 1995, om ethvert isotropisk log-konkavt sandsynlighedsmål i et n-dimensionalt rum har en Cheeger-konstant, der er begrænset nedefra af en universel positiv konstant. Med enklere ord spørger opslaget fra Microsoft Research, om det bedste plane snit eller hyperplansnit for en bred klasse af højdimensionelle sandsynlighedsfordelinger altid er næsten lige så effektivt som det bedste snit af enhver form, således at forskellen mellem de to højst er en universel konstant, uanset antallet af dimensioner. Da snittenes geometri afgør, hvor hurtigt tilfældige vandringer kan udforske en fordeling, spiller formodningen en central rolle i teorien om højdimensionel sampling.

Før dette arbejde var det bedste kendte resultat den 21 sider lange artikel KLS-konstanten er O(log^{1/4} n) af Brayden Letwin, indsendt den 27. juli 2026. Den viste, at ψ_n højst er en konstant gange log^{1/4} n, en grænse, der ifølge opslaget fra Microsoft Research stadig voksede langsomt, efterhånden som antallet af dimensioner steg. Det nye resultat gælder med en fast grænse, der ikke varierer med dimensionen.

Formodningens betydning blev anerkendt længe før den blev løst. Opslaget fortæller, at årsrapporten for 2017–18 fra Mathematical Sciences Research Institute kaldte KLS et centralt uløst problem inden for højdimensionel konveks geometri, at Simons Institute beskrev den som et af de vigtigste uløste problemer inden for konveks geometri, og at Ronen Eldan fremhævede dens vidtrækkende implikationer i beretningen fra den internationale matematikerkongres i 2022.

En menneskestyret, agentbaseret forskningsproces

Ifølge opslaget begyndte forfatterne med at forsøge at forbedre resultatet fra juli 2026. Gennem en struktureret, menneskestyret proces med AI-agenter undersøgte de mere end 100 mulige tilgange, hvoraf mange indebar omfattende beregninger med tensorer af højere orden, og udviklede et nyt matematisk kriterium, som blev grundlaget for det endelige bevis.

Forfatterne opdagede derefter, at kriteriet kunne anvendes rekursivt: Hver forbedret grænse blev ført tilbage ind i det samme argument for at frembringe en endnu strammere grænse. I versionen af artiklen fra den 1. oktober 2026 reducerede dette dimensionsafhængigheden til den itererede logaritme, som vokser ekstremt langsomt, men stadig vokser med dimensionen, og derfor løste resultatet endnu ikke formodningen. Det sidste skridt var at gentage hele den rekursive forfining i stedet for kun at anvende den én gang, en idé, som ifølge opslaget var inspireret af forfatternes tidligere arbejde med hurtige algoritmer til lineær programmering. Forfatterne beviste, at de små fejl, der opstår på hvert trin, aftager hurtigt nok til, at deres samlede størrelse forbliver begrænset af en universel konstant, der er uafhængig af dimensionen. Dermed blev beviset fuldført i versionen fra den 4. oktober 2026.

Opslaget fastslår, at den rekursive metode, dens gentagne anvendelse og argumentet om begrænsede fejl er forskernes egne bidrag. AI-værktøjer hjalp med at udforske mulige tilgange, gennemføre detaljerede udledninger, udarbejde manuskriptet og foretage interne kontroltjek af beviset, mens forskerne fastlagde den matematiske retning, udvalgte de lovende idéer, samlede dem i det endelige argument og verificerede beviset. Opslaget beskriver metoden som agentsøgning med iterativ, menneskeassisteret frasortering: Mens flere agenter udforskede variationer af en idé parallelt, gennemgik forskeren de mellemliggende resultater, frasorterede de mindre lovende retninger og sendte det mest lovende resultat videre til næste runde. Omkring 100 forskningsforløb blev udforsket, før det afgørende gennembrud kom.

I et separat spor af projektet gjorde forfatterne gentagne, uvejledte forsøg på at løse det samme problem med flere førende AI-modeller og brugte omtrent det samme samlede tokenbudget som i hovedforløbet. Opslaget fortæller, at disse forsøg ikke nåede målet. Ifølge opslaget afhang den endelige succes både af AI-systemernes kapacitet og af forskernes matematiske dømmekraft. Opslaget takker Song for hans bidrag til arbejdet samt Victor Reis og Ishai Menache for deres drøftelser undervejs i projektet.

Uafhængige beviser og maskinel verifikation

Den 4. oktober 2026, samme dag som det fuldstændige bevis blev offentliggjort, offentliggjorde Pierre Bizeul, Boaz Klartag og Joseph Lehec et sideløbende udviklet bevis på 32 sider med titlen Præsentation af et bevis for Kannan-Lovász-Simonovits-formodningen. Artiklen anfører i sit abstract, at »det afgørende skridt i beviset er det helt nye kriterium fra Song og Zhang, der omfatter højereordens afledte af tilt-gennemsnit«, og i kommentarerne på arXiv bemærkes det, at artiklen indeholder et afsnit, der beskriver brugen af AI. Abstractet fremhæver KLS sammen med Bourgains snitproblem og variansformodningen som drivkræfter bag den matematiske udvikling inden for højdimensionel geometri i de seneste årtier.

Krishnakumar Balasubramanian og Shiva Kasiviswanathan offentliggjorde et separat bevis med titlen En dimensionsuafhængig grænse for Poincaré-konstanten for isotrope log-konkave mål, som først blev indsendt den 6. oktober 2026 og revideret den 8. oktober 2026. I abstractet beskrives et deterministisk variationsbevis med en eksplicit øvre grænse på 25 for Poincaré-konstanten for ethvert isotropt log-konkavt sandsynlighedsmål.

Derefter fulgte en Lean 4-formalisering ved navn KLS500, som formaliserer en dimensionsuafhængig Poincaré-konstant på højst 500 for enhver isotrop log-konkav sandsynlighedsfordeling. Ifølge arkivet bygger udviklingen hovedsageligt på Bizeul, Klartag og Lehecs kumulant- og suspensionsmetode, som kombineres med tilt-spektralkriteriet fra Song og Zhang, og verificeringen genopbyggede 1.710 matematiske moduler på kernens tillidsniveau nul. Lean-verificeringen bestod også for den præcise formulering af KLS-formodningen, som OpenAI havde defineret, med den universelle Poincaré-konstant 500. Projektet er udgivet under Apache 2.0-licensen.

Indlægget fra Microsoft Research beskriver uafhængige beviser som en af matematikkens stærkeste former for validering, fordi de viser, at et resultat ikke hviler på én enkelt ræsonnementskæde. Nu hvor formodningen er løst, kan resultater, der tidligere byggede på den som en antagelse, ifølge indlægget formuleres ubetinget. Forfatterne har forkortet deres bevis og verificeret den strømlinede argumentation i Lean, og indlægget oplyser, at de planlægger at offentliggøre begge dele efter den endelige gennemgang.