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.
- Last year class
Related classes¶
-
In Summer semester there was/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.
-
Another
Organization¶
Lecture in SW1 Tue 17:20-18:50. Tutorials in form of homework problems + consultation (time TBA).
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¶
-
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.