La revista Science publicó el 8 de octubre de 2026 el artículo «Advancing mathematics research with AI-driven formal proof search», firmado por George Tsoukalas y colegas de Google DeepMind, que presenta AlphaProof Nexus: un marco de inteligencia artificial basado en modelos de lenguaje que busca demostraciones matemáticas de forma autónoma y las verifica paso a paso en Lean, un lenguaje formal cuyo compilador comprueba cada inferencia lógica. Según el resumen difundido por la Asociación Estadounidense para el Avance de la Ciencia (AAAS) en EurekAlert, el sistema resolvió decenas de problemas que seguían abiertos en varias ramas de las matemáticas.
El dato más llamativo procede de los problemas de Erdős, el catálogo de más de 1.200 preguntas planteadas por el matemático húngaro Paul Erdős y sus colaboradores que mantiene Thomas Bloom. El repositorio abierto Formal Conjectures contiene formalizaciones en Lean de un subconjunto de esos problemas; en el momento del experimento eran 353. El agente más completo de DeepMind los atacó todos, con un límite de 3.000 episodios por problema, y resolvió nueve. Dos de ellos llevaban 56 años sin solución, según el preprint del trabajo.
Además, AlphaProof Nexus demostró 44 de 492 conjeturas abiertas de la Enciclopedia en Línea de Sucesiones de Enteros (OEIS), resolvió una pregunta abierta desde hacía quince años sobre funciones de Hilbert en geometría algebraica y mejoró una cota conocida en optimización convexa al descubrir un nuevo calendario de parámetros algorítmicos. Los autores señalan también que el sistema identificó varias formalizaciones erróneas en la literatura, ayudó a resolver un problema de la conocida lista de Ben Green y está contribuyendo a investigaciones en curso en óptica cuántica y teoría de grafos.
La arquitectura es la clave del enfoque. En su versión básica, varios subagentes buscan demostraciones de manera independiente y reciben como retroalimentación los mensajes de error del compilador de Lean, que les indican exactamente qué paso falla. En la versión «completa», esos subagentes se coordinan mediante un algoritmo evolutivo inspirado en AlphaEvolve y pueden recurrir a AlphaProof, el sistema de aprendizaje por refuerzo que DeepMind desarrolló para la demostración de teoremas de nivel olímpico, como herramienta especializada para subproblemas difíciles.
La verificación formal aborda uno de los problemas centrales de la IA aplicada a las matemáticas: los modelos de lenguaje pueden producir argumentos convincentes que contienen errores sutiles o directamente inventados. Revisar a mano demostraciones largas exige el tiempo de expertos, que es escaso. Cuando la prueba está escrita en Lean y el compilador la acepta, la corrección lógica queda garantizada, siempre que el enunciado formal capture fielmente la pregunta original. Por eso, tras cada resolución, especialistas del equipo validaron que la formalización de cada problema de Erdős era fiel al enunciado.
El coste también es relevante. Según el preprint, el agente completo resolvió los problemas de Erdős con un coste de inferencia de unos pocos cientos de dólares por problema. Esa cifra, modesta frente al valor de un resultado matemático nuevo, sugiere que este tipo de búsqueda podría convertirse en una herramienta rutinaria para grupos de investigación, al menos en problemas que se puedan formalizar con precisión. DeepMind publicó las demostraciones en Lean y versiones en prosa redactadas por humanos en el repositorio público alphaproof-nexus-results.
La comunidad matemática ha seguido estos avances con interés y cautela. Los resultados sobre problemas de Erdős quedaron registrados en la wiki que Terence Tao mantiene sobre contribuciones de la IA a esos problemas. En una perspectiva publicada junto al artículo en Science, Jeremy Avigad, de la Universidad Carnegie Mellon, y Matthew Ballard, de la Universidad de Carolina del Sur, destacan que incluso los intentos fallidos de la IA ayudaron a los autores a entender mejor los problemas, y subrayan que el objetivo esencial es apoyar a los matemáticos en la búsqueda de conocimiento y comprensión.
Conviene situar la cifra en su contexto. Nueve de 353 equivale a algo más del 2,5 % de los problemas intentados, y muchos de los problemas de Erdős resueltos no figuran entre los más famosos del catálogo. El trabajo no afirma haber resuelto ninguno de los grandes problemas del milenio ni nada comparable. Su aportación es demostrar que un sistema automatizado puede producir, con garantías formales, resultados nuevos y verificables en matemáticas de nivel de investigación, algo que hasta hace poco se limitaba a competiciones o a la formalización de demostraciones ya conocidas.
La publicación en una revista con revisión por pares también marca un contraste con otras vías de difusión. En las últimas semanas, otros laboratorios han publicado grandes lotes de manuscritos matemáticos generados por IA directamente en repositorios, lo que ha abierto un debate sobre cómo validar y atribuir ese tipo de trabajos. El artículo de DeepMind pasó por el proceso editorial de Science y viene acompañado de los archivos formales, lo que permite a cualquier persona con Lean instalado comprobar las demostraciones.
Entre los nombres que figuran como contactos expertos en el comunicado de la AAAS están Pushmeet Kohli y Swarat Chaudhuri, de Google DeepMind. La línea de trabajo enlaza con AlphaProof y AlphaGeometry, que en 2024 alcanzaron rendimiento de medalla en la Olimpiada Internacional de Matemáticas, y con AlphaEvolve, el sistema de búsqueda evolutiva de algoritmos. AlphaProof Nexus combina esas piezas y da el salto de los problemas de competición, con solución conocida, a preguntas para las que nadie tenía respuesta.
Las implicaciones van más allá de las matemáticas puras. La combinación de modelos generativos con un verificador estricto es un patrón aplicable a otros campos donde existe una forma automática de comprobar resultados, como la verificación de software, el diseño de chips o ciertos problemas de optimización industrial. La mejora de la cota en optimización convexa, obtenida al descubrir un nuevo calendario de parámetros, ilustra cómo un resultado teórico puede tener consecuencias prácticas en algoritmos usados a diario.
Quedan límites claros. El método depende de que el problema pueda expresarse formalmente, y buena parte de las matemáticas actuales todavía no está formalizada en Lean. También depende de la fidelidad de la formalización: un enunciado formal mal planteado puede producir una demostración correcta de algo distinto a lo que se pretendía, un riesgo que el propio sistema ayudó a detectar al identificar formalizaciones erróneas. Y la elección de qué preguntas merecen atención sigue siendo, por ahora, una tarea humana.
Con todo, la publicación de AlphaProof Nexus en Science consolida una tendencia: la IA empieza a funcionar como colaboradora verificable en la investigación matemática, no solo como asistente que sugiere ideas. Si los costes siguen bajando y la biblioteca de matemáticas formalizadas crece, herramientas de este tipo podrían cambiar la manera en que se exploran conjeturas abiertas, siempre con la verificación formal como garantía y con los matemáticos decidiendo qué resultados importan.
