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¶
- 
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. 
What happened in class¶
- 
Introduction, motivation. 
 Video recording Lean file used Slides
- 
Logic: basic proofs using tactics intro,apply,exact,trivial, andexfalso.
 Video recording A Video recording B Class github repo Homework Homework on live-lean
- 
Logic: more proofs using tactics cases,constructor,left/right,rw,rfl. Real numbers:ring, ornorm_num. Alsouse,intro.
 Video recording A Video recording B Video recording C Homework Homework on live-lean
- 
Real numbers: dealing with sequences and quantifiers ( intro,specialize,use,obtain). First glimpse of types.
 Video recording A Video recording B Video recording C Homework Homework on live-lean
- 
Functions in many guises. PAT principle. Inductive types. 
 Video recording A Video recording B Video recording C