DeepMind publica en Science un agente que resuelve problemas abiertos de Erdős

Google DeepMind ha publicado en la revista Science un paper en el que presenta AlphaProof Nexus, un agente que combina generación de pruebas con un modelo de lenguaje y verificación formal en Lean. El sistema ha resuelto de forma autónoma 9 de 353 problemas abiertos de Erdős y ha demostrado 44 de 492 conjeturas de la Online Encyclopedia of Integer Sequences.

-IA Crew dice: Resolver problemas que llevaban décadas abiertos a un coste de unos cientos de dólares cada uno es el tipo de noticia que hace que los matemáticos miren dos veces la factura de la nube.-

Cómo funciona el agente

AlphaProof Nexus alterna entre propuestas de prueba generadas por un LLM (principalmente Gemini) y la verificación automática que realiza el compilador de Lean. Si un paso no es correcto, el sistema lo detecta y vuelve a intentarlo. Una versión básica del agente, que simplemente itera generación y verificación, ya fue capaz de reproducir los nueve éxitos de Erdős. La versión completa añade un pool compartido de bocetos, ranking y selección evolutiva.

Dos de los problemas de Erdős resueltos llevaban 56 años abiertos. El coste de inferencia por problema se sitúa en el orden de unos cientos de dólares. El paper también reporta la resolución de una cuestión abierta en geometría algebraica y la mejora de un bound en optimización.

La clave es que cada paso de la prueba queda verificado por el compilador, lo que elimina gran parte de la incertidumbre habitual en las demostraciones generadas por lenguaje natural.

-IA Crew dice: Lean no acepta un “parece correcto”. O el paso es válido o hay que volver a empezar, y eso cambia bastante el juego.-

Por qué supone un avance real

Hasta ahora los modelos de lenguaje destacaban en problemas de olimpiada o en tareas con soluciones conocidas. Aquí el agente se enfrenta a problemas abiertos de investigación, formalizados previamente, y produce pruebas que pueden comprobarse mecánicamente. El hecho de que una versión simple ya obtenga los mismos resultados en Erdős sugiere que el ciclo generación-verificación es, por sí solo, muy potente.

DeepMind indica que el sistema se está desplegando en áreas como combinatoria, teoría de grafos, geometría algebraica y óptica cuántica. También ha ayudado a detectar formalizaciones incorrectas en la literatura existente.

Límites y contexto

El enfoque depende de que los problemas estén formalizados en Lean. No todos los problemas abiertos lo están, y formalizarlos sigue siendo trabajo humano. El paper no afirma que el agente haya inventado matemáticas completamente nuevas desde cero, sino que ha resuelto problemas ya planteados y formalizados. Aun así, la escala y el coste hacen que la búsqueda formal de pruebas pase de ser una curiosidad a una herramienta de investigación utilizable.

-IA Crew dice: Si el agente resuelve problemas de Erdős mientras tú revisas el correo, quizá sea el momento de preguntarle si también puede formalizar el problema que tienes abierto en la pizarra.-

Diccionario de la Crew

Lean — Asistente de pruebas formal en el que cada paso lógico es verificado automáticamente por el compilador.

Erdős — Paul Erdős, matemático húngaro que planteó cientos de problemas abiertos, muchos de ellos aún sin resolver.

OEIS — Online Encyclopedia of Integer Sequences, base de datos de secuencias enteras y conjeturas asociadas.

Agente — Sistema que itera entre generación de candidatos y verificación externa para resolver una tarea en varios pasos.