Compartimos la primera prueba completa verificada por computadora del último teorema de Fermat. Claude trabajó en gran medida de forma autónoma durante 11 días para escribir la prueba en el lenguaje de programación Lean. A continuación, describimos cómo se realizó la formalización y compartimos algunas reflexiones sobre lo que este trabajo podría significar para las matemáticas de investigación.

Alrededor de 1637, Pierre de Fermat anotó una afirmación en el margen de su copia de la Arithmetica de Diofanto que se convertiría en una de las conjeturas matemáticas más famosas de todos los tiempos: no hay enteros positivos a, b, c que satisfagan aⁿ + bⁿ = cⁿ para ningún n > 2. El último teorema de Fermat (FLT), como se conoció la conjetura, resultó increíblemente difícil de probar. La primera prueba, de Sir Andrew Wiles en 1995, tenía 129 páginas y requirió meses de trabajo minucioso para verificar.

Una década después, el informático holandés Jan Bergstra propuso “formalizar” la prueba de Wiles: convertir el razonamiento matemático en una forma que las computadoras puedan verificar automáticamente. Desde entonces, los matemáticos han estado desarrollando los métodos necesarios para codificar una prueba tan compleja, incluido un esfuerzo comunitario de varios años iniciado en 2024 por Kevin Buzzard en el Imperial College de Londres para completar la formalización utilizando el asistente de pruebas Lean.

Recientemente, Tianyi Peng, investigador de Anthropic cuyo grupo en la Universidad de Columbia construye herramientas para la formalización de IA, se propuso probar si Claude podría avanzar en la formalización de FLT. El resultado fue más allá de lo que esperaba. En 11 días, trabajando en gran medida de forma autónoma, Claude produjo la primera prueba de FLT de extremo a extremo y verificada por computadora. En el proceso, escribió 13 millones de líneas de Lean y demostró 29,500 teoremas intermedios.