Google DeepMind presentó AlphaProof Nexus, un framework que combina generación de demostraciones con modelos de lenguaje y verificación automática para atacar problemas matemáticos abiertos que llevan décadas sin respuesta.

Según la información de The Decoder, el sistema resolvió de forma autónoma 9 de 353 problemas abiertos de Erdős intentados, incluidos dos sin respuesta desde hace 56 años. También demostró 44 de 492 conjeturas abiertas del Online Encyclopedia of Integer Sequences (OEIS), cerró una pregunta de 15 años sobre funciones de Hilbert en geometría algebraica y mejoró una cota conocida en optimización convexa. El costo de inferencia fue de apenas algunos cientos de dólares por problema, según el paper de investigación.

¿Cómo evita las alucinaciones de los LLM?

A diferencia de los enfoques puramente en lenguaje natural —como la reciente demostración de OpenAI— el modelo de lenguaje subyacente en AlphaProof Nexus, en este caso Gemini 3.1 Pro, no tiene que sostener toda la cadena lógica por sí solo.

En vez de eso, genera pasos de demostración en el lenguaje formal de Lean, y el compilador chequea cada uno. Los mensajes de error vuelven directo a la siguiente iteración. Así el LLM queda anclado por retroalimentación simbólica, una red de seguridad que compensa las debilidades conocidas de los modelos de lenguaje en razonamiento lógico. Los humanos solo intervienen al final para revisar los resultados.

Cuatro agentes, un resultado sorprendente

El sistema consta de cuatro variantes de agente con complejidad creciente. El más simple, Agente (A), despliega subagentes independientes corriendo sobre Gemini 3.1 Pro en loops: el modelo genera pasos, Lean los chequea y los errores alimentan el siguiente intento.

Agente (B) agrega consultas a AlphaProof, el sistema de Google basado en aprendizaje por refuerzo para olimpiadas matemáticas, que puede rellenar segmentos faltantes de demostración. Agente (C) introduce un componente evolutivo inspirado en AlphaEvolve: los subagentes comparten una población común de bocetos de demostración, agentes de scoring construidos sobre Gemini 3.0 Flash los puntúan por plausibilidad y novedad, y luego los rankean con un sistema Elo. El Agente (D) combina todas estas capacidades.

El Agente (D) fue el usado para los problemas de Erdős. Pero un análisis posterior arrojó una sorpresa: el Agente (A) más simple, que solo usa LLM y feedback del compilador, también pudo demostrar los 9 problemas de Erdős resueltos, aunque con mayor costo en los más difíciles.

Los investigadores atribuyen el éxito del agente simple a dos factores: la mejora acelerada de los modelos de lenguaje base y "el poder del feedback del compilador para anclar el razonamiento del LLM". El agente completo aún mantiene ventaja en las tareas más duras, aunque esa diferencia podría reducirse a medida que los LLM mejoren. El paper habla de "un cambio en curso desde sistemas entrenados especializados hacia loops agénticos simples a medida que los LLM se vuelven más capaces".

¿Para qué sirve aunque no complete la demostración?

Los aciertos del sistema se concentran en áreas como combinatoria, optimización convexa y teoría de números, donde la biblioteca matemática Mathlib de Lean está madura y los problemas se descomponen en sub-objetivos manejables. La mayoría de los problemas de Erdős quedaron fuera del alcance: "Más aún, problemas que requieren teoría nueva extensa", escriben los investigadores. Los agentes también heredan la falta de fiabilidad de los modelos de lenguaje subyacentes.

Aun así, ven valor más allá de los problemas resueltos. Matemáticos que trabajaron con el sistema reportaron que incluso los intentos fallidos profundizaban su comprensión del problema, o como lo plantean los autores: "La búsqueda formal de demostraciones impulsada por IA puede servir no solo para resolver problemas, sino para profundizar la comprensión humana".

Como los bocetos eran formales, los expertos podían enfocarse en los sub-objetivos no resueltos en vez de re-chequear todo el argumento desde cero. Los agentes también demostraron ser eficaces para detectar formalizaciones erróneas en la literatura. "La verificación formal puede servir como filtro para decidir qué demostraciones merecen revisión humana", concluyen los autores.

El sistema ya se está usando en investigación en curso sobre óptica cuántica y teoría de grafos, según el paper. Todas las demostraciones formales en Lean y una selección de demostraciones en lenguaje natural están disponibles en GitHub.

¿Es AlphaProof mejor que GPT-5 en matemáticas?

OpenAI recientemente usó un modelo de razonamiento propietario para refutar la conjetura de distancia unitaria de Erdős. El medallista Fields Tim Gowers la calificó como "un hito en matemáticas con IA". Antes de eso, GPT-5.2 Pro ayudó a resolver el problema #281 de Erdős, con Terence Tao describiendo el caso como "quizás la instancia más inequívoca" de un LLM resolviendo un problema matemático abierto. Después, GPT-5.4 resolvió otro problema de Erdős.

En cierto sentido, esos resultados son más impresionantes que el enfoque de DeepMind. El modelo de lenguaje tuvo que cargar la cadena lógica completa en lenguaje natural, sin un compilador Lean revisando cada paso. AlphaProof Nexus es más sistemático y escalable, pero apunta a un objetivo distinto: construir una herramienta de IA confiable para investigación matemática cotidiana. OpenAI podría integrar Lean a su scaffold también, claro, pero ahí el foco es testear la capacidad bruta del LLM.

Tao ya había advertido contra leer demasiado en los titulares. La tasa real de éxito de la IA en problemas de Erdős está apenas en uno o dos por ciento, concentrada en los más fáciles. El sistema de Google resolvió solo 9 de 353 problemas, una tasa de 2,5% que coincide casi exactamente con la barrera del 2% que planteó Tao.