Matemáticos buscan una prueba por computadora del enigma de 350 años: el último teorema de Fermat
(dongascience.com)El último teorema de Fermat se volverá a demostrar en un lenguaje de computadora
- El profesor Kevin Buzzard, del Imperial College London, planea escribir una prueba formal del último teorema de Fermat (FLT) usando el demostrador de teoremas Lean a partir de octubre de 2024.
- El Engineering and Physical Sciences Research Council[EPSRC] del Reino Unido decidió financiar al profesor Buzzard durante cinco años a partir de ese mes.
- Está previsto que a finales de abril de 2024 se publique un plan del proyecto creado con Lean blueprints, un plugin de plasTeX.
¿No estaba ya demostrado el último teorema de Fermat?
Sí, ya fue demostrado. El matemático británico Andrew Wiles publicó la demostración en 1994, y esta fue publicada oficialmente en 1995. Sin embargo, todavía no existe una prueba formal escrita en el lenguaje de los demostradores interactivos de teoremas[ITP].
¿Demostrador interactivo de teoremas? ¿Prueba formal? ¿Qué es eso?
- Demostrador interactivo de teoremas[ITP]: programa de computadora que ayuda a las personas a escribir pruebas formales. También se le llama asistente de pruebas [proof assistant].
- Prueba formal: una prueba que puede ser verificada por un programa de computadora llamado verificador de pruebas [proof verifier]. Los asistentes de pruebas normalmente también cumplen la función de verificadores de pruebas.
¿Un demostrador de teoremas es inteligencia artificial?
El demostrador neuronal de teoremas[NTP] podría considerarse como tal, pero muchos demostradores interactivos de teoremas, incluido Lean, no son programas basados en aprendizaje automático.
Preséntame el demostrador de teoremas Lean.
- Es a la vez un demostrador interactivo de teoremas y un lenguaje de programación funcional puro.
- Está basado en teoría de tipos dependientes.
- Tiene funciones como clases de tipos, sintaxis extensible, macros y metaprogramación.
- En comparación con otros asistentes de pruebas, entre los usuarios de Lean hay especialmente muchos matemáticos (que investigan áreas fuera de los fundamentos de las matemáticas).
¿Por qué quieren escribir una prueba formal del último teorema de Fermat?
Citando una publicación en X del profesor Kevin Buzzard: "para hacer que las computadoras entiendan la teoría moderna de números y, con el tiempo, puedan ayudar a los teóricos de números".
Enlaces
- Mensaje que el profesor Kevin Buzzard publicó en el chat de Zulip de Lean el 3 de octubre de 2023: https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/…
- Biblioteca matemática de Lean: https://github.com/leanprover-community/mathlib4
- Artículo de New Scientist: https://institutions.newscientist.com/article/…
- Artículo de Popular Mechanics: https://popularmechanics.com/science/math/…
1 comentarios
Los apoyo. Si les interesa la
formal proof, también les recomiendo escuchar la clase Machine Assisted Proofs del profesor Terrence Tao (https://www.youtube.com/watch?v=AayZuuDDKP0).