¿Son nuevas las nueve demostraciones de DeepMind?

Una demostración matemática puede estar escrita con elegancia y, aun así, esconder un fallo que nadie detecte durante años. El agente de inteligencia artificial AlphaProof Nexus, de Google DeepMind, demostró nueve problemas planteados por Paul Erdős, y un programa verificó cada paso. El trabajo apareció primero en un preprint de mayo (arXiv) y, tras la revisión por pares, se publicó en Science el 8 de octubre (Science). El programa podía confirmar la lógica, pero decidir si esa lógica aportaba algo nuevo correspondía a los matemáticos.

Un árbitro al que no se puede convencer con elocuencia

Los chatbots saben escribir matemáticas que parecen correctas. Un párrafo convincente puede ocultar un paso que falta, y solo una lectura atenta permite descubrirlo. AlphaProof Nexus evita ese problema al trabajar con Lean, un lenguaje de programación que permite formular definiciones, afirmaciones y demostraciones con tal precisión que un ordenador puede verificarlas.

Lean es como un árbitro que lee cada línea de una demostración completa y aplica reglas fijas. El estilo no cuenta. Si un paso no se deduce de los anteriores, la demostración falla, por elegante que parezca el resto.

El equipo describe el agente como un sistema que busca demostraciones escritas en Lean. Los investigadores también le dieron acceso a AlphaProof, un sistema anterior de DeepMind diseñado específicamente para demostrar teoremas. En las pruebas del equipo, una configuración más sencilla obtuvo los mismos resultados: un modelo de lenguaje combinado con Lean, sin AlphaProof, también resolvió los nueve problemas de Erdős (The Decoder). Para esos problemas, el componente especializado resultó innecesario.

El artículo presenta demostraciones aceptadas de las nueve afirmaciones de Erdős y de 44 conjeturas, es decir, afirmaciones que se consideran ciertas pero aún no se han demostrado, incluidas en Online Encyclopedia of Integer Sequences, un amplio catálogo de patrones numéricos (Science). Entre los resultados de Erdős figura una pregunta de dos partes sobre números enteros que el matemático planteó junto con András Sárközy en 1970. Permaneció abierta durante más de medio siglo (ABC).

Lo que el árbitro no puede ver

La garantía de Lean tiene un límite preciso: confirma que una demostración establece exactamente la afirmación tal como está escrita en el código. Hay tres cuestiones que quedan fuera de su alcance: si el código recoge lo que Erdős quería decir, si alguien había respondido a la pregunta hace tiempo y si la respuesta aporta algo al conocimiento matemático.

El problema de 1970 muestra por qué importan las dos últimas cuestiones. La segunda parte implica la primera, así que una sola demostración resuelve ambas. Cuando empezaron a circular las pruebas del agente, se descubrió que bastaba con introducir un pequeño ajuste en una construcción del artículo original de 1970 para responder también a las dos partes (arXiv). Las demostraciones del agente eran correctas. El problema, sencillamente, estaba más cerca de resolverse de lo que sugería su etiqueta de «abierto».

Para detectar este tipo de detalles hacen falta especialistas en la materia. Gergely Bérczi, matemático de Aarhus University en Dinamarca y uno de los autores, ayudó a elegir preguntas adecuadas y a validar las soluciones (Aarhus University). También colaboró en la redacción de versiones de las demostraciones que pudieran seguir los lectores. Lean avaló cada paso; Bérczi y sus colegas juzgaron qué aportaba el conjunto.

Esa división del trabajo distingue este estudio de un hito del mes pasado. Entonces, Claude, el sistema de Anthropic, convirtió a Lean una demostración ya conocida del último teorema de Fermat (To Brief). La traducción de una demostración célebre no plantea dudas sobre su novedad. Buscar entre afirmaciones que se consideran abiertas sí las plantea; en ese caso, comprobar la novedad pasa a ser la tarea principal.

El equipo ha publicado los archivos de las demostraciones para que otros puedan pasarlos por el mismo árbitro (GitHub). El avance que muestra el estudio es concreto: un agente de inteligencia artificial produjo demostraciones verificables por ordenador de algunas afirmaciones que los matemáticos consideraban abiertas, y la garantía se limita a esas afirmaciones tal como están formuladas en Lean. Determinar qué aportaba cada demostración a las matemáticas siguió siendo tarea de quienes las leyeron.