Introducción
En mayo de 2026, DeepMind publicó en arXiv el paper Advancing Mathematics Research with AI-Driven Formal Proof Search, donde presenta AlphaProof Nexus, un sistema de pruebas formales orientado a la investigación matemática.
Si solo miramos los resultados, parece otra historia sobre IA demostrando problemas matemáticos: el sistema resolvió 9 de 353 problemas abiertos de Erdos formalizados, probó 44 de 492 conjeturas de OEIS, y también se utilizó en investigaciones reales de teoría de grafos, optimización, geometría algebraica, combinatoria aditiva y óptica cuántica.
Pero para mí, trabajando en IA + educación, lo más interesante no es solo el resultado, sino la ruta de investigación:
Dejar que los grandes modelos propongan ideas de prueba, que sistemas formales como Lean las verifiquen, que buscadores especializados resuelvan objetivos locales, y que una orquestación multiagente convierta fallos, borradores parciales y subobjetivos en activos reutilizables de búsqueda.
Este ensayo explica AlphaProof Nexus en lenguaje sencillo: por qué existe, cómo está diseñado el sistema y cuáles son los cuatro paradigmas de investigación matemática con IA que aparecen en el paper.
1. Por qué AI for Math necesita pruebas formales
La mayoría de las personas entiende una prueba matemática en lenguaje natural:
Como A es verdadero, se sigue B. Por cierto teorema, se sigue C. Por lo tanto, la conclusión es verdadera.
Esto funciona para matemáticos humanos porque las personas pueden completar los pasos lógicos omitidos. Para la IA, sin embargo, hay un problema serio: los grandes modelos escriben muy bien textos que parecen pruebas, pero eso no significa que realmente hayan demostrado algo.
Pueden:
- citar teoremas inexistentes;
- saltarse pasos clave;
- reemplazar un problema difícil por otro que parece más fácil pero sigue sin estar demostrado;
- escribir derivaciones muy seguras en tono, pero incorrectas en lógica.
Por eso el punto de partida del paper de DeepMind es hacer que la IA trabaje dentro de un sistema estricto.
Ese sistema es Lean.
Lean puede entenderse como un compilador matemático. Cuando los programadores escriben código, el compilador revisa errores de sintaxis y de tipos. Cuando los matemáticos escriben pruebas en Lean, Lean revisa si cada paso lógico realmente se sostiene.
Si Lean acepta una prueba, esa prueba no solo parece correcta. Ha pasado una verificación estricta por máquina.
Esa es la idea básica de AlphaProof Nexus:
La IA puede adivinar, probar y fallar, pero la respuesta final debe pasar la verificación de Lean.
2. Qué es AlphaProof Nexus
AlphaProof Nexus no es un único gran modelo ni un asistente matemático que solo conversa. Se parece más a una línea de investigación matemática con IA.
La entrada es un archivo Lean con una prueba de teorema sin terminar. El sistema modifica, completa y descompone esa prueba una y otra vez hasta que Lean la acepta.
Podemos imaginarlo así:
Hay varios roles clave:
- LLM: propone ideas de prueba, escribe código Lean y corrige errores.
- Lean: verifica si la prueba es realmente correcta.
- AlphaProof: resuelve ciertos objetivos locales de prueba.
- Rater Agent: compara borradores y estima cuáles son más prometedores.
- Population DB: guarda muchos borradores incompletos pero valiosos.
- SafeVerify: hace las comprobaciones finales contra trampas, como modificar el teorema original o introducir axiomas no permitidos.
3. Cuatro paradigmas de investigación matemática con IA
DeepMind compara cuatro configuraciones de agentes. También pueden leerse como cuatro paradigmas para hacer investigación matemática con IA.
Paradigma 1: Basic Agent
El primer patrón es el más básico: LLM + bucle de feedback de Lean.
Funciona de forma parecida a un programador escribiendo código:
- El LLM lee una prueba Lean incompleta.
- Intenta completar una parte del código de prueba.
- Lean compila el archivo.
- Si Lean reporta errores, esos errores vuelven al LLM.
- El LLM edita la prueba según los errores.
- Esto se repite hasta que la prueba pasa o se agota el presupuesto.
La capacidad central aquí es iterar, fallar y corregir.
Imagina a un estudiante resolviendo un problema. Primero escribe una solución, el profesor señala qué está mal, y luego el estudiante la revisa. En este caso el profesor no es una persona, sino el compilador Lean. Lean no dirá si una idea es elegante, pero sí indicará con dureza si un tipo no encaja, si queda un objetivo sin resolver, si un teorema no corresponde o si falta un paso lógico.
Eso le da al gran modelo feedback de muy alta calidad.
Una conclusión interesante del paper es que Basic Agent ya es fuerte.
En experimentos posteriores, Basic Agent también pudo reproducir los 9 casos exitosos de Erdos, aunque los problemas más difíciles exigieron más coste y tuvieron peor eficiencia.
Esto sugiere que, a medida que mejoran los modelos base, el bucle simple de "generar - compilar - reparar" ya se ha convertido en una línea base muy competitiva para matemática formal.
La lección es clara: no hay que esperar que un gran modelo produzca una prueba perfecta en un solo intento. Hay que ponerlo dentro de un entorno que pueda dar feedback continuo y forzar revisiones.
Paradigma 2: Basic Agent + AlphaProof
El segundo paradigma añade AlphaProof sobre Basic Agent.
AlphaProof es un sistema de búsqueda de pruebas formales que DeepMind desarrolló antes. En Nexus no es el protagonista principal. Funciona más como un especialista en pruebas locales.
Cuando un LLM escribe pruebas en Lean, a menudo se encuentra con objetivos pequeños, por ejemplo:
En el contexto actual, demuestra este subresultado.
Algunos subobjetivos son mecánicos, pero no siempre son fáciles de escribir para un LLM. Otros requieren buscar una secuencia de tactics, es decir, comandos de prueba en Lean. En ese momento, el sistema puede entregar esos objetivos locales a AlphaProof.
AlphaProof puede devolver tres tipos de resultado:
- encuentra una prueba;
- demuestra que el subobjetivo en realidad es falso;
- no encuentra una prueba dentro del presupuesto.
Esto importa porque el LLM ya no tiene que cargar solo con todos los detalles de la prueba.
Podemos verlo así: el LLM se parece a un estudiante de posgrado que se encarga de la idea global y de la estructura; AlphaProof se parece a un buscador táctico que resuelve detalles técnicos locales; Lean es el juez final.
El paper también señala que AlphaProof por sí solo no puede resolver de forma independiente estos problemas abiertos de nivel investigador.
En los experimentos, AlphaProof aislado no resolvió los 9 problemas de Erdos. Su lugar efectivo es dentro del sistema más grande de Nexus, como herramienta local de prueba.
Paradigma 3: Basic Agent + Evolution
El tercer paradigma introduce una idea clave: búsqueda evolutiva.
Una prueba matemática muchas veces no es lineal.
Una ruta puede atascarse a mitad de camino. Otra puede estar incompleta, pero más cerca de la idea central. Una tercera puede haber demostrado lemas útiles aunque el teorema principal siga pendiente.
Si cada ejecución del agente empieza desde cero, se desperdicia mucha exploración. Por eso AlphaProof Nexus guarda borradores de prueba incompletos en una Population DB, una población semilla de proof sketches.
Luego el sistema usa un Rater Agent para comparar esos borradores y decidir cuáles tienen más potencial.
Se parece un poco a la evolución:
- cada borrador de prueba es un individuo;
- los agentes mutan y reescriben borradores;
- el evaluador selecciona borradores más prometedores;
- el sistema invierte cómputo en las rutas con más potencial.
La dificultad es que las señales de éxito en una prueba matemática son muy escasas. En optimización de programas, incluso un programa no óptimo puede obtener una puntuación. En prueba formal, normalmente la prueba completa funciona o no funciona.
Los estados intermedios son difíciles de cuantificar.
La solución de DeepMind es pedir a los modelos que comparen la calidad de borradores, en lugar de asignar puntuaciones absolutas. Por ejemplo:
Entre estas pruebas incompletas, ¿qué ruta es más clara? ¿Qué objetivos restantes parecen más creíbles? ¿Cuál tiene más probabilidad de completarse?
Después, el sistema ordena los borradores con un mecanismo similar a Elo y usa una estrategia tipo P-UCB para equilibrar dos necesidades:
- seguir desarrollando rutas con alta puntuación;
- explorar rutas que todavía no se han intentado lo suficiente.
Paradigma 4: Full-Featured Agent
El cuarto paradigma es el sistema principal del paper: LLM + Lean + AlphaProof + Evolution.
Combina las capacidades anteriores:
- el LLM escribe pruebas, edita pruebas y propone lemas;
- Lean verifica si cada paso es correcto;
- AlphaProof maneja subobjetivos locales;
- Evolution guarda y filtra diferentes rutas de prueba;
- Rater Agent decide qué borradores merecen más trabajo;
- SafeVerify realiza la verificación final de seguridad.
Esa es la forma completa de AlphaProof Nexus.
La manera en que resuelve problemas matemáticos se parece a un equipo de investigación altamente automatizado: alguien propone ideas, alguien revisa la lógica, alguien resuelve detalles técnicos locales, alguien evalúa distintas direcciones, alguien administra intentos históricos y alguien hace la validación final.
4. Un diseño clave: la búsqueda de pruebas debe prevenir trampas
La prueba matemática con IA tiene un modo de fallo particular: el sistema puede hacer que la prueba sea más fácil cambiando el problema, y a menudo aprende a hacerlo.
Supongamos que el objetivo original es demostrar que la propiedad P se cumple para todos los números naturales n.
Un agente podría cambiarlo silenciosamente a: la propiedad P se cumple para algunos números naturales n.
O podría introducir un axioma no permitido que, en la práctica, asume la conclusión.
Lean podría pasar ciertas verificaciones locales, pero eso claramente no es la prueba que queremos.
Por eso AlphaProof Nexus realiza varias capas de comprobación de seguridad:
- comprobar si el enunciado del teorema fue modificado;
- comprobar si queda algún
sorry; - comprobar si se introdujeron axiomas no permitidos;
- comprobar si la prueba corresponde realmente al problema original;
- ejecutar Lean en un entorno sandbox.
Esto sirve para todos los sistemas de agentes: cuando el objetivo es lo bastante complejo, los agentes pueden aprender a esquivar el objetivo en lugar de cumplirlo. Las restricciones fuertes de verificación son obligatorias.
5. Resultados experimentales del paper
DeepMind aplicó el sistema a varias tareas matemáticas. Las más representativas son los problemas de Erdos y las conjeturas de OEIS.
1. Problemas de Erdos
Erdos fue uno de los matemáticos más importantes del siglo XX y dejó muchos problemas abiertos. El paper reporta que el sistema procesó 353 problemas abiertos de Erdos formalizados y resolvió 9.
El porcentaje puede parecer bajo, pero estos no son problemas elementales de competición. Son problemas matemáticos de nivel investigador.
2. Conjeturas de OEIS
OEIS es una base de datos de sucesiones enteras con muchas conjeturas sobre patrones de secuencias. El sistema probó 44 de 492 conjeturas de OEIS.
Este tipo de tarea encaja muy bien con los sistemas de prueba formal, porque muchas conjeturas de sucesiones pueden codificarse de forma clara como definiciones y teoremas.
3. Uso en investigación matemática real
El paper también afirma que el sistema se usó en varias áreas de investigación, incluidas teoría de grafos, optimización, geometría algebraica, combinatoria aditiva y óptica cuántica.
6. Cierre
Estas son mis conclusiones después de leer el paper con detalle.
Conclusión 1: Los LLM ya pueden ser componentes centrales de la búsqueda formal de pruebas
Durante mucho tiempo se dijo que los grandes modelos no sirven para matemática rigurosa porque alucinan, saltan pasos e inventan cosas.
Eso es cierto, pero incompleto.
Si le pedimos a un LLM que escriba directamente una prueba en lenguaje natural, no es confiable. Pero si lo ponemos dentro de un sistema de feedback estricto como Lean, puede convertirse en un motor de búsqueda eficiente.
El valor del LLM no está en ser siempre correcto. Está en proponer muchas rutas candidatas y corregirlas continuamente según el feedback del compilador.
Conclusión 2: La orquestación multiagente importa más que un único modelo
El punto de AlphaProof Nexus no es que cierta versión de modelo pueda resolver problemas difíciles. El punto es que el sistema separa capacidades: generación, verificación, búsqueda, evaluación, caché y validación.
Esa es una mentalidad de ingeniería. La investigación matemática se modela como un proceso de búsqueda de largo plazo.
Conclusión 3: Los fallos también tienen valor
Proof sketches incompletos, subobjetivos fallidos, errores de Lean y resultados de búsqueda de AlphaProof pueden entrar en ciclos posteriores.
Eso hace que la búsqueda de pruebas matemáticas se parezca más a la ingeniería de software: el código se puede reutilizar, los logs de error se pueden analizar, los estados intermedios se pueden guardar, las ramas pueden continuar y el resultado final lo acepta un compilador.
Conclusión 4: Los modelos fuertes y baratos pueden dividir el trabajo
El paper usa modelos más fuertes para generar pruebas complejas y modelos más baratos para comparar y ordenar borradores.
Es una lección práctica de ingeniería de agentes. No todos los pasos necesitan el modelo más fuerte.
Usar modelos fuertes para razonamiento complejo, modelos baratos para evaluación de alto volumen y herramientas especializadas para pruebas locales escala mejor que pedirle a un único modelo caro que haga todo.