Introduction to the Type Theory of Lean

Abstract: As Lean slowly but surely takes over the world, it is becoming necessary for more and more people to understand how it works. Unfortunately, the people who built Lean must have known this would happen because they made it as hard to understand as they could. The foundational proof system of Lean is the "Calculus of Constructions with Inductive Types" which is a dependent type theory. In this talk, we will take an introductory look at how types work in Lean, starting with what they are and what the colon in expressions like A : T means, and going from there.