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-73L 4 Credits BSC , MSC D-MATH

Computer Formalisation of Proofs

Lecturers & Examiners: Prof. Dr. David Alexander Loeffler
Number of participants limited to 20.
VVZ CR n/a

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

Abstract

This seminar will be an introduction to computer formalisation of mathematical proofs. The focus will be on learning to use the "Lean" proof assistant.

Objective

Students will learn the purpose and general principles of proof assistants, and will gain experience of formalising simple proofs (in a mathematical area of their choice).

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 Computer Formalisation of Proofs
Fully booked. The seminar starts on 27 February 2025
  • Thu 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.)