Según Anthropic: el último teorema de Fermat, formalizado en Lean

El momento decisivo de este proyecto sobre Fermat no tiene nada de espectacular: en Lean, una demostración compila o no compila. En el repositorio de GitHub de Anthropic hay ahora, según la empresa, una versión completamente verificada por ordenador del último teorema de Fermat. El matemático Kevin Buzzard ya ha compilado personalmente el código y ejecutado el comparador correspondiente.

Desde el punto de vista matemático, el teorema no es nuevo. Andrew Wiles demostró en 1995, en 129 páginas, que la ecuación xⁿ + yⁿ = zⁿ no tiene soluciones enteras para exponentes enteros n > 2. Lo novedoso es la formalización: la demostración se traduce a código de modo que un ordenador pueda controlar cada paso, en lugar de confiar en pasos intermedios omitidos por resultar evidentes para los seres humanos.

Lean es a la vez lenguaje de programación y sistema de verificación. Las afirmaciones matemáticas y sus demostraciones se comprueban con arreglo a un conjunto fijo de reglas lógicas; si queda siquiera un vacío, la demostración no compila. Por tanto, la confianza debe depositarse sobre todo en el pequeño núcleo de Lean y sus axiomas. Sin embargo, la biblioteca disponible Mathlib limita el margen de acción a la parte de las matemáticas que ya ha sido formalizada.

Según Anthropic, docenas de agentes de Claude trabajaron durante once días en una versión simplificada de la demostración de Wiles basada en el trabajo de Darmon, Diamond y Taylor. El resultado fueron 13 millones de líneas de código Lean y unas 29.500 teorías intermedias. Según la empresa, los primeros equipos fracasaron a la hora de mantener una visión general del proyecto; el trabajo solo avanzó con Prove2Me, una plataforma desarrollada por el grupo de Tianyi Peng en la Universidad de Columbia que gestiona los siguientes pasos de la demostración en un grafo dirigido acíclico. Según Anthropic, el esfuerzo ascendió a unos seis mil millones de tokens de salida; a partir de esa cifra pueden calcularse unos costes de entre 100.000 y 300.000 dólares estadounidenses.

Esto ya cambia algo concreto para la formalización de la literatura matemática: terceros pueden compilar el código publicado y comprobar la cadena lógica. Esto permite una verificación técnicamente reproducible, pero no sustituye una evaluación independiente, que hasta ahora sigue pendiente en gran medida. Buzzard considera que la formalización supone un gran paso hacia la formalización automática de las matemáticas modernas; al mismo tiempo, sigue la literatura temprana y no aporta ninguna afirmación matemática nueva sobre el último teorema de Fermat.