Valerio Proietti: Computer assisted proofs

Abstract: I will discuss computer assisted proofs, and in particular the formalization of mathematical statements and proofs using Lean, a free and open source programming language and interactive theorem prover. My personal opinion is that technologies of this kind will play an increasingly important role in mathematics. I will briefly introduce Lean's type theory and, if time allows it, I plan to do a walk-through formalization of the Birkhoff transitivity theorem from topological dynamics.