Anthropic indica que Claude ha completado la primera prueba formal completa del último teorema de Fermat. No se trata de un redescubrimiento del teorema, sino de reescribir la prueba existente como código lógico verificable línea por línea por una computadora. La empresa afirma que este trabajo tomó 11 días y generó aproximadamente 13 millones de líneas de contenido.
El significado de la prueba formal consiste en escribir argumentos matemáticos en un lenguaje verificable por máquina. Las pruebas en artículos tradicionales a menudo requieren una revisión prolongada por pares, y si existe una falla en algún paso intermedio, el proceso de corrección puede durar meses e incluso años. El Último Teorema de Fermat fue demostrado por el matemático británico Andrew Wiles en 1995, pero convertir completamente esta demostración en una versión verificable por máquina se ha considerado siempre un proyecto de ingeniería intensiva.
11 días para alcanzar el objetivo del proyecto a largo plazo
El matemático del Imperial College de Londres, Kevin Buzzard, ha impulsado el proyecto desde 2024, con el mismo objetivo de reescribir la demostración de Wiles en el asistente de prueba Lean. Según el plan original, este trabajo requiere una colaboración a largo plazo, con fondos asignados hasta 2029.
Anthropic afirmó que Claude completó con anticipación este objetivo similar. Tras revisarlo, Buzzard indicó que esta demostración puede sostenerse sin depender de supuestos adicionales, es decir, se verifica únicamente sobre el sistema axiomático más básico de las matemáticas.
Realizado en paralelo por múltiples agentes
Según Anthropic, el equipo de Tianyi Peng de la Universidad de Columbia hizo que múltiples agentes de Claude trabajaran en paralelo, encargándose cada uno de escribir definiciones y demostrar conclusiones más pequeñas, y luego ensamblarlas progresivamente en estructuras de prueba más grandes. La intervención humana fue mínima, consistiendo principalmente en establecer prioridades por etapas.
Los avances iniciales no fueron fáciles. Anthropic indicó que algunos agentes no podían compartir temporalmente el contenido completado y repetían el trabajo. Posteriormente, el equipo utilizó una herramienta llamada Prove2Me para proporcionar a cada agente una lista unificada de tareas y un método de organización de archivos, además de conservar notas en lenguaje natural que les ayudaran a reutilizar los resultados de los demás.
- Más de 30,000 teoremas de soporte
- El consumo total ha alcanzado miles de millones de tokens
- Finalmente se demostraron aproximadamente 13 millones de líneas
Enfócate en lo verificable, no en nuevos teoremas.
El enfoque de este logro no radica en descubrir nuevas proposiciones matemáticas, sino en convertir demostraciones importantes ya existentes en versiones verificables paso a paso por computadora. A medida que aumentan los artículos matemáticos y el contenido generado por IA, el costo de revisar manualmente cada demostración también crece, lo que ha aumentado la atención hacia las herramientas de formalización.
Anthropic también indicó que esta prueba es más de cinco veces más grande que la biblioteca compartida utilizada comúnmente en la comunidad matemática, Mathlib. El archivo completo ya se ha subido a GitHub, y los investigadores pueden continuar revisando línea por línea su estructura y corrección.