Course Outline

The course outline is still subject to change, but will roughly be as follows.

Slides

Why formalize maths? The tech stack: how to properly organize a formalization project.

Section	Topic
`S04_NumberTheoryExample`	An example from number theory
`S04_TopologyExample`	An example from topology
`S05_ProgrammingLanguage`	Introduction to Lean as a Programming Language

Foundations of logic in Lean: what is a type and what does being classical vs. intuitionistic mean?

Section	Topic	Exercises
`S01_Fundamentals`	Fundamentals of Lean Proofs	`B01` \| `B02` \| `B03` \| `B04`
`S02_Reasoning`	Reasoning Tactics	`B01` \| `B02`
`S03_Connectives`	Logical Connectives	`B01` \| `B02` \| `B03`
`S04_Negation`	Negation and Classical Logic	`B01` \| `B02` \| `B03`
`S05_Quantifiers`	Quantifiers in Lean	`B01`

Set theory in Lean: why you should rarely do set theory in Lean.

Section	Topic	Exercises
`S01_SubsetsComplements`	Sets	`B01` \| `B02`
`S02_IntersectionsUnions`	Sets: Intersections and Unions	`B01` \| `B02`
`S03_SetFamilies`	Sets: Set Families	`B01`

Dependent type theory: where do the axioms live?

Section	Topic
`S02_DependentTypeTheory`	Dependent Type Theory
`S03_LeanImplementation`	Lean’s Implementation
`S04_VerifiedComputation`	Verified Computation and Trust

Natural numbers in Lean: why inductive types are so powerful.

Section	Topic	Exercises
`S01_Definition`	Defining the Natural Numbers	`B01` \| `B02`
`S02_Addition`	Addition	`B01` \| `B02`
`S03_Multiplication`	Multiplication	`B01` \| `B02`
`S04_Power`	Exponentiation	`B01` \| `B02`
`S05_AdvancedAddition`	Advanced Addition	`B01`
`S06_Inequalities`	Inequalities	`B01`
`S07_AdvancedMultiplication`	Advanced Multiplication	`B01`

Final exam and distribution of formalization projects for Master-level students.