Speaker
Prof.
Sébastien Gouëzel
(CNRS and Université de Rennes)
Description
Interactive theorem provers are a kind of programming languages in which one explains proofs to a computer in a formal language, where the computer checks that the proof respects the rules of logic. I will present the Lean theorem prover, together with its mathematics library Mathlib. This library is advanced enough that one may start to formalize complicated statements in dynamics (and all other areas of mathematics!)
