Tórtola Vivo, Francisco2023-12-192023-12-192023-12-18https://hdl.handle.net/10115/27470Trabajo Fin de Grado leído en la Universidad Rey Juan Carlos en el curso académico 2023/2024. Directores/as: Juan Manuel Serrano HidalgoEn este trabajo se explica el funcionamiento de Lean, un asistente de verificación formal de teoremas matemáticas, para ello se ven demostraciones en distintos ámbitos de las matemáticas. También se ve funcionalidad de este lenguaje y se explican conceptos de los asistentes de demostración.spaDemostraciónLeanAsistente de verificaciónFormalizaciónProgramación funcionalTipos dependientesLenguaje de demostracióninfo:eu-repo/semantics/studentThesisinfo:eu-repo/semantics/embargoedAccess