Theorem Proving in Lean

PhD course
7.5 credits
Study period 3, Jan-Mar 2025
Chalmers University of Technology
University of Gothenburg

Teaching Team

Lecturer (course-responsible): Mario Carneiro
Examiner (PhD): Magnus Myreen
Examiner (Masters: DAT235/DIT577): Ana Bove

Purpose

This is a PhD course on the Lean interactive theorem prover. It has seen increased use in industry as a formal verification tool, as well as in the mainstream mathematics community as a tool for stating definitions and checking theorems. The goal will be to gain familiarity with the system and learn how to use it to do mathematics and formal verification.

On completion of this course, students are expected to have learned:

This is a project course where students work either individually or in pairs on projects in the Lean interactive theorem prover. Early in the course there will be general introductory lectures about Lean. Once the students have settled into their projects, the lectures will become weekly project status reporting meeting and troubleshooting sessions.

Prerequisites

Students must have prior courses on functional programming and on logic.

For PhD Students

Organization is informal, come to the first lecture and we can go from there.

For Masters Students

This course is primarily intended for PhD students, but Masters students with a suitable backgrounds are most welcome too.

For masters students, this is an instance of Research-oriented course in Computer Science and Engineering (Chalmers: DAT235, GU: DIT577) with Ana Bove as examiner. Contact Ana Bove if you would like to be registered to this course. Note that you may not take the class for credit if you already have a result for this course code DAT235/DIT577 (e.g. from a previous iteration of the course).

Masters students that would like to be registered to this course need to have completed:

Examination and Grading

The course will be examined in two parts: (1) the code will be reviewed by the teacher and examiner, (2) the students need to present their project orally to fellow students.

The grading scale for Masters students is:

For a PhD student to pass, the PhD student must achieve at least grade 4.

Schedule

Lectures in EDIT Anaylsen 13:00-14:45 on Tuesdays and Thursdays starting 28 Jan 2025. The course finishes during exam week of Study Period 3, i.e., 21 March 2025.

Resources

Lectures

The course materials can be found on GitHub. You should check out this repository and build it to follow along with the lectures, and it can serve as a template scratch pad project as well.

In case you cannot attend a lecture or just want to follow along without the pressure of getting a grade, the lectures are all being recorded and posted on YouTube.