Lean valida la prueba de Fermat de Claude

Lean, el programa de verificación de demostraciones que utilizan matemáticos de todo el mundo, ha aceptado una versión formal completa del último teorema de Fermat. La formalización, generada por el sistema Claude de Anthropic y publicada en un repositorio abierto, no contiene pasos provisionales sin resolver, axiomas adicionales ni atajos computacionales ajenos a los fundamentos habituales de Lean (repositorio). Kevin Buzzard, matemático del Imperial College London que dirigía su propio proyecto de formalización, compiló el trabajo por separado y confirmó su validez; lo calificó como «un logro extraordinario de formalización automática» (Buzzard).

El problema matemático se resolvió hace tiempo. Andrew Wiles demostró el teorema en 1995 y ningún matemático serio ponía en duda el resultado. Quedaba, sin embargo, reescribir aquella demostración como una serie de instrucciones para un verificador literal, con todas las definiciones y los pasos intermedios que un autor puede dar por supuestos. Anthropic asegura que decenas de agentes de inteligencia artificial completaron esa traducción en once días de agosto, trabajando en paralelo mediante una plataforma denominada Prove2Me (Anthropic).

Ese plazo corresponde a un proceso que nadie ajeno a Anthropic puede reproducir. La publicación no incluye el modelo interno, la infraestructura de coordinación, las decisiones de los operadores ni el gasto computacional. Sí permite reproducir el resultado final: cualquiera que disponga de equipos suficientes puede volver a compilar el proyecto en Lean y confirmar que la demostración supera la verificación. Anthropic también la comprobó con otro verificador escrito en Rust, que determinó que las 1.052.234 declaraciones del artefacto formal eran coherentes (informe técnico). Se trata de una segunda lectura del mismo texto, no de una reconstrucción independiente del trabajo realizado durante esos once días.

Cómo trabajaron los agentes

Formalizar una demostración consiste en reescribir el razonamiento de un matemático para que un programa sin intuición matemática pueda confirmar cada paso lógico. El enunciado del teorema parece sencillo: para cualquier exponente entero igual o superior a tres, no existen tres enteros positivos que satisfagan aⁿ + bⁿ = cⁿ. Su demostración, en cambio, atraviesa capas profundas de teoría de números a lo largo de cientos de páginas.

Claude no descubrió matemáticas nuevas. Formalizó la cadena de resultados ya conocida que conduce a la demostración de Wiles, siguiendo una exposición de los matemáticos Henri Darmon, Fred Diamond y Richard Taylor (Anthropic, informe técnico). La idea creativa correspondió a Wiles y a sus predecesores. La aportación de Claude fue traducirla a unos 10,5 millones de líneas de código verificable por una máquina (informe técnico).

La plataforma Prove2Me, diseñada por el investigador de Anthropic Tianyi Peng junto con colaboradores de Columbia University, dividió la demostración en un grafo de dependencias compuesto por unas 29.511 afirmaciones independientes (informe técnico). Los agentes escogían las que estaban listas, escribían sus demostraciones en Lean y comprobaban las formulaciones propuestas por otros agentes, todo ello en paralelo. La operación consumió unos 6.000 millones de tokens de salida de un modelo interno de investigación (informe técnico).

Según Anthropic, los operadores humanos no escribieron código de Lean durante el proceso, aunque eligieron el teorema, facilitaron la vía de demostración conocida, diseñaron la infraestructura de agentes y reajustaron ocasionalmente las prioridades (Anthropic). La empresa no publicó la transcripción completa de las intervenciones ni los costes computacionales.

A partir de años de trabajo humano

El resultado se apoyó en Mathlib, la gran biblioteca de matemáticas formalizadas que mantiene la comunidad, y utilizó directamente dos proyectos anteriores. El equipo de Buzzard en Imperial trabajaba desde finales de 2023 en una formalización del último teorema de Fermat en Lean, financiada con una ayuda de un millón de libras del EPSRC prevista hasta 2029 (ayuda del EPSRC). Otro proyecto comunitario ya había formalizado el teorema para un subconjunto de casos. El archivo de atribuciones de Anthropic identifica 106 ficheros con material tomado o adaptado de esos trabajos (atribuciones).

La ejecución en paralelo impide comparar los once días naturales con las horas de trabajo acumuladas por el equipo de Buzzard, que llevaba unos 22 meses financiados cuando comenzó la operación de Claude (ayuda del EPSRC). Anthropic no reveló las horas de uso de procesadores gráficos ni el consumo energético.

Hasta esta publicación, el último teorema de Fermat era el único problema pendiente en la lista de Freek Wiedijk de cien teoremas importantes por formalizar, una referencia que lleva dos décadas registrando los avances en este campo (Buzzard).

La prueba más exigente de que este método puede generalizarse llegará con la formalización de matemáticas recientes y peor documentadas, para las que no existan una hoja de ruta, bibliotecas maduras ni trabajos formales anteriores. Este ejercicio abordó un teorema célebre que ya contaba con una infraestructura considerable. Demuestra que los agentes de inteligencia artificial pueden producir una formalización completa, aceptada por Lean y verificable por terceros, cuando disponen de una vía de demostración conocida y de trabajo formal previo. Los materiales publicados, sin embargo, no permiten reproducir el proceso que la generó.