Anthropic afirma que Claude formalizó el último teorema de Fermat en Lean

Anthropic anunció el 4 de septiembre de 2026 que Claude produjo en gran medida de forma autónoma la primera prueba completa del último teorema de Fermat verificada por ordenador. El modelo trabajó durante 11 días para escribir la demostración en el lenguaje de programación Lean.

El sistema generó 13 millones de líneas de código Lean y demostró 29.500 teoremas intermedios utilizados en la prueba final. En total, produjo pruebas verificables por ordenador para 30.300 teoremas. Decenas de agentes de Claude colaboraron en la definición de conceptos, la demostración de resultados intermedios y la construcción de afirmaciones cada vez más complejas.

La formalización sigue una versión simplificada de la demostración de Andrew Wiles, basada en el trabajo de Darmon, Diamond y Taylor. Anthropic indica que la intervención humana se limitó a instrucciones ocasionales de alto nivel proporcionadas por Tianyi Peng, investigador de la empresa.

El trabajo se completó mediante Prove2Me, una plataforma colaborativa abierta para formalizar matemáticas desarrollada por Tianyi Peng y sus colaboradores en Columbia University. La plataforma organizó las afirmaciones en un grafo dirigido acíclico, facilitó el trabajo paralelo de los agentes y permitió buscar y reutilizar teoremas mediante descripciones en lenguaje natural.

Anthropic compartió el resultado con Kevin Buzzard, quien señaló que el logro muestra que la autoformalización puede aplicarse a álgebra, análisis armónico, geometría y teoría de números, y que estos artefactos pueden servir como base para desarrollos posteriores. La empresa distingue este avance de trabajos recientes sobre la hipótesis de Riemann: en este caso, la novedad principal es la verificación computerizada de una demostración matemática ya conocida.

Fuente: Anthropic.