Computer-assisted proofs, proof assistants and visualization in dynamical systems
timetable:
Fri 21 Jun, 10:10 - 11:00, Aula Dini
<< Go back
Formalizing topological entropy in Lean
speaker: Damien Thomine (Université Paris-Saclay)abstract: I will present a project to formalize some elements of topological dynamics in Lean, and its current advancement. A special emphasis will be given to many design decisions, and how they arise from the interaction between a well-established mathematical theory and a proof assistant.
timetable:
Fri 21 Jun, 10:10 - 11:00, Aula Dini
<< Go back