Anthropic dice que decenas de agentes de Claude han producido la primera demostración del último teorema de Fermat verificada de punta a punta por un ordenador. Tardaron 11 días, escribieron 13 millones de líneas de Lean y demostraron por el camino 30.300 teoremas intermedios. La comunidad matemática llevaba años tratando ese mismo objetivo como un proyecto de varios años.
Puntos clave
- 11 días de trabajo mayormente autónomo, con decenas de agentes de Claude corriendo en paralelo.
- 13 millones de líneas de Lean, el lenguaje en el que se escriben demostraciones que una máquina puede comprobar línea a línea.
- 30.300 teoremas intermedios demostrados, de los que 29.500 acaban entrando en la prueba final.
- El modelo no era un Claude comercial: uno interno de investigación de propósito general, comparable a Claude Fable 5.1, que quemó 6.000 millones de tokens de salida.
- Kevin Buzzard, de Imperial College London, revisó el resultado.
Qué significa formalizar un teorema
Conviene separar dos cosas que se mezclan siempre que sale esta noticia. Una es demostrar el teorema. Eso lo hizo Andrew Wiles en 1994 y nadie lo discute. Otra es formalizarlo: reescribir esa demostración en un lenguaje como Lean, donde cada paso se apoya en algo ya probado y un verificador comprueba mecánicamente que no hay huecos.
La demostración de Wiles ocupa cientos de páginas y se apoya en décadas de teoría de números. Trasladar eso a Lean sin dar nada por supuesto es un trabajo que Buzzard llevaba coordinando con voluntarios desde hace años, con horizonte de una década.
Lo que Anthropic dice haber hecho es completar esa traducción siguiendo una versión simplificada de la ruta de Wiles. Buzzard, que revisó el artefacto, lo describió como "un logro extraordinario de autoformalización que demuestra el último teorema de Fermat sin más supuestos que los axiomas de las matemáticas".
Esa frase es la parte importante. No es un modelo diciendo que ha demostrado algo. Es un fichero que un verificador lee y acepta.
Cómo lo montaron
El andamiaje se llama Prove2Me, una plataforma colaborativa abierta que diseñó Tianyi Peng, investigador de Anthropic, con colaboradores de su grupo en la Universidad de Columbia.
Prove2Me mantiene un grafo dirigido acíclico con todos los enunciados de teoremas del proyecto. Traducido: un mapa de qué depende de qué, para que los agentes no repitan trabajo ni se bloqueen esperando piezas. Además acelera la compilación de Lean, que es el cuello de botella obvio cuando manejas millones de líneas, y permite buscar y reutilizar resultados ya probados con descripciones en lenguaje natural.
Ese último detalle es el que explica el paralelismo. Un agente que necesita un lema puede preguntar por él en español o en inglés y encontrar el que otro agente demostró hace horas, en vez de rehacerlo.
Lo que Anthropic reconoce que salió regular
La prueba pesa unas cinco veces Mathlib, la biblioteca estándar de matemáticas formalizadas de Lean. Anthropic admite que es probablemente más larga de lo necesario.
El 7% de las líneas viene de intentos fallidos que quedaron dentro. Y el consumo de tokens fue brutal: 6.000 millones de salida para un solo proyecto.
Eso dibuja bien el estado del arte. La máquina llega al final, pero por un camino que ningún matemático humano firmaría por estética. Funciona porque el verificador no juzga elegancia, solo corrección.
Dónde encaja esto
En julio contamos que Claude Fable 5 tumbó una conjetura abierta desde 1939 con un contraejemplo. En agosto, que Axiom formalizó en Lean 4 el teorema de los huecos entre primos con revisión humana. Y la semana pasada, que Anthropic lanzó Fable 5.1 y Mythos 5.1 recortando el precio de la caché un 75%.
Las tres piezas apuntan al mismo sitio. Las matemáticas formales son el único dominio donde un agente puede trabajar días seguidos sin supervisión y el resultado se valida solo. No hay opinión, no hay alucinación que sobreviva al compilador.
Por qué importa
Si diriges una empresa, el titular no es Fermat. Es que hay una clase de trabajo donde la verificación es automática, y ahí los agentes ya corren solos durante días.
Piensa en qué procesos tuyos se parecen a eso. Conciliación contable, validación de datos maestros, comprobación de que un cálculo de IVA cuadra en catorce países. Tareas donde existe un criterio mecánico de "esto está bien o está mal", sin que haga falta que una persona lea el resultado para juzgarlo.
En esos casos puedes soltar la correa. En los demás sigues necesitando a alguien revisando, y por eso el mismo modelo que formaliza a Fermat todavía no puede cerrar tu mes sin que nadie lo mire. La diferencia no está en la inteligencia del modelo, está en si tienes un verificador.
Fuente original: Anthropic
Relacionado
