El 21 de octubre, Microsoft Research afirmó que Xinzhi Zhang y Zhao Song habían demostrado la conjetura de Kannan–Lovász–Simonovits, un problema matemático planteado en 1995. En el anuncio de Microsoft Research, la empresa señala que el resultado surgió de un flujo de agentes dirigido por humanos, y no de una ejecución de modelo totalmente autónoma.
Microsoft afirma que los sistemas de IA exploraron más de 100 enfoques candidatos, mientras los investigadores eligieron qué ramas seguir, descartaron rutas débiles y comprobaron las matemáticas restantes. La empresa también indica que los intentos sin supervisión con varios modelos líderes y aproximadamente el mismo presupuesto total de tokens no resolvieron el problema.
La publicación indica que las herramientas se utilizaron más allá de la generación de ideas, incluidas derivaciones, la redacción del artículo y comprobaciones internas de la demostración. Microsoft añade que ya se ha publicado una formalización en Lean 4, y que se prevé una versión más corta verificada por máquina tras la revisión final.
Aún conviene interpretarlo como un resultado importante en prepublicación, no como un hito consolidado en los libros de texto. Informes independientes señalaron que otros grupos publicaron demostraciones paralelas en pocos días, lo que aporta confianza, pero el trabajo todavía no ha pasado por revisión de una revista.