Syllabus and Policies

Goals of the Course

This short course provides an introduction to the basics of machine- assisted proofs and program verification in the Lean proof assistant. We will learn how to combine programming and proving in the same environ- ment, blending together mathematical theorems, program specifications, and executable code. This class is for you if

• you enjoy rigorous mathematical reasoning;

• you are curious why Fields Medalist Terence Tao now does all his research in the Lean proof assistant;

• you want to learn the technology that is powering AI-based research in modern computer-assisted mathematics, such as AlphaProof;

• you are curious about what it means to “prove a theorem about a program”;

• you want to be introduced to the deep and elegant connection between mathematical logic and programming.

We will study the fundamentals of formalising mathematical statements and proving them in a computer-assisted tool. We will revise familiar notions, like theorems, proofs, and reasoning by induction, and will understand how they correspond to common programming intuition. We will learn how to specify properties of programs, ranging from exercises in functional programming to distributed systems. This is a hands-on class; it will include many live demonstrations, and you will be expected to participate in programming sessions and interactive discussions.

You are expected to put in considerable time and effort into working on the homework exercises and projects to gain experience with the techniques seen in class.

Homework Assignments and Projects

Each lecture of the class will be accompanied by a graded homework assignment, contributing to the final grade as per the schema below.

In addition to the assignments, there will be a course project on the topic of interactive reasoning in Lean. The projects will be done in teams of one or two students and will contribute a significant portion of the grade. Some high-level ideas for the projects will be offered around the third week of the class. The whole team is responsible for the work submitted. Although the work is shared, each student will received an individual grade. Team members will be asked to submit an evaluation of how well they and their teammates performed as team members. Each evaluation is confidential and will be be incorporated into the calculation of the individual grade.

Teams of one person are accepted but not encouraged.

Topics and Lectures

The list of topics below is a subject of possible minor changes.

• Types and functional programs

• Theorems and programs

• Different styles of a mechanised proof

• Inductive predicates and proofs

• Proofs of properties of functional and imperative programs

• Safety proofs of state-transition systems

• Encoding mathematical structures in Lean

Grading Schema

The final grade is combined from the following components:

• Homework Assignments: 60% (6 homeworks, 10% each)

• Research Project: 40%.

  • Written report: 10% (evaluated based on structure, clarity)

  • Code quality: 5% (well-documented, corresponds to the text in the report)

  • Presentation: 15% (you should be able to explain your design choices)

  • Self- and peer evaluation: 10% (based on the peer feedback in case of teams of two)

The following cutoffs will be used to determine letter grades. In the ranges below, x stands for your total score at the end of the semester. Final scores near a cutoff will be individually considered for the next higher grade. Plus(+) and minus(-) grades will also be given; their cutoffs will be determined at the end of the semester.

Score	Grade
88 ≤ x < 100	A
75 ≤ x < 88	B
60 ≤ x < 75	C
50 ≤ x < 60	D
0 ≤ x < 50	F

Grades are not curved. It is theoretically possible for everyone in the class to get an A (or an F). Your final grade depends only on your own final score and not on that of others.