La IA convierte el último teorema de Fermat en la mayor demostración realizada hasta ahora en Lean

El último teorema de Fermat se ha traducido por primera vez a código verificable por ordenador, dando lugar a una demostración formal de 13 millones de líneas en solo 11 días. Un grupo de agentes de IA desarrolló unos 29.500 teoremas intermedios necesarios para completar el trabajo en Lean, un lenguaje de programación diseñado para verificar la lógica matemática.

El logro no sustituye ni amplía la demostración humana que Andrew Wiles y Richard Taylor completaron en la década de 1990. En cambio, convierte ese razonamiento ya establecido en un formato que un ordenador puede comprobar paso a paso. El teorema afirma que no hay números enteros que satisfagan aⁿ + bⁿ = cⁿ cuando n es mayor que 2.

Expertos humanos proporcionaron ocasionalmente orientación general. Al principio, los agentes tuvieron dificultades para coordinarse, pero lo consiguieron tras utilizar Prove2Me, una herramienta de colaboración que les ayudó a llevar un registro de las tareas completadas y a elegir cuáles abordar a continuación. El matemático Kevin Buzzard compiló el código resultante y ejecutó las comprobaciones estándar de Lean, y concluyó que realmente desarrolla las matemáticas necesarias.

La formalización tiene más de cinco veces el tamaño de Mathlib, la principal biblioteca compartida de matemáticas de Lean. Su escala sugiere que la IA podría ayudar pronto a convertir grandes partes de la literatura matemática en código verificable, aunque revisar resultados tan extensos y hacerlos comprensibles para las personas sigue planteando desafíos considerables.