Nueve de los 353 problemas abiertos de Erdős que se le pusieron por delante han caído ante un agente de IA, y otras 44 de 492 conjeturas sobre secuencias de enteros han quedado demostradas. Son enunciados que llevaban años, en algunos casos décadas, sin que nadie los cerrara —incluidas dos preguntas abiertas durante 56 años—, según el paper «Advancing Mathematics Research with AI-Driven Formal Proof Search».

Cada prueba se escribió en Lean, el lenguaje formal en el que el ordenador comprueba paso a paso que el razonamiento no tiene huecos. El agente resolvió 9 de 353 a un coste de inferencia de unos cientos de dólares por problema, con tope de 3.000 episodios de búsqueda por enunciado.

Lo que valida un humano es que el enunciado en Lean sea fiel a la conjetura original, y eso lo hicieron expertos del equipo tras cada resolución. Para blindarse contra formalizaciones erróneas en OEIS, el agente debió probar antes «lemas test» con los primeros términos de cada secuencia. Las pruebas son públicas y constan en la wiki que Terence Tao mantiene sobre contribuciones de la IA a los problemas de Erdős.

El botín no termina ahí: el mismo agente resolvió una pregunta de 15 años sobre funciones de Hilbert en geometría algebraica, mejoró una cota abierta en optimización convexa con un esquema de parámetros inédito, detectó formalizaciones erróneas en la literatura y ya trabaja en combinatoria, teoría de grafos, geometría algebraica y óptica cuántica, como resume PubMed (8-oct-2026).

El matiz honesto lo ponen los propios autores y la experiencia paralela de DeepMind: solo una fracción de la literatura matemática está formalizada en Lean, muchos enunciados son ambiguos y el estatus «abierto» de varios problemas resolvía más oscuridad que dificultad. La IA, aquí, es tanto detectora de huecos como resolvedora.

El agente muestra su trabajo línea a línea, de modo que comprobarlo cuesta bastante menos que seguir una demostración escrita a mano. La matemática verificable por máquina deja de ser promesa para ser método —y van nueve muescas en el tablero de Erdős.

El contexto es una primavera formal: el repositorio abierto Formal Conjectures ya reúne enunciados Lean de parte del catálogo de Bloom (más de 1.200 problemas de Erdős y colaboradores), y la wiki de Tao registra soluciones semanales de Aristotle, GPT, Claude, Codex y Gemini. La carrera por formalizar las matemáticas avanza más rápido que la de resolverlas a mano.

Fuentes
arXiv: búsqueda formal de pruebas con IA (abs + HTML)
Wiki de Terence Tao: contribuciones de la IA a problemas de Erdős
PubMed: resumen del estudio (8-oct-2026)
Crédito de la imagen: Paul Erdős con el joven Terence Tao, fotografía de Billy o Grace Tao, licencia CC BY-SA 2.0 vía Wikimedia Commons.