Formalizando el Último Teorema de Fermat en Lean: Un Proyecto de Código Abierto Colaborativo

Una colaboración internacional liderada por Kevin Buzzard está llevando a cabo la ambiciosa tarea de probar formalmente el Último Teorema de Fermat utilizando el verificador de teoremas Lean. Financiado por el Consejo de Investigación de Ingeniería y Ciencias Físicas del Reino Unido y alojado en el Imperial College London, este proyecto expande los límites de la verificación de pruebas matemáticas. Al usar una computadora para verificar la prueba, el proyecto explora el potencial de la formalización y la verificación automatizada en matemáticas, con implicaciones para futuras investigaciones.