An introduction to computer formalisation of mathematical proofs using the Lean proof assistant.

This course introduces the principles and practice of computer-assisted proof formalization using the Lean 4 proof assistant. Students learn how to encode mathematical statements in Lean4, construct rigorous proofs, and verify correctness through Lean’s type-theoretic framework, and learn about the logical foundations of Lean4.