I re-read Theorem Proving In Lean over the weekend. The first time I read it was over the summer, when I was learning the basics of Lean, and I got a lot out of it. This time I knew something about Lean already, and this time I understood the vast majority of the book and of course I learnt a lot more.
One thing that I had not understood too well before this weekend, was what Lean’s type system looked like. Here is a very naive explanation of it.
At the top of the Type tree is a type called Prop and a type called Type. There are other things higher than these guys, e.g. Type has type Type 1, and Type 1 has type Type 2 and so on, but really (at least as far as I am concerned in this post) these extra types are just put there so that every object can have a type. I am much more interested in the definitions and theorems of mathematics, which typically go on below Prop and Type.
The object universe goes down two levels from Prop and Type. I guess it looks like this. There are Definitions: these are types
D such that the type of
D is Type. And under this is Data: these are objects
d such that the type of
d is some Definition
This structure is mirrored on the Prop side. If
P is a type whose type is
P is said to be a proposition. And under the propositions are Proofs: these are objects
p such that the type of
p is some proposition
So Lean is all about constructing Definitions, Data, Propositions and Proofs.
Here are examples of each of these things.
Definitions: the natural numbers, the integers, the real numbers, the complex numbers. Groups, rings, fields, schemes, complex manifolds, number fields, Banach spaces…
Data: The number 6, the number , the trivial group, the Riemann Zeta function, Ramanujan’s modular form .
Propositions: 2+2=4, 2+2=5, Fermat’s Last Theorem, the Birch and Swinnerton-Dyer conjecture, the Riemann Hypothesis, the statement that sqrt(2) is irrational, the statement that every positive real number has a positive real square root.
Proofs: These are just proofs of propositions.
For mathematics to work easily in Lean, it would be nice to get more of all of these things in. Johan de Jong started writing a web book on the foundations of algebraic geometry. His definition of an affine scheme is here: Definition of affine scheme in the stacks project. Could we put that definition into Lean? How about the Ramanujan Delta function? What actually needs to be done? Ramanujan conjectured that if was the coefficient of $q^p$ in his function, then had size at most . His conjecture was proved several decades later by Deligne, and the proof is thousands of pages long in some sense. Could we get the statement of Ramanujan’s conjecture into Lean? How about the definition of a modular form?