Computer Formalisation of Mathematics

I gave two guest lectures on metaprogramming and tactic writing in Lean 4. This github repository hosts the lecture notes and code.

Course Description

This course will give an introduction to computer formalisation of mathematics, working primarily in the Lean theorem prover.

Formalising mathematics on computers — not just numerical calculations, but definitions, abstract constructions, and proofs — is a project that has taken many decades to mature. In recent years, it has finally reached the point where formalisation is practicable for current research topics in many fields of mathematics. This is thanks to a combination of theoretical advances, and the resultant social traction which has drawn mathematicians from many areas to build up large and wide-ranging libraries of formalised material, covering much of the “standard literature”.

TThe present course will be primarily a practical introduction to Lean and Mathlib, aiming to enable students to formalise research-level mathematics in their own fields. We will also spend a little time on the theory of the logical systems (dependent type theories) underlying Lean and similar computer theorem provers.

Prerequisites None beyond standard PhD-student background in mathematics.
Some previous experience of programming helpful but not essential — no specific programming knowledge will be assumed.

Instructors Peter LeFanu Lumsdaine Anders Mörtberg