Theorem Proving in Lean notes.

These notes were made while teaching myself how to do mathematics using the Lean4 programming language.

Helpful Resources#

I found the following resources to be very helpful. I have not read each of them exhaustively, but there were parts in each of these links that were helpful. I found the Functional programming in lean book hard to read. The theorem proving in Lean book was more forgiving. In general, I find articles written by the programming languages community slightly opaque, and difficult to understand. This is entirely because I do not possess the right background or shared vocabulary.

Proving Theorems In Lean#

• Glimpses of Lean (Short Version).
• University of Bonn lectures.
• Imperial Course on formalising mathematics in Lean - By Bhavik Mehta and Kevin Buzzard. I could not speak more highly of this course. My solutions (see branch titled solutions). I only worked through sets 1-10, and then the combinatorics stuff.
• Number theory Game

Theory#

• Andrej Bauers Course: A lot of the links in the course are now returning 404 error, but I found the introduction to Type Theory helpful. Beyond that, this course really leans on Glimpses of Lean, and is similar to the Imperial and Bonn course.
• Hitchhikers guide to formal verification: Long but very good for starting off.
• Notes on Lambda Calculus