Claude completa la primera prueba formal y verificada por computadora del Último Teorema de Fermat
Trabajando de forma mayormente autónoma durante 11 días sobre la plataforma Prove2Me, agentes de Claude generaron 13 millones de líneas de código Lean y probaron más de 30,000 teoremas para cerrar el último reto de formalización de la lista de Freek Wiedijk.
Anthropic reportó que Claude produjo la primera prueba formal, de extremo a extremo y verificable por computadora, del Último Teorema de Fermat en el lenguaje Lean. El trabajo tomó 11 días de ejecución mayormente autónoma, consumió alrededor de seis mil millones de tokens de salida y generó 13 millones de líneas de código Lean, probando 30,300 teoremas -29,500 de los cuales terminaron usándose en la prueba final.
La pieza clave fue darle a Claude acceso a Prove2Me, una herramienta de código abierto que mantiene un grafo acíclico dirigido de enunciados de teoremas y coordina a múltiples agentes de Claude trabajando en paralelo sobre ese grafo. La intervención humana se limitó a instrucciones ocasionales de alto nivel de un matemático -del tipo "conviene priorizar el jacobiano como esquema" o "hay que terminar pronto el teorema de Mazur"- en vez de guiar paso a paso la demostración.
El logro cierra, además, la lista de 100 retos de formalización de Freek Wiedijk, un benchmark de facto para matemáticas formalizadas que llevaba dos décadas abierto: el Último Teorema de Fermat era el último pendiente. Para quien trabaja con asistentes de prueba como Lean, Coq o Isabelle, o construye herramientas de verificación formal, el caso sugiere que orquestar muchos agentes contra un grafo de dependencias explícito -en vez de pedirle a un solo modelo una prueba monolítica- puede ser el patrón que haga viable automatizar matemática de investigación a esta escala.