Em 21 de outubro, a Microsoft Research afirmou que Xinzhi Zhang e Zhao Song haviam provado a conjectura de Kannan–Lovász–Simonovits, um problema matemático proposto em 1995. No anúncio da Microsoft Research, a empresa afirma que o resultado veio de um fluxo de agentes dirigido por humanos, e não de uma execução de modelo totalmente autônoma.
A Microsoft afirma que sistemas de IA exploraram mais de 100 abordagens candidatas, enquanto os pesquisadores escolheram quais caminhos seguir, eliminaram rotas fracas e verificaram a matemática restante. A empresa também diz que tentativas sem orientação com vários modelos líderes e aproximadamente o mesmo orçamento total de tokens não resolveram o problema.
A publicação afirma que as ferramentas foram usadas além da geração de ideias, incluindo derivações, redação do artigo e verificações internas da prova. A Microsoft acrescenta que uma formalização em Lean 4 já foi lançada, com uma versão mais curta verificada por máquina planejada após a revisão final.
Ainda é melhor interpretar o resultado como um preprint importante, não como um marco consolidado em livros didáticos. Relatos independentes disseram que outros grupos publicaram provas paralelas em poucos dias, o que aumenta a confiança, mas o trabalho ainda não passou por revisão de periódico.