Matemáticos con agentes de IA demuestran la conjetura KLS de hace 31 años. Los modelos solos, con los mismos tokens, no lo lograron

Microsoft Research anunció el 21 de octubre que su investigador Xinzhi Zhang y el coautor Zhao Song han demostrado la conjetura KLS, planteada en 1995. Para las matemáticas, se cierra un problema de 31 años. Para los equipos de IA, es un relato inusualmente detallado de qué hicieron los agentes y qué hicieron las personas.

Un corte plano basta en cualquier dimensión

La conjetura de Kannan, Lovász y Simonovits trata sobre una amplia clase de distribuciones de probabilidad en alta dimensión, las llamadas distribuciones log-cóncavas. Pregunta si el mejor corte plano de una de esas formas es casi tan bueno como el mejor corte de forma arbitraria. La conjetura afirma que la diferencia está acotada por una constante que no depende del número de dimensiones. En eso se apoya la teoría de los paseos aleatorios con los que los algoritmos muestrean distribuciones.

El mejor resultado conocido, de julio de 2026, todavía permitía que la cota creciera despacio con la dimensión. Los autores primero lo afinaron y, con agentes de IA, recorrieron más de 100 enfoques posibles, muchos con largos cálculos sobre tensores de orden superior. De ahí salió un criterio nuevo. La versión del artículo del 1 de octubre lo aplicó de forma repetida y redujo la dependencia de la dimensión al logaritmo iterado. La versión del 4 de octubre repitió todo el procedimiento, mostró que los pequeños errores no se acumulan sin límite y completó la demostración. Según el blog, la idea de este paso surgió de trabajos anteriores de los autores sobre algoritmos rápidos de programación lineal.

Otros ya han confirmado el resultado. Ese mismo día, un grupo independiente de expertos publicó su propia demostración completa y calificó la primera versión del artículo de Microsoft como «el paso crucial». Una tercera demostración, aparecida también ese día, se basa en una idea muy parecida. Después llegó una formalización en Lean 4 que combina el criterio de la primera versión con otras investigaciones.

El intento de control sin humanos importa más a los equipos de IA que la propia demostración

El blog detalla con precisión el reparto del trabajo. Las herramientas de IA probaron variantes, hicieron derivaciones detalladas, ayudaron a redactar el manuscrito y realizaron comprobaciones internas de la demostración. Las personas marcaron la dirección, eligieron las ideas prometedoras, las ensamblaron en el argumento final y verificaron la demostración. Los agentes trabajaban en paralelo y, tras cada ronda, el investigador descartaba los callejones sin salida y pasaba el mejor resultado intermedio a la siguiente. Hubo unas cien ramas de este tipo.

El dato más valioso es el intento de control. Los autores trataron varias veces de resolver el mismo problema con varios modelos punteros sin guía y con un presupuesto de tokens parecido. No lo consiguieron. Para las empresas que esperan sustituir la investigación por una única ejecución larga de un modelo, es una advertencia útil. Lo que funcionó fue la combinación de búsqueda y criterio humano, que iba apartando a los agentes de los caminos equivocados.

Para las matemáticas, el efecto es directo. Muchos teoremas que hasta ahora solo valían si se suponía cierta la conjetura KLS pasan a valer sin condiciones. Eso refuerza los cimientos de la geometría convexa, la teoría de la probabilidad y la informática teórica.

El experimento de control es, por ahora, una frase en un blog

Microsoft no ha revelado qué modelos participaron en el intento de control, cuántas pruebas hubo ni cuántos tokens se gastaron. La afirmación de que el trabajo fracasó sin humanos es, de momento, el testimonio de los propios autores y no una medición que otros puedan repetir. Lo mismo vale para los «más de 100 enfoques», que describen su propio proceso.

La verificación formal también tiene dos capas. La formalización publicada en Lean 4 combina el criterio de la primera versión con otras investigaciones, así que no es una comprobación automática de esta demostración exacta. Los autores tienen una demostración abreviada verificada en Lean, pero solo la publicarán tras la revisión final. Además, el resultado en sí no aporta un algoritmo de muestreo nuevo. Lo que cambia, sobre todo, es lo que se puede demostrar sobre los que ya existen.

La demostración en Lean y los detalles del intento de control dirán cuán sólido es el argumento

Para los matemáticos, lo decisivo será la demostración abreviada verificada en Lean y su aceptación en la revisión por pares. Tres demostraciones independientes el mismo día son una señal fuerte, pero la revisión dará al resultado su peso definitivo.

Para el mundo de la IA, la cuestión clave es si Microsoft publica los datos del intento de control: los modelos, el número de ejecuciones y el gasto en tokens. Solo entonces se podrá medir con honestidad cuánto trabajo hizo la persona que iba descartando callejones sin salida. También se verá si la búsqueda podada por humanos sirve para otros problemas abiertos o si solo funcionó aquí.

El veredicto de Lilith

Cien agentes buscaban un camino mientras un matemático tachaba los callejones sin salida tras cada ronda. Los modelos sin él recibieron el mismo presupuesto de tokens y no encontraron la demostración, algo que debería leer dos veces cualquier directivo que quiera confiar la investigación a una sola ejecución gigante.