Un estudio de Google DeepMind publicado el 8 de octubre de 2026 informó de que la configuración completa de AlphaProof Nexus resolvió 9 de 353 problemas de Erdős formalizados. El sistema también demostró 44 de 492 conjeturas seleccionadas de la Online Encyclopedia of Integer Sequences (OEIS); dos de los problemas de Erdős llevaban 56 años abiertos.
Qué hace AlphaProof Nexus
AlphaProof Nexus es un sistema de búsqueda de demostraciones formales: parte de un enunciado matemático expresado en un lenguaje preciso y genera intentos de prueba que un programa puede comprobar. En este caso, ese programa es Lean, un asistente de demostraciones que verifica mecánicamente si la prueba formal demuestra el teorema codificado.
El estudio de Google DeepMind presentó los resultados en dos conjuntos separados. Cada cifra corresponde a un tipo distinto de problema y a su propia muestra.
Qué miden los resultados publicados
| Conjunto evaluado | Problemas o conjeturas demostrados | Elementos evaluados | Alcance |
| Problemas de Erdős | 9 | 353 | Problemas formalizados en el repositorio Formal Conjectures cuando se realizó la evaluación |
| Conjeturas de la OEIS | 44 | 492 | Conjeturas abiertas seleccionadas para el estudio |
Las 353 entradas de Erdős eran el subconjunto formalizado disponible en Formal Conjectures para la evaluación, no todo el catálogo de problemas de Erdős, que supera los 1.200. En la muestra estudiada, dos de los nueve problemas resueltos llevaban 56 años abiertos.
Para las conjeturas de la OEIS, los investigadores seleccionaron 492 casos abiertos. El estudio informó de que una revisión manual encontró que las 44 conjeturas demostradas estaban correctamente formalizadas y no se habían demostrado antes.
Cómo funciona la búsqueda de demostraciones
La entrada descrita para AlphaProof Nexus es un teorema escrito en Lean y un esquema de demostración. Puede incluir también contexto en lenguaje natural y conocimiento del dominio codificado en Lean. Los agentes de modelos de lenguaje proponen y revisan fragmentos de prueba; Lean los comprueba y devuelve errores del compilador que orientan los siguientes intentos.
La configuración completa añade una búsqueda evolutiva: mantiene una población compartida de esquemas, los clasifica y selecciona cuáles desarrollar. También puede recurrir a AlphaProof, un sistema especializado en demostraciones, para abordar subobjetivos. La implementación descrita empleó Gemini 3.1 Pro para los agentes que razonan sobre demostraciones y Gemini 3.0 Flash para puntuar esquemas.
Qué significan los resultados
Lean comprueba que una demostración formal se ajusta al enunciado formalizado. La correspondencia entre ese enunciado y la pregunta matemática original es una cuestión distinta. Para los problemas de Erdős, el estudio describe una revisión experta de las formalizaciones.
La mayoría de los problemas de Erdős evaluados quedó sin resolver. Los autores situaron los éxitos sobre todo en áreas como combinatoria, optimización convexa y teoría de números, donde las bibliotecas matemáticas de Lean están más desarrolladas.
