Claude formaliza la prueba del Último Teorema de Fermat

Anthropic anunció el 4 de septiembre que sus modelos Claude formalizaron una prueba completa y verificable por computadora del Último Teorema de Fermat, una tarea que la comunidad matemática esperaba que tomara varios años de trabajo humano.

El proyecto, liderado por el investigador Tianyi Peng, empleó decenas de agentes de Claude trabajando en paralelo en Prove2Me, una plataforma para traducir argumentos matemáticos al lenguaje de pruebas Lean. En 11 días, los agentes produjeron cerca de 13 millones de líneas de código Lean, demostrando unos 29.500 teoremas intermedios, una formalización unas cinco veces mayor que toda la biblioteca matemática existente de Lean, Mathlib. Anthropic indicó que el trabajo consumió cerca de 6.000 millones de tokens de salida de un modelo de investigación interno de propósito general con capacidades comparables a Claude Fable 5.1.

El Último Teorema de Fermat, propuesto por primera vez en 1637, establece que ningún trío de enteros positivos puede satisfacer la ecuación a^n + b^n = c^n para un entero n mayor que 2. Andrew Wiles lo demostró en 1995 tras años de trabajo, pero su prueba, como la mayoría de las matemáticas avanzadas, estaba escrita en lenguaje natural y dependía de que lectores y revisores detectaran errores. La formalización convierte ese razonamiento en una forma que un asistente de pruebas como Lean puede verificar línea por línea, usando solo los tres axiomas lógicos estándar de Lean, eliminando la dependencia de la revisión humana para confirmar la corrección.

Por qué ahora: Anthropic publicó la formalización en GitHub y dijo que una herramienta comparadora independiente confirmó que el enunciado final del teorema coincide con la formulación matemática estándar, atendiendo a una preocupación común de que un sistema de IA pudiera formalizar un enunciado más fácil y sutilmente distinto del que afirma probar.

Por qué importa: Kevin Buzzard, matemático del Imperial College de Londres y voz destacada en la comunidad de formalización, dijo que el resultado muestra que la autoformalización ahora tiene éxito en álgebra, análisis armónico, geometría y teoría de números, no solo en problemas aislados y sencillos. Verificar a mano una prueba matemática importante puede llevarle años a los matemáticos, como ocurrió con el trabajo original de Wiles. Si los sistemas de IA pueden convertir de forma fiable pruebas humanas densas en formalizaciones verificables por máquina, podrían darle al campo una vía más rápida y confiable para confirmar que los nuevos resultados son correctos, y permitir que los sistemas de IA aborden problemas sin resolver con resultados que otros matemáticos puedan verificar rápidamente en vez de confiar solo en la reputación.

Aviso: El proceso editorial de NewUJ utiliza los modelos Claude de Anthropic.