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

Microsoft Research kunngjorde 21. oktober 2026 at Xinzhi Zhang, seniorforsker i gruppen for maskinlæring og optimering, og samarbeidspartneren Zhao Song har bevist Kannan–Lovász–Simonovits-formodningen, et 31 år gammelt problem innen høyddimensjonal geometri og sannsynlighet, ved hjelp av en menneskestyrt, agentbasert KI-forskningsprosess.

Formodningen og den nye grensen

Beviset presenteres i artikkelen på 140 sider En O(1)-grense for KLS-konstanten, ført i pennen av Zhao Song og Xinzhi Zhang. Den ble først sendt inn til arXiv 1. oktober 2026 og revidert 4. oktober 2026, med Zhang som innsender. I sammendraget står det at forfatterne beviser at KLS-konstanten ψ_n er begrenset ovenfra av en universell konstant C, og dermed løser formodningen. De beviser også en universell øvre grense for Poincaré-konstanten til alle isotrope log-konkave sannsynlighetsmål.

Formelt spør formodningen, som ble fremsatt i 1995, om hvert isotrope log-konkave sannsynlighetsmål i et n-dimensjonalt rom har en Cheeger-konstant som er begrenset nedenfra av en universell positiv konstant. Enklere forklart spør den, slik innlegget fra Microsoft Research beskriver det, om det beste snittet langs en linje eller et hyperplan alltid er nesten like effektivt som det beste snittet av en hvilken som helst form for en bred klasse høyddimensjonale sannsynlighetsfordelinger, med en forskjell på høyst en universell konstant, uavhengig av antall dimensjoner. Siden geometrien til slike snitt avgjør hvor raskt tilfeldige vandringer kan utforske en fordeling, står formodningen sentralt i teorien om høyddimensjonal utvalgsmetodikk.

Før dette arbeidet var det beste kjente resultatet den 21 sider lange artikkelen KLS-konstanten er O(log^{1/4} n) av Brayden Letwin, sendt inn 27. juli 2026. Den viste at ψ_n er høyst en konstant ganger log^{1/4} n. Innlegget fra Microsoft Research påpeker at denne grensen likevel økte sakte etter hvert som antallet dimensjoner steg. Det nye arbeidet gir en fast grense som ikke varierer med dimensjonen.

Formodningens betydning var anerkjent lenge før den ble løst. Innlegget viser til at årsrapporten for 2017–18 fra Mathematical Sciences Research Institute kalte KLS et sentralt åpent problem innen høyddimensjonal konveks geometri, at Simons Institute beskrev det som et av de viktigste uløste problemene innen konveks geometri, og at Ronen Eldan påpekte de vidtrekkende implikasjonene i referatene fra den internasjonale matematikerkongressen i 2022.

En menneskestyrt, agentbasert forskningsprosess

Ifølge innlegget begynte forfatterne med å arbeide med å forbedre resultatet fra juli 2026. Gjennom en strukturert, menneskestyrt prosess med KI-agenter utforsket de mer enn 100 mulige tilnærminger, mange av dem med omfattende beregninger ved hjelp av tensorer av høyere orden. De utarbeidet også et nytt matematisk kriterium som ble grunnlaget for det endelige beviset.

Forfatterne oppdaget deretter at kriteriet kunne anvendes rekursivt: Hver forbedrede grense kunne føres tilbake inn i det samme argumentet for å få en enda strammere grense. I versjonen av artikkelen fra 1. oktober 2026 reduserte dette avhengigheten av dimensjonen til den itererte logaritmen, som vokser svært langsomt, men fortsatt øker med dimensjonen. Dermed var formodningen ennå ikke løst. Det siste steget var å gjenta hele den rekursive forbedringen i stedet for å anvende den bare én gang. Innlegget sier at ideen var inspirert av forfatternes tidligere arbeid med raske algoritmer for lineær programmering. Forfatterne beviste at de små feilene som oppstår på hvert trinn, avtar raskt nok til at summen deres forblir begrenset av en universell konstant som ikke avhenger av dimensjonen. Dermed ble beviset fullført i versjonen fra 4. oktober 2026.

Innlegget opplyser at den rekursive metoden, den gjentatte anvendelsen av den og argumentet om begrensede feil er forskernes egne bidrag. KI-verktøy bidro til å utforske mulige tilnærminger, gjennomføre detaljerte utledninger, utarbeide manuskriptet og foreta interne kontroller av beviset. Forskerne fastsatte imidlertid den matematiske retningen, valgte ut de lovende ideene, satte dem sammen til det endelige argumentet og verifiserte beviset. Innlegget beskriver metoden som agentbasert søk med iterativ, menneskeassistert utsiling: Mens flere agenter utforsket ulike varianter av en idé parallelt, gjennomgikk forskeren mellomresultatene, forkastet lite lovende retninger og sendte det mest lovende resultatet videre til neste runde. Omtrent hundre forskningsløp ble utforsket før det avgjørende gjennombruddet kom.

I et separat spor av prosjektet forsøkte forfatterne gjentatte ganger, uten veiledning, å løse det samme problemet med flere ledende KI-modeller og brukte omtrent samme samlede tokenbudsjett som i hovedprosessen. Innlegget opplyser at dette arbeidet ikke nådde målet. Ifølge innlegget var den endelige suksessen avhengig både av KI-systemenes kapasitet og av forskernes matematiske skjønn. Innlegget takker Song for bidragene hans til arbeidet, og Victor Reis og Ishai Menache for diskusjoner gjennom hele prosjektet.

Uavhengige bevis og maskinverifisering

Den 4. oktober 2026, samme dag som det fullstendige beviset ble lagt ut, publiserte Pierre Bizeul, Boaz Klartag og Joseph Lehec et 32-siders bevis de hadde utviklet parallelt, med tittelen «Et bevis for Kannan–Lovász–Simonovits-formodningen». Artikkelens sammendrag fastslår at «det avgjørende steget i beviset er det helt nylige kriteriet fra Song og Zhang, som involverer høyereordensderiverte av tilt-gjennomsnitt», og kommentarene på arXiv opplyser at artikkelen inneholder et avsnitt som beskriver bruk av KI. Sammendraget setter KLS på linje med Bourgains snittproblem og variansformodningen som drivkrefter bak den matematiske utviklingen innen høydimensjonal geometri de siste tiårene.

Krishnakumar Balasubramanian og Shiva Kasiviswanathan publiserte et separat bevis, En dimensjonsuavhengig øvre grense for Poincaré-konstanten til isotrope log-konkave mål, som først ble sendt inn 6. oktober 2026 og revidert 8. oktober 2026. Sammendraget beskriver et deterministisk variasjonsbevis med en eksplisitt øvre grense på 25 for Poincaré-konstanten til ethvert isotropt log-konkavt sannsynlighetsmål.

Deretter fulgte en Lean 4-formalisering kalt KLS500, som formaliserer en dimensjonsuavhengig Poincaré-konstant på høyst 500 for enhver isotrop log-konkav sannsynlighetsfordeling. Ifølge repositoriet bygger utviklingen først og fremst på kumulant- og suspensjonstilnærmingen til Bizeul, Klartag og Lehec, og innlemmer tilt–spektralkriteriet til Song og Zhang. Verifikasjonen bygde opp 1 710 matematiske moduler på nytt, med kjernetillitsnivå null. Lean-verifikasjonen besto også for den nøyaktige formuleringen av KLS-formodningen som OpenAI hadde definert, med den universelle Poincaré-konstanten 500. Prosjektet er lisensiert under Apache 2.0.

Innlegget fra Microsoft Research beskriver uavhengige bevis som en av matematikkens sterkeste former for validering, fordi de viser at et resultat ikke bygger på én enkelt resonnementskjede. Nå som formodningen er løst, kan resultater som tidligere bygde på den som en antakelse, formuleres uten forbehold, står det i innlegget. Forfatterne har forkortet beviset sitt og verifisert det forenklede argumentet i Lean, og innlegget opplyser at de planlegger å publisere begge deler etter den endelige gjennomgangen.