Claude formaliza el Teorema de Fermat: 11 días, 13M líneas Lean

Por qué el Último Teorema de Fermat sigue siendo el examen perfecto

En algún momento alrededor de 1637, Pierre de Fermat escribió al margen de su copia de la Aritmetica de Diofanto que no existían enteros positivos a, b, c que satisficieran aⁿ + bⁿ = cⁿ para n > 2. Junto a la afirmación añadió la frase que dio inicio a una obsesión de 350 años: "he descubierto una demostración verdaderamente maravillosa, que este margen es demasiado estrecho para contener". Esa demostración nunca apareció, y la comunidad matemática lleva siglos intentando reconstruirla.

La primera prueba válida la publicó Sir Andrew Wiles en mayo de 1995 (con ayuda posterior de Richard Taylor), tras un intento fallido presentado en junio de 1993 en el que un revisor encontró un hueco crítico. La prueba ocupa 129 páginas y depende de maquinaria algebraica que Fermat jamás pudo haber conocido. En 1908 se ofrecieron 100.000 marcos de oro alemanes (equivalentes, según Anthropic, a entre 1 y 2 millones de dólares actuales) por una demostración correcta; solo en el primer año se registraron 621 intentos incorrectos.

Formalizar esa demostración —convertirla a un lenguaje que un computador pueda verificar paso a paso— era hasta hace poco un trabajo que el consenso matemático esperaba medir en años. El propio Kevin Buzzard, matemático de Imperial College London que lidera un proyecto comunitario de formalización lanzado en 2023 con apoyo del EPSRC británico, ha dicho públicamente que dudaba de poder terminarlo en su horizonte de cinco años, según reportó Science News.

Qué hizo Claude exactamente: 11 días, 13 millones de líneas y 29.500 teoremas

Anthropic publicó que Claude produjo en 11 días la primera demostración completa de extremo a extremo del Último Teorema de Fermat verificable por computador. Los números que la acompañan dan la medida del salto:

• 13 millones de líneas de Lean en la prueba final, más de 5 veces el tamaño de Mathlib, la biblioteca comunitaria sobre la que se construye.
• 29.500 teoremas intermedios incorporados en la prueba final, sobre un total de 30.300 demostrados a lo largo del proceso.
• ~6 mil millones de tokens de salida consumidos por un modelo interno de investigación roughly comparable to Claude Fable 5.1, según describe Anthropic.
• Demostración construida sobre la exposición simplificada de Henri Darmon, Fred Diamond y Richard Taylor, que es la versión que ha guiado todo el trabajo comunitario de formalización.

El documento afirma que la demostración fue verificada por Lean y que solo utiliza los tres axiomas estándar del asistente de pruebas. Un comparador confirmó además que el enunciado coincide exactamente con el de Mathlib para el Último Teorema de Fermat.

La pila técnica: Prove2Me, agentes Claude Code y un humano con instrucciones de alto nivel

El proyecto no fue obra de un único Claude en una sola sesión. Anthropic describe una arquitectura multi-agente basada en Claude Code, en la que docenas de agentes colaboraron para definir conceptos, demostrar teoremas intermedios y encadenarlos hacia arriba. La capa de coordinación es Prove2Me, una plataforma abierta de formalización diseñada por Tianyi Peng, investigador de Anthropic cuyo grupo en la Universidad de Columbia construye herramientas para formalización con IA, junto con colaboradores de esa universidad.

Los intentos iniciales fallaron: los agentes tenían cierto éxito temprano pero perdían el estado del proyecto y dejaban de coordinarse. Anthropic estima que esos intentos fallidos contribuyeron alrededor del 7% de las líneas no boilerplate de la prueba final. La arquitectura funcionó al migrar a Prove2Me.

La intervención humana fue deliberadamente mínima. Las instrucciones de Tianyi Peng eran indicaciones de alto nivel, del tipo "Jacobian as a scheme sounds high priority" o "push [the] Mazur [theorem] to be done soon". No dirigió líneas de Lean: dirigió prioridades.

La revisión independiente: Buzzard y la marca de agua humana

Anthropic envió la demostración a Kevin Buzzard para revisión externa. Su veredicto, citado en el anuncio, resume el alcance del trabajo:

"This extraordinary autoformalization achievement, which Anthropic researchers say only took 11 days, proves Fermat's Last Theorem with no assumptions other than the axioms of mathematics. Along the way we see autoformalization of algebra, harmonic analysis, geometry and number theory, and we learn that AI autoformalization artefacts are now robust enough to be built upon; the proof is multi-layered."

Buzzard añadió que, si la autoformalización del FLT es ya posible, estamos ante "un gran paso hacia la autoformalización de la literatura matemática moderna", con herramientas para detectar errores en el corpus matemático y aligerar la carga de los revisores.

Lo que esto cambia para la investigación matemática

El anuncio contrasta deliberadamente este trabajo con la reciente oleada de resultados de IA sobre la hipótesis de Riemann, donde la IA produjo matemática novel. Aquí lo nuevo no es el contenido: la prueba es la conocida de Wiles. Lo nuevo es la verificación, equivalente a comprobar una demostración matemática como se comprueba un cálculo con calculadora.

Anthropic lo enmarca como infraestructura: si cada nueva demostración matemática se acompaña de una versión formalizada, los referees humanos pueden centrarse en las ideas grandes en lugar de dedicar meses a verificar detalles. Para la comunidad que ya trabaja con Lean —el asistente de pruebas creado por Leonardo de Moura en Microsoft en 2013, según recoge Science News— esto valida una tesis que llevan años defendiendo.

El propio documento incluye un experimento adicional: con tres suscripciones personales Claude Max y colaboración exclusivamente a través de Prove2Me, los agentes formalizaron el Teorema de los Tres Primos de Vinogradov mediante aplicaciones del Método del Círculo de Hardy-Littlewood en tres días. Anthropic lo presenta como señal de que la formalización colaborativa de resultados mayores con suscripciones de consumo es viable con el andamiaje adecuado.

¿Qué significa esto para tu startup?

Aunque el protagonista sea una conjetura del siglo XVII, las implicaciones para founders que construyen sobre IA son inmediatas.

• La verificación automatizada de razonamiento complejo ya no es promesa, es producto. Si Claude puede mantener la coherencia lógica sobre 13 millones de líneas durante 11 días, los patrones de uso son extrapolables a auditorías de código, due diligence técnica sobre codebases grandes, o validación de pipelines regulatorios en fintech y salud.
• Multi-agente + andamiaje especializado es la arquitectura que funciona. El proyecto fracasó en sus primeras iteraciones porque los agentes perdían el estado; triunfó al migrar a una plataforma diseñada para coordinar (Prove2Me). Tu propia arquitectura agentic necesita un harness —un armazón de coordinación— antes que más potencia bruta.
• La economía de la investigación cambia. Anthropic ofrece créditos de investigación y suscripciones gratuitas o con descuento a matemáticos externos. El precedente indica que la estrategia de los grandes laboratorios será subsidiar investigación adyacente para acelerar la siguiente generación de benchmarks; founders en sectores adyacentes (educación, biotech, materiales) pueden aprovechar esos programas antes que sus competidores.

Fuentes

• Anthropic — Formalizing Fermat's Last Theorem (fuente original)
• Science News — Math long resisted a digital disruption. AI is poised to change that