Anthropic demuestra el Último Teorema de Fermat en Lean 4
Fermat's Last Theorem in Lean 4
Anthropic ha publicado una prueba completa y verificada por máquina del Último Teorema de Fermat en el asistente de pruebas Lean 4, construida sobre Mathlib. La demostración sigue el argumento de Frey, Serre, Ribet, Wiles y Taylor-Wiles, y fue verificada con tres comprobadores independientes: el kernel de Lean, el comparador de leanprover y nanoda, un kernel independiente escrito en Rust. El repositorio incluye una versión navegable en HTML y una ruta de prueba detallada. La verificación confirma que la prueba se basa únicamente en los tres axiomas estándar de Lean, sin lagunas ni axiomas adicionales.
Lo que ninguna herramienta puede comprobar es que cada teorema intermedio significa lo que su nombre sugiere; eso queda a juicio del lector, y PROOF-PATH.md nombra el teorema de Lean detrás de cada paso y establece exactamente cuán fuerte es cada resultado clásico nombrado tal como se demuestra aquí.