VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.

401-3049-75L 5 Credits BSC , MSC D-MATH

Formalising Mathematics in Lean

Lecturers & Examiners: Dr. Jaume De Dios Pont
VVZ CR n/a

Last Updated: 2026-06-01 11:31:23

Abstract

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.

Objective

Learn the purpose and general design principles of proof assistants, specifically focused on the Lean4 proof assistant. Learn the main syntax of the Lean4 programming language. Understand the logical foundations of Lean4. Gain enough experience using lean4 to formalise small proofs in mathematical areas that the students are already familiar with. Understand the general steps needed to turn a large mathematical proof into a computer-assisted proof.

Resources

Lecture Notes

No course-specific lecture notes will be provided. The course will follow a combination of the public notes in the Literature section, and the slides of the course (including references to the notes when applicable) will be provided

Literature

We will use material from the following notes/books - Mathematics in Lean ( https://leanprover-community.github.io/mathematics_in_lean/ ) - Theorem proving in Lean 4 ( https://leanprover.github.io/theorem_proving_in_lean4/ ) - Functional programming in Lean ( https://lean-lang.org/functional_programming_in_lean/ ) - Metaprogramming in Lean ( https://leanprover-community.github.io/lean4-metaprogramming-book/ ) - "Formalizing Mathematics" lecture notes ( https://b-mehta.github.io/formalising-mathematics-notes/ ) Meta-resource (list of notes with different styles) - https://leanprover-community.github.io/learn.html Other: - Natural Numbers Game ( https://adam.math.hhu.de )

General Information

Language
English
Levels
BSC , MSC

Examination

Type
graded semester performance
Homework/work-assessed class (details will be specified by the lecturer).No exam repetition!

Course Components

Type Title Time & Place Hours
lecture with exercise Formalising Mathematics in Lean
Permission from lecturers required for all students. lecture: Wed 12-14 exercises: Thu 17-18
  • Wed 12:15-14:00 (HG D 7.1)
  • Thu 17:15-18:00 (HG E 33.3)
3 h weekly

Offered In