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

401-3040-25L 4 Credits BSC , MSC D-MATH

Formalising Mathematics in Lean

Lecturers & Examiners: Dr. Jaume De Dios Pont
Number of participants limited to 16.
VVZ CR n/a

Last Updated: 2026-06-01 11:33:48

Abstract

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

Objective

Learn the purpose and general principles of proof assistants. Gain experience of formalising simple proofs in a mathematical area of their choice. Understand the general steps to turn a mathematical proof into a computer-assisted proof.

Resources

Literature

[1] The Lean Game Server: https://adam.math.hhu.de/#/ (We will focus on Natural Numbers/Set Theory) [2] Mathematics in Lean: https://leanprover-community.github.io/mathematics_in_lean/ (Standard tutorial in Lean) [3] Theorem proving in Lean https://lean-lang.org/theorem_proving_in_lean4/ (More type-theoretic, slightly beyond the scope of the course)

General Information

Language
English
Levels
BSC , MSC

Examination

Type
ungraded semester performance

Registration & Places

Limited places (Special selection)
Signup End
08.02.2025
Priority: Registration for the course unit is only possible for the primary target group

Course Components

Type Title Time & Place Hours
seminar Formalising Mathematics in Lean
Fully (or almost fully) booked. The seminar started on 27 February 2025 If there are unexpectedly still free places in this seminar, it was recommended to attend the introductory session of this seminar on 27 Feburary 2025 (12:15-14:00 HG G26.1). (Without guarantee)
  • Thu 12:15-14:00 (HG F 26.5)
  • 27.02 Date 12:15-14:00 (HG G 26.1)
2 h weekly

Offered In

  • Mathematik Bachelor
    • Seminare (ZUR BEACHTUNG: Damit die Zuteilung der verfügbaren Seminarplätze sich nicht primär auf den Zeitpunkt des Einschreibens in die Warteliste stützen muss, haben die meisten Mathematik-Seminare ein spezielles Auswahlverfahren. Eine direkte Belegung in myStudies ist dann nicht möglich, alle kommen zuerst auf die Warteliste. Ausserdem gilt: Die Auswahl an Mathematik-Seminaren wird auf 1 Seminar pro Semester beschränkt. Beachten Sie auch die Lerneinheit 401-0002-99L Generic Seminar - Second Priority / Third Priority.)
  • Mathematik Master
    • Seminare und Semesterarbeiten
      • Seminare (ZUR BEACHTUNG: Damit die Zuteilung der verfügbaren Seminarplätze sich nicht primär auf den Zeitpunkt des Einschreibens in die Warteliste stützen muss, haben die meisten Mathematik-Seminare ein spezielles Auswahlverfahren. Eine direkte Belegung in myStudies ist dann nicht möglich, alle kommen zuerst auf die Warteliste. Ausserdem gilt: Die Auswahl an Mathematik-Seminaren wird auf 1 Seminar pro Semester beschränkt. Falls Sie in diesem Semester 2 Seminare absolvieren müssen, melden Sie sich bitte beim Studiensekretariat (E-Mail: ). Beachten Sie auch die Lerneinheit 401-0002-99L Generic Seminar - Second Priority / Third Priority.)