Qué afirma el artículo
Un equipo de Google DeepMind ha publicado un informe revisado por pares sobre un sistema de IA que encuentra demostraciones matemáticas y las somete a verificación automática sobre la marcha. El artículo, “Advancing Mathematics Research with AI-Driven Formal Proof Search”, de Tsoukalas y colegas, apareció en Science el 8 de octubre.
El sistema, AlphaProof Nexus, está construido en torno a Gemini 3.1 Pro. Redacta una demostración en Lean, un lenguaje formal en el que cada paso lógico es verificado por software, y los mensajes de error del verificador guían el siguiente borrador. Para subproblemas más difíciles puede delegar en AlphaProof, la herramienta especializada de DeepMind.
Los investigadores seleccionaron 353 problemas abiertos de la colección de Erdős y los codificaron en Lean. El sistema cerró nueve de ellos — alrededor del 2,5% — dos de los cuales llevaban 56 años sin resolver. También demostró 44 conjeturas de la Enciclopedia en Línea de Sucesiones de Enteros, resolvió una cuestión abierta de geometría algebraica y mejoró una cota conocida en optimización min-max, una técnica que se usa al entrenar algunos modelos de IA.
La ablación es la parte interesante
DeepMind informa de que el sistema resolvió esos mismos nueve problemas de Erdős sin AlphaProof. Un análisis de ablación encontró que una configuración más simple, que el artículo llama Agente A, alcanzó los mismos nueve, un punto que plantea Josep Curto, de la Universitat Oberta de Catalunya, en los comentarios de expertos recogidos por Science Media Centre España. Curto lee el resultado como señal de sobreingeniería y sostiene que el artículo arrastra inconsistencias metodológicas.
Su objeción más afilada es sobre qué compra y qué no compra la verificación formal. Lean, señala, garantiza que una demostración es lógicamente válida. No garantiza que el enunciado que alguien formalizó sea el problema que pretendía enunciar. La traducción de una conjetura informal a Lean sigue siendo un paso humano, y un error ahí sobrevive intacto al verificador.
Cómo debe leerse nueve de 353
El denominador importa. Son nueve éxitos sobre un conjunto definido que el equipo eligió y formalizó, no una capacidad general de derribar conjeturas célebres. Pablo Haya Coll, de la Universidad Autónoma de Madrid, en el mismo conjunto de comentarios, apunta a la metodología más que al recuento: el valor está en una forma repetible de generar descubrimientos matemáticos, no en los nueve.
Javier Aramayona, director del Instituto de Ciencias Matemáticas, plantea el problema que se deriva de que las demostraciones verificadas lleguen más rápido de lo que alguien las lee: muchos resultados generados por IA están verificados y, aun así, no se entienden del todo. Teodoro Calonge, de la Universidad de Valladolid, lo calificó de artículo de alta calidad y de intento temprano, con bastante margen de mejora.
El contraste con el otro laboratorio
La ruta que tomó este trabajo forma parte de la historia. DeepMind publicó las soluciones de Erdős antes de que apareciera el artículo y después sometió el trabajo a revisión por pares. OpenAI tomó la otra ruta y publicó cientos de demostraciones generadas por IA en un repositorio, lo que llevó a un grupo de matemáticos a pedir un boicot a la empresa a principios de este mes.
Lo que conviene vigilar es si los archivos de Lean resisten el escrutinio externo, y si alguna de las nueve formalizaciones termina enunciando algo distinto del problema de Erdős con el que está etiquetada. Esa comprobación está ahora al alcance de cualquiera, que es el argumento práctico a favor de la ruta que eligió DeepMind.
