El sistema de demostración matemática AlphaProof Nexus, de Google DeepMind, se ha publicado oficialmente en Science. El primer autor del artículo es Tsoukalas, y todo el equipo de investigación pertenece a DeepMind. El trabajo ya se había difundido como preprint a finales de mayo; ahora llega la versión de revista, tras la revisión por pares.
El balance no cambia: el sistema intentó 353 problemas de Erdős sin resolver y logró 9, dos de ellos abiertos desde hacía 56 años; de las 492 conjeturas abiertas de la OEIS, la base de datos de sucesiones de enteros, demostró 44. Además respondió a una pregunta de geometría algebraica sobre la función de Hilbert, pendiente desde hacía unos 15 años, y mejoró una cota conocida en optimización min-max.
Un Gemini y un compilador de Lean
La base del sistema es Gemini 3.1 Pro. El modelo redacta demostraciones en el lenguaje formal Lean; el compilador de Lean las comprueba tras cada cambio y los mensajes de error se devuelven directamente al siguiente intento. En todo el proceso, la persona solo mira el resultado al final.
El artículo distingue cuatro versiones:
- Versión A: el bucle “generar y verificar” más básico, en el que el modelo grande escribe y el compilador juzga;
- Versión B: sobre la A, incorpora AlphaProof, el demostrador anterior de DeepMind, para completar los fragmentos que faltan en la demostración;
- Versión C: añade un mecanismo evolutivo, en el que varios subagentes comparten un conjunto de borradores de demostración ordenado por puntuación Elo;
- Versión D: todo lo anterior combinado, usado para atacar los problemas de Erdős.
Lo más llamativo del resultado es que la versión A también demostró de forma independiente los 9 problemas de Erdős; solo que en los más difíciles gastó más dinero. El coste de inferencia que cita The Decoder es de unos cientos de dólares por problema. Los autores escriben en el artículo:
"power of compiler feedback in grounding LLM reasoning"
(La retroalimentación del compilador ancla en la realidad el razonamiento de los grandes modelos de lenguaje.)
Las reservas de varios académicos españoles
El mismo día en que se publicó el artículo, el Science Media Centre España recabó la opinión de varios investigadores del país, y las valoraciones se dividieron.
Pablo Haya Coll, investigador de la UAM, considera que el método puede producir de forma sistemática descubrimientos matemáticos de peso. Josep Curto, de la UOC, lo calificó de "a dazzling display of technical capability marred by significant methodological inconsistencies", es decir, una exhibición técnica deslumbrante pero con claras incoherencias metodológicas. Señaló tres puntos: que A y D resuelvan los mismos problemas indica que la complejidad del marco no determina necesariamente la capacidad de descubrimiento; el coste solo contabiliza las ejecuciones exitosas, y en las cuentas de B y D tampoco se incluye el gasto de inferencia del propio AlphaProof; y Lean solo garantiza que la demostración vale para “el enunciado que se ha escrito”, mientras que si ese enunciado traduce fielmente el problema original sigue dependiendo de la comprobación manual de los matemáticos, algo que el artículo admite al reconocer errores de formalización.
El director del ICMAT, Javier Aramayona, se preocupa por otra cosa: la aparición de una avalancha de resultados “que se sabe que son ciertos, pero que nadie comprende del todo”, lo que podría debilitar el eslabón de la comprensión en la investigación matemática y la formación de los jóvenes investigadores. Teodoro Calonge, de la Universidad de Valladolid, fue más directo: el campo tiene todavía un margen de mejora considerable.
Los propios autores delimitan el alcance: la tasa de éxito global de la IA en los problemas de Erdős ronda entre el 1 % y el 2 %, los resueltos son en su mayoría relativamente fáciles y se concentran en combinatoria, optimización convexa y teoría de números, áreas donde la biblioteca Mathlib está más desarrollada y los problemas se descomponen mejor en subobjetivos. Los problemas que exigen inventar mucha teoría nueva quedan prácticamente fuera del alcance del sistema.
Unir los hechos de este año
En mayo informamos de que un modelo de OpenAI había resuelto una conjetura de Erdős de 80 años; en septiembre estalló una disputa de autoría entre matemáticos y OpenAI; el 6 de octubre, OpenAI publicó de golpe en GitHub 722 manuscritos matemáticos generados por IA, en un repositorio de código abierto con licencia Apache 2.0 y sin pasar por ninguna revista. Según The Decoder, un grupo de matemáticos encabezado por Terence Tao pidió después boicotear esta práctica.
La diferencia entre las dos compañías queda clara. OpenAI apuesta por el volumen y la apertura, y deja que la comunidad haga la criba; DeepMind apuesta por muchos menos resultados, pero cada uno pasó por el compilador de Lean y por la revisión de una revista. En cuanto al papel de Lean, DeepMind es bastante comedida en el artículo; la frase original dice que la verificación formal "can serve as a filter for determining which proofs merit human review", es decir, sirve para decidir qué demostraciones merecen que una persona las lea.
Un cálculo a grandes rasgos: a unos cientos de dólares por problema, el coste de inferencia de los 9 problemas de Erdős queda muy por debajo del sueldo mensual de un posdoctorando; pero cuánto subiría la cuenta con el criterio señalado por Curto, al sumar las ejecuciones fallidas y las llamadas a AlphaProof, es algo que el artículo todavía no cuantifica. DeepMind ha dejado las demostraciones y parte de las explicaciones en el repositorio alphaproof-nexus-results de GitHub, para que matemáticos externos puedan contrastarlas una por una.
Fuentes: artículo de la revista Science, The Decoder, CocoLoop, valoraciones de expertos del Science Media Centre España; el texto del artículo se contrastó en cuanto a los 9 problemas resueltos de 353 de Erdős, las 44 conjeturas demostradas de 492 de la OEIS y el reparto de funciones de las cuatro versiones de agentes.