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).
You may get an idea by trying one of the Lean games -- build a part of mathematics from the ground up.

In Summer semester there will be another class on LEAN taught by Mirek Olšák. The focus will be different, we both believe it makes sense for students to take both classes. (In any order.)
More broadly, there is also a course on Isabelle at Matfyz by Štěpán Holub, and on SAT & SMT solvers by Mikoláš Janota.

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 search -- Find theorems in Mathlib4 using natural language query
Loogle -- More structural search for Lean and Mathlib definitions and theorems.

LEAN -- Computer-Assisted Proofs¶

What is it about¶

Related classes¶

Organization¶

Resources¶

What happened in class¶