Speaker
Damien Thomine
(Université Paris-Saclay)
Description
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.
