Badacz Microsoftu i jego współpracownik dowodzą 31-letniej hipotezy KLS

Microsoft Research ogłosił 21 października 2026 roku, że Xinzhi Zhang, starszy badacz w należącej do firmy grupie zajmującej się uczeniem maszynowym i optymalizacją, oraz współpracujący z nim Zhao Song udowodnili hipotezę Kannan–Lovásza–Simonovitsa, problem z zakresu geometrii wysokowymiarowej i teorii prawdopodobieństwa, postawiony 31 lat temu. Wykorzystali przy tym kierowany przez człowieka, agentowy proces badawczy oparty na sztucznej inteligencji.

Hipoteza i nowa granica

Dowód przedstawiono w 140-stronicowej pracy O(1)-granica dla stałej KLS, której autorami są Zhao Song i Xinzhi Zhang. Pracę po raz pierwszy przesłano do arXiv 1 października 2026 roku, a poprawioną wersję opublikowano 4 października 2026 roku; Zhang figuruje jako autor zgłaszający. W streszczeniu podano, że autorzy dowodzą, iż stała KLS ψ_n jest ograniczona z góry przez stałą uniwersalną C, co rozstrzyga hipotezę. Dowodzą również istnienia uniwersalnego ograniczenia stałej Poincarégo dla każdej izotropowej miary probabilistycznej o log-wklęsłej gęstości.

W ujęciu formalnym hipoteza, sformułowana w 1995 roku, pyta, czy każda izotropowa miara probabilistyczna o log-wklęsłej gęstości w przestrzeni n-wymiarowej ma stałą Cheegera ograniczoną od dołu przez pewną uniwersalną dodatnią stałą. Mówiąc prościej, jak wyjaśniono we wpisie Microsoft Research, chodzi o to, czy dla szerokiej klasy wysokowymiarowych rozkładów prawdopodobieństwa najlepsze cięcie płaskie lub hiperpłaszczyzną jest zawsze niemal równie skuteczne jak najlepsze cięcie o dowolnym kształcie, a różnica między nimi nie przekracza pewnej uniwersalnej stałej, niezależnie od liczby wymiarów. Ponieważ geometria tych cięć określa, jak szybko błądzenia losowe mogą eksplorować rozkład, hipoteza odgrywa kluczową rolę w teorii próbkowania wysokowymiarowego.

Przed tą pracą najlepszym znanym wynikiem była 21-stronicowa praca Stała KLS jest rzędu O(log^{1/4} n) autorstwa Braydena Letwina, przesłana 27 lipca 2026 roku. Wykazano w niej, że ψ_n jest nie większa niż stała pomnożona przez log^{1/4} n. Jak zauważono we wpisie Microsoft Research, ograniczenie to nadal powoli rosło wraz ze wzrostem liczby wymiarów. Nowy wynik zapewnia stałe ograniczenie, które nie zależy od wymiaru.

Znaczenie hipotezy dostrzegano na długo przed jej rozstrzygnięciem. We wpisie odnotowano, że roczne sprawozdanie Mathematical Sciences Research Institute za lata 2017–18 określało KLS jako centralny nierozwiązany problem w wysokowymiarowej geometrii wypukłej, Simons Institute uznał ją za jeden z najważniejszych otwartych problemów geometrii wypukłej, a Ronen Eldan zwrócił uwagę na jej szerokie implikacje w materiałach z Międzynarodowego Kongresu Matematyków z 2022 roku.

Kierowany przez człowieka, agentowy proces badawczy

Według wpisu autorzy rozpoczęli prace od próby ulepszenia wyniku z lipca 2026 roku. W ramach uporządkowanego procesu kierowanego przez człowieka, z udziałem agentów AI, zbadali ponad 100 możliwych podejść, z których wiele wymagało długich obliczeń z użyciem tensorów wyższych rzędów. Opracowali też nowe kryterium matematyczne, które stało się podstawą ostatecznego dowodu.

Autorzy odkryli następnie, że kryterium można stosować rekurencyjnie: każde uzyskane lepsze ograniczenie można wprowadzić z powrotem do tego samego argumentu, by otrzymać jeszcze ciaśniejsze. W wersji pracy z 1 października 2026 roku pozwoliło to ograniczyć zależność od wymiaru do logarytmu iterowanego, który rośnie niezwykle powoli, ale nadal zwiększa się wraz z wymiarem, więc hipoteza nie została jeszcze rozstrzygnięta. Ostatnim krokiem było powtórzenie całego procesu rekurencyjnego udoskonalania zamiast zastosowania go tylko raz. Jak podano we wpisie, pomysł ten zainspirowały wcześniejsze prace autorów nad szybkimi algorytmami programowania liniowego. Autorzy dowiedli, że niewielkie błędy wprowadzane na każdym etapie maleją na tyle szybko, iż ich suma pozostaje ograniczona przez stałą uniwersalną niezależną od wymiaru. W ten sposób w wersji z 4 października 2026 roku zakończyli dowód.

We wpisie podano, że metoda rekurencyjna, jej wielokrotne zastosowanie oraz argument dotyczący ograniczonego błędu stanowią oryginalny wkład badaczy. Narzędzia AI pomogły w eksplorowaniu możliwych podejść, przeprowadzaniu szczegółowych wyprowadzeń, przygotowaniu manuskryptu i wewnętrznej weryfikacji dowodu. Badacze wyznaczali jednak kierunek matematyczny, wybierali obiecujące pomysły, łączyli je w końcowy argument i sprawdzali dowód. We wpisie opisano tę metodę jako agentowe poszukiwanie z iteracyjnym odrzucaniem wariantów przy wsparciu człowieka: gdy wiele agentów równolegle badało różne wersje pomysłu, badacz analizował wyniki pośrednie, odrzucał nieobiecujące kierunki i przekazywał najbardziej obiecujący rezultat do następnej rundy. Zanim pojawił się kluczowy przełom, zbadano około stu ścieżek badawczych.

W osobnym nurcie projektu autorzy wielokrotnie próbowali rozwiązać ten sam problem bez wskazówek, korzystając z kilku wiodących modeli AI i przeznaczając na to mniej więcej taki sam łączny budżet tokenów jak w głównym procesie. We wpisie podano, że te próby nie doprowadziły do celu. Jak stwierdzono we wpisie, ostateczny sukces zależał zarówno od możliwości systemów AI, jak i od matematycznego osądu badaczy. We wpisie podziękowano Songowi za jego wkład w pracę, a także Victorowi Reisowi i Ishaiowi Menache za rozmowy prowadzone w trakcie projektu.

Niezależne dowody i weryfikacja maszynowa

4 października 2026 roku, tego samego dnia, w którym opublikowano pełny dowód, Pierre Bizeul, Boaz Klartag i Joseph Lehec opublikowali opracowany równolegle 32-stronicowy dowód zatytułowany „Przedstawiamy dowód hipotezy Kannan–Lovász–Simonovits”. W abstrakcie artykułu stwierdzono, że „kluczowym krokiem w dowodzie jest bardzo niedawne kryterium Song i Zhanga, wykorzystujące wysokiego rzędu pochodne średnich po przechyleniu”, a w komentarzach na arXiv zaznaczono, że artykuł zawiera akapit opisujący wykorzystanie AI. W abstrakcie hipotezę KLS wymieniono obok problemu przekroju Bourgaina i hipotezy wariancji jako siły napędowe rozwoju matematyki w geometrii wysokowymiarowej w ostatnich dekadach.

Krishnakumar Balasubramanian i Shiva Kasiviswanathan opublikowali osobny dowód zatytułowany Oszacowanie niezależne od wymiaru stałej Poincarégo dla izotropowych miar log-wklęsłych. Artykuł został po raz pierwszy zgłoszony 6 października 2026 roku, a następnie zaktualizowany 8 października 2026 roku. W abstrakcie opisano deterministyczny dowód wariacyjny z jawnym ograniczeniem stałej Poincarégo do wartości 25 dla dowolnej izotropowej, log-wklęsłej miary probabilistycznej.

Następnie powstała formalizacja w Lean 4 o nazwie KLS500, która formalizuje niezależne od wymiaru ograniczenie stałej Poincarégo do wartości nie większej niż 500 dla każdej izotropowej, log-wklęsłej miary probabilistycznej. Według repozytorium projekt opiera się przede wszystkim na podejściu wykorzystującym kumulanty i zawieszenie, opracowanym przez Bizeula, Klartaga i Leheca, oraz uwzględnia kryterium przechyleniowo-spektralne Song i Zhanga. W ramach weryfikacji ponownie zbudowano 1710 modułów matematycznych przy zerowym poziomie zaufania do jądra. W Lean pomyślnie zweryfikowano także dokładne sformułowanie hipotezy KLS zdefiniowane przez OpenAI, przyjmujące uniwersalną stałą Poincarégo równą 500. Projekt jest udostępniany na licencji Apache 2.0.

Wpis Microsoft Research przedstawia niezależne dowody jako jedną z najmocniejszych form weryfikacji w matematyce, ponieważ pokazują one, że wynik nie opiera się na jednym ciągu rozumowania. Jak czytamy we wpisie, po rozstrzygnięciu hipotezy wyniki, które wcześniej zakładały jej prawdziwość, można teraz formułować bezwarunkowo. Autorzy skrócili swój dowód i zweryfikowali jego uproszczoną wersję w Lean. Wpis informuje, że po końcowej weryfikacji planują opublikować oba.