The goal of this talk is to give an introduction to formalization of mathematics: this is the process of using a computer to reason. I will explain what formalizing mathematics means and why it is interesting and useful for people interested in "standard" mathematics. I will show how this is done in practice using Lean, one of the several proof assistants available today. This is not a course in logic nor foundations of mathematics, in particular no prior knowledge of these topics is needed.
The talk will take place in HS5!