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í.
- black_knight
Me pregunto si alguna parte del código de Lean tiene una forma que permita contribuirla a alguna de las bibliotecas de Lean existentes. Mi experiencia es que se necesita mucha intervención humana para que Fable escriba código lo bastante bueno para una biblioteca de formalización en la que otros puedan trabajar. Pero, dado que seguramente también se han formalizado muchos prerrequisitos, sería bueno que no se desperdiciara todo el esfuerzo en una única demostración final. (Reenvío de un comentario anterior, pero creo que encaja mejor aquí)
- superposeur
Gran parte del valor de una demostración reside en el desarrollo de definiciones matemáticas y teoremas intermedios necesarios para llegar hasta ella, al estilo de Grothendieck. Esta capacidad parece aún estar más allá de la IA (al menos, no he oído que ninguna definición fundamentalmente nueva y útil, como "esquema" o "forma modular", haya surgido de la última avalancha de demostraciones con IA). PERO, me pregunto si la IA podría desarrollar también esta habilidad mediante un proceso de refactorización eficiente de una gran demostración en Lean en piezas de Lean, para luego interpretar esas piezas de nuevo en definiciones nuevas, comprensibles para los humanos y con nombres evocadores.
- mcapodici
Qué época para estar vivo.
https://github.com/anthropics/fermats-last-theorem/blob/main...
- chvid
Creo que un problema interesante, quizá incluso más interesante, sería la demostración más corta / más concisa / más fácil de entender (verificable formalmente).
- rawling
Discusión en portada: https://news.ycombinator.com/item?id=49568506