Learning Lean Prover

Today I start learning Lean Prover seriously. I’ll spend a couple of days to get familar with this language and join this very forum. Anyone has slightest interest in this language please drop me a line we could study it together.

I’ll update resources / links / some thoughts during the journey.

Lean Web Editor for testing

Lean4 Documentation

Theorem Proving in Lean

Set up Lean (install VSCode -> Lean 4 extension, pretty easy)

IMO Grand Challenge

Quick review about Lean (it’s an article since 2018 so I suppose he talked about Lean 3 but now Lean 4 is out so after this course I’ll check whether those comments were oudated or not)

Dependent Type Theory tutorial by Lean

History of Type Theory (wiki)

—

First, Lean was developed by Microsoft Research lab (launched by Leonardo de Moura) and its purpose was to create the bridge between ITP and ATP <source>.

Some keywords: Lean’s behind logic was Dependent type theory. More specifically, it’s Calculus of Constructions with inductive types (this is a sort of Dependent type).

—

A couple of terms

• simple type
• alpha equivalent
• term normalization or definitionally equal. They are considered “the same” by Lean’s type checker, and Lean does its best to recognize and support these identifications. Point here is: Lean does it best because this is an undecidable problem. However, does it best is a black box and I don’t think it’s modular enough for further development or being re-programmed.
• type inference: when Lean has enough information about type, we don’t need to declare it. This is helpful & convenient rather than essential.
• open: same as import in Python
• namespace: same as import in Python
• dependent type: to learn more
• proposition as type
• proof as type:
• Curry-Howard isomorphism (propositions-as-types paradigm)

Books on this problem

• a good list of books on this topic

---

>> Feynman Learning Technique. When I have nobody to teach, I’ll try to explain this topic clearly in this article.

>> Overview about Type Theory

By Stanford Encyclopedia of Philosophy | Wikipedia | Some Preprint | Short Course

>> Overview

Type Theory is a vague term that refers to lot of stuffs but now it refers to typed systems based around lambda calculus.

2 most influential theories:

• typed lambda calculus (by Church)
• intuitionistic type theory (by Per Martin-Löf)

The type theory for most decent ITPs:

• Calculus of Constructions (from Coquand, that’s where Coq came from). Inductype Types added to enforce CoC, in Lean/Coq for instance.

Another development:

• Homotopy type theory (HoTT)

---

Certain Understanding

• Type is an object like any other objects: vector, map, matrix, group, semi-ring, ideal, manifold, sheaf..
• A type is not always a “constant” or “static” type like Nat, Int..
• A type has structure. A type T can be written as T = T1 -> T2 for instance.
• Term is something. It’s an object of our theory. We have a collection of types (say a set U of all types) and a collection of terms (say a set M of all terms).
• There’s a map Type: term –> type. It’s like each field has a characteristic or each matrix has its determinant. It’s a map. It’s a property of a term.
• However, a type is also a term. So the collection of terms covers the collection of types. Hence, while a type is a term, a type has a type. If tau is a type then it’s a term hence we have type(tau). So the map Type from Terms -> Types inherits an internal-map inside collection of Types.
• Terms are either atomic terms or some_function + sub_tersms. This principle is simple, minimal. All terms are made this way even quantifier terms. That’s the viewpoint of type theory. They keeps things simple. However, point here is: a function can be considered as a term. And a function must be defined (construct, and that’s why we have constructive mathematics)

Wow, I have all good books recommended by Wikipedia.

Lambda Cube | A very good book by Henk Barendregt

CoC book –> I gotta say this is by far the best book in type theory for dummies. It tells hidden facts. It focuses on true problem. It expresses things in formal language precisely rather than human-friendly shits that make things even more ambigious.

Proof of the Martin Lof Type Theory | Some Work of Harrison on Resersion