Pesquisador da Microsoft e colaborador provam conjectura de KLS formulada há 31 anos

A Microsoft Research anunciou, em 21 de outubro de 2026, que Xinzhi Zhang, pesquisador sênior de seu grupo de Aprendizado de Máquina e Otimização, e seu colaborador Zhao Song provaram a conjectura de Kannan–Lovász–Simonovits, um problema de 31 anos em geometria e probabilidade de alta dimensão, por meio de um processo de pesquisa com IA agêntica dirigido por humanos.

A conjectura e o novo limite

A demonstração consta no artigo de 140 páginas Um limite O(1) para a constante de KLS, de Zhao Song e Xinzhi Zhang, enviado pela primeira vez ao arXiv em 1º de outubro de 2026 e revisado em 4 de outubro de 2026, com Zhang como autor responsável pelo envio. O resumo afirma que os autores provam que a constante de KLS ψ_n é limitada superiormente por uma constante universal C, resolvendo a conjectura, e que também provam um limite universal para a constante de Poincaré de toda medida de probabilidade isotrópica log-côncava.

Formalmente, a conjectura, proposta em 1995, pergunta se toda medida de probabilidade isotrópica log-côncava em um espaço n-dimensional tem uma constante de Cheeger limitada inferiormente por uma constante positiva universal. Em termos mais simples, como explica a publicação da Microsoft Research, ela pergunta se, para uma ampla classe de distribuições de probabilidade de alta dimensão, o melhor corte plano ou por hiperplano é sempre quase tão eficaz quanto o melhor corte de qualquer formato, com uma diferença entre eles que não ultrapassa uma constante universal, independentemente do número de dimensões. Como a geometria desses cortes determina a rapidez com que caminhadas aleatórias podem explorar uma distribuição, a conjectura ocupa um lugar central na teoria da amostragem em alta dimensão.

Antes deste trabalho, o melhor resultado conhecido era o artigo de 21 páginas A constante de KLS é O(log^{1/4} n), de Brayden Letwin, enviado em 27 de julho de 2026. Ele estabeleceu que ψ_n é, no máximo, igual a uma constante multiplicada por log^{1/4} n; como observa a publicação da Microsoft Research, esse limite ainda aumentava lentamente à medida que o número de dimensões crescia. O novo trabalho estabelece um limite fixo, que não varia com a dimensão.

A importância da conjectura já era reconhecida muito antes de ela ser resolvida. A publicação registra que o relatório anual de 2017–18 do Mathematical Sciences Research Institute chamou a KLS de um problema em aberto central na geometria convexa de alta dimensão; que o Simons Institute a descreveu como um dos problemas em aberto mais importantes da geometria convexa; e que Ronen Eldan destacou suas amplas implicações nos anais do Congresso Internacional de Matemáticos de 2022.

Um processo de pesquisa agêntica dirigido por humanos

Segundo a publicação, os autores começaram tentando aprimorar o resultado de julho de 2026. Por meio de um processo estruturado e dirigido por humanos, com agentes de IA, exploraram mais de 100 abordagens possíveis, muitas delas envolvendo cálculos extensos com tensores de ordem superior, e produziram um novo critério matemático que se tornou a base da demonstração final.

Em seguida, os autores descobriram que era possível aplicar o critério recursivamente, realimentando o mesmo argumento com cada limite aprimorado para obter outro ainda mais restrito. Na versão do artigo de 1º de outubro de 2026, isso reduziu a dependência da dimensão ao logaritmo iterado, que cresce muito lentamente, mas ainda aumenta com a dimensão e, portanto, não resolvia a conjectura. A etapa final consistiu em repetir todo o refinamento recursivo, em vez de aplicá-lo apenas uma vez; segundo a publicação, a ideia foi inspirada no trabalho anterior dos autores sobre algoritmos rápidos para programação linear. Os autores provaram que os pequenos erros introduzidos em cada etapa diminuem com rapidez suficiente para que sua soma permaneça limitada por uma constante universal independente da dimensão, concluindo a demonstração na versão de 4 de outubro de 2026.

A publicação afirma que o método recursivo, sua aplicação repetida e o argumento de que os erros permanecem limitados são contribuições originais dos pesquisadores. As ferramentas de IA ajudaram a explorar abordagens possíveis, realizar derivações detalhadas, preparar o manuscrito e fazer verificações internas da demonstração; os pesquisadores, por sua vez, definiram a direção matemática, selecionaram as ideias promissoras, reuniram-nas no argumento final e verificaram a demonstração. A publicação descreve o método como uma busca agêntica com seleção iterativa assistida por humanos: enquanto vários agentes exploravam, em paralelo, variações de uma ideia, o pesquisador examinava os resultados intermediários, descartava as direções pouco promissoras e encaminhava o resultado mais promissor para a rodada seguinte. Foram exploradas cerca de cem linhas de pesquisa antes de surgir a descoberta decisiva.

Em uma linha de trabalho separada do projeto, os autores fizeram várias tentativas sem orientação para resolver o mesmo problema usando diversos modelos de IA de ponta e aproximadamente o mesmo orçamento total de tokens que no processo principal; a publicação relata que esse esforço não alcançou o objetivo. Segundo a publicação, o sucesso final dependeu tanto dos recursos dos sistemas de IA quanto do discernimento matemático dos pesquisadores. A publicação agradece a Song por suas contribuições ao trabalho e a Victor Reis e Ishai Menache pelas discussões ao longo do projeto.

Demonstrações independentes e verificação por máquina

Em 4 de outubro de 2026, no mesmo dia em que a prova completa foi publicada, Pierre Bizeul, Boaz Klartag e Joseph Lehec publicaram uma prova de 32 páginas, desenvolvida em paralelo, intitulada Apresentação de uma prova da conjectura de Kannan-Lovász-Simonovits. O resumo do artigo afirma que «o passo crucial da prova é o critério muito recente de Song e Zhang, que envolve derivadas de alta ordem das médias de inclinação», e os comentários no arXiv observam que o artigo contém um parágrafo que descreve o uso de IA. O resumo situa a conjectura KLS ao lado do problema do corte de Bourgain e da conjectura da variância, apontando-os como forças motrizes dos avanços matemáticos em geometria de altas dimensões nas últimas décadas.

Krishnakumar Balasubramanian e Shiva Kasiviswanathan publicaram uma prova separada, Um limite independente da dimensão para a constante de Poincaré de medidas isotrópicas log-côncavas, submetida pela primeira vez em 6 de outubro de 2026 e revisada em 8 de outubro de 2026. O resumo descreve uma prova variacional determinística com um limite explícito de 25 para a constante de Poincaré de qualquer medida de probabilidade isotrópica log-côncava.

Em seguida, surgiu uma formalização em Lean 4 chamada KLS500, que formaliza uma constante de Poincaré independente da dimensão e igual a, no máximo, 500 para toda distribuição de probabilidade isotrópica log-côncava. Segundo o repositório, o desenvolvimento se baseia principalmente na abordagem por cumulantes e suspensão de Bizeul, Klartag e Lehec, incorporando o critério de tilt-espectral de Song e Zhang; sua verificação reconstruiu 1.710 módulos matemáticos com nível zero de confiança no kernel. A verificação em Lean também foi aprovada para a formulação exata da conjectura KLS definida pela OpenAI, usando a constante universal de Poincaré 500. O projeto está licenciado sob Apache 2.0.

A publicação da Microsoft Research descreve provas independentes como uma das formas mais fortes de validação em matemática, pois demonstram que um resultado não depende de uma única linha de raciocínio. Com a conjectura resolvida, afirma a publicação, resultados que antes dependiam dela como hipótese podem agora ser enunciados sem condições. Os autores encurtaram a prova e verificaram a argumentação simplificada em Lean; a publicação informa que planejam divulgar ambas após a revisão final.