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
You're viewing possible stale or outdated data. Please check the latest semester for more up-to-date information.

Computer Formalisation of Proofs

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

Last Updated: 2026-02-05 16:14: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 Start
31.07.2023
Signup End
10.09.2023
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
  • Thu 12:15-14:00 (HG G 26.3)
2 h weekly

Offered In

  • Mathematics Bachelor
    • Seminars (NOTICE: The number of seminar places is limited, and the special selection procedure should help to allocate the places not primarily according to the registration time. Everybody is waitlisted first when he/she tries to register for a seminar in myStudies. Moreover: Only one mathematics seminar can be chosen per semester. Notice also the course unit 401-0002-99L Generic Seminar - Second Priority / Third Priority.)
  • Mathematics Master
    • Seminars and Semester Papers
      • Seminars (NOTICE: The number of seminar places is limited, and the special selection procedure should help to allocate the places not primarily according to the registration time. Everybody is waitlisted first when he/she tries to register for a seminar in myStudies. Moreover: Only one mathematics seminar can be chosen per semester. In case you need to attend 2 seminars in this semester, please take contact with the Study Administration (email: ). Notice also the course unit 401-0002-99L Generic Seminar - Second Priority / Third Priority.)