Reacción a "Diseñan AlphaProof Nexus, una nueva herramienta de IA para abordar demostraciones matemáticas"

Cuando leemos titulares sobre sistemas de inteligencia artificial (IA) "resolviendo problemas abiertos de matemáticas que llevaban décadas estancados", es fácil dejarse llevar por la narrativa del progreso inevitable. Sin embargo, al analizar con lupa los detalles técnicos del artículo sobre AlphaProof Nexus, publicado en Science por investigadoras e investigadores de Google DeepMind, nos encontramos con un patrón tristemente habitual en el panorama actual de la IA: una demostración deslumbrante de capacidad técnica empañada por importantes inconsistencias metodológicas y un severo problema de sobreingeniería.  

El artículo presenta a AlphaProof Nexus como un marco avanzado para la búsqueda de demostraciones formales en Lean. Los autores construyeron un agente ‘completo’ (Agente D) que combina un bucle básico de generación-verificación, integración con el probador AlphaProof mediante aprendizaje por refuerzo y un algoritmo evolutivo guiado por un sistema de votación y ratings Elo entre subagentes. Sobre el papel, la cifra impresiona: resolución autónoma de nueve problemas abiertos de la célebre lista de Erdős, 44 conjeturas del OEIS y descubrimientos aplicados en optimización y teoría de grafos.  

Pero cuando uno profundiza en la metodología y en el análisis post hoc del propio estudio, la estructura conceptual empieza a agrietarse.   

Primero. El propio análisis de ablación de los autores revela un dato demoledor: el Agente A (un bucle básico y simple tipo "Ralph loop" que alterna la generación del LLM con la verificación del compilador de Lean) replicó los mismos nueve problemas de Erdős que resolvió el sofisticado Agente D. ¿Qué nos dice esto? Que la complejidad del framework no es la que impulsa el descubrimiento; lo que realmente mueve la aguja es la capacidad base del LLM (en este caso, Gemini 3.1 Pro) combinada con el feedback directo e inflexible del compilador formal.  

Segundo. Desde una perspectiva de gestión de datos y recursos, la evaluación financiera del estudio es, como mínimo, opaca. En sus métricas de coste de inferencia (en USD), el estudio muestra que los agentes simplificados son más rentables en la mayoría de problemas, mientras que el Agente D solo justifica su coste en casos puntuales como Erdős #125. El artículo omite dos detalles relevantes: los cálculos solo contabilizan la inferencia en las ejecuciones exitosas y los costes reportados para los agentes B y D excluyen el coste de inferencia de AlphaProof.  

Tercero. Existe la falsa percepción de que, al utilizar un lenguaje formal como Lean, la ‘alucinación’ queda erradicada. Lean garantiza que la demostración es lógicamente válida para el enunciado escrito en Lean, pero no garantiza que dicho enunciado traduzca fielmente el problema matemático real. El artículo reconoce varios escenarios en los que los agentes alucinan y/o incurren en vulnerabilidades de formalización errónea. Esto demuestra que el sistema sigue necesitando una supervisión humana experta intensiva para validar que lo que el agente ha demostrado es realmente lo que se quería demostrar.  

La verdadera lección que nos deja este trabajo (aunque los autores intenten matizarla) es que el mercado y la investigación deben inclinarse hacia la simplicidad: bucles agénticos limpios, potentes modelos de lenguaje y entornos de retroalimentación estricta (compiladores, ejecuciones de código, pruebas unitarias y supervisión humana experta), aunque probablemente no al alcance de todas las universidades e institutos de investigación. Todo lo demás, de momento, son fuegos artificiales evolutivos que aportan más complejidad arquitectónica que resultados tangibles.