LEAN -- Computer-Assisted Proofs¶

What is it about¶

Lean is a programming language that enables one to write statements and proofs of mathematical theorems.
We will learn how to use it, with the focus on being able to get fluent in doing proofs in this system.
We will also learn how to use Mathlib -- a collection of over 200K theorems covering most of undergraduate mathematics.
Based on time and interest, we will also see how Lean does what it does, how to use AI-assistence, etc.
We will use Lean4 (note that some resources on the web use the older version Lean3).

Organization¶

Lecture in SW2 Wed 17:20-18:50. Tutorials in form of homework problems.

The course credit is awarded for continuous work on homework assignments. The exam is based on a "project" (more substantial theorem with its proof in Lean), and a discussion over this.

Resources¶

How to run the thing
Page in SIS
Class github repo contains also instructions to install Lean in various ways.
In the first month we will be following the approach of Formalising Mathematics course by Bhavik Mehta and Kevin Buzzard. They created a useful reference.
Ultimate reference are the web sites of Lean theorem prover and the community around it.

LEAN -- Computer-Assisted Proofs¶

What is it about¶

Organization¶

Resources¶

What happened in class¶