Anthropic informó este jueves que Claude completó la primera demostración formal y verificada por computadora del Último Teorema de Fermat, trabajando de forma mayormente autónoma durante 11 días en el lenguaje de programación Lean.
El teorema, planteado por Pierre de Fermat alrededor de 1637 y probado por primera vez por Andrew Wiles en 1995 tras casi una década de trabajo, establece que no existen enteros positivos a, b y c que satisfagan la ecuación aⁿ + bⁿ = cⁿ para ningún valor de n mayor a 2. La demostración de Wiles ocupó 129 páginas y requirió meses de verificación manual por parte de la comunidad matemática.
Según explicó Anthropic, el proyecto fue impulsado por Tianyi Peng, investigador de la compañía y de la Universidad de Columbia, quien buscaba probar si Claude podía avanzar en la formalización del teorema dentro del asistente de pruebas Lean, un esfuerzo comunitario que Kevin Buzzard, del Imperial College de Londres, había iniciado en 2024 y que se estimaba tomaría años en completarse.
En el proceso, decenas de agentes de Claude escribieron 13 millones de líneas de código en Lean y demostraron 29,500 teoremas intermedios, apoyándose en Prove2Me, una plataforma colaborativa desarrollada por Peng y su equipo que organizó el trabajo mediante un grafo de teoremas para coordinar a los agentes y evitar que perdieran el hilo del proyecto. La compañía detalló que el esfuerzo consumió alrededor de seis mil millones de tokens de salida de un modelo de investigación interno comparable a Claude Fable 5.1.
Buzzard, quien revisó la prueba final, calificó el logro como un paso importante hacia la automatización de la formalización de la literatura matemática moderna. Anthropic señaló que la demostración completa está disponible públicamente en GitHub junto con una explicación técnica del proceso.
El caso ilustra cómo los sistemas de IA empiezan a desplazar el cuello de botella de la investigación matemática de la creación de pruebas hacia su verificación automática, un cambio que Anthropic reconoce que no sustituye la exposición humana pero que podría volverse indispensable para que la comunidad científica revise al ritmo que la IA produce resultados.
