Which definitions do we want in our library?

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 D.

This structure is mirrored on the Prop side. If P is a type whose type is Prop then 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 P.

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 \pi, the trivial group, the Riemann Zeta function, Ramanujan’s modular form \Delta.

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 \tau(p) was the coefficient of $q^p$ in his function, then \tau(p) had size at most 2p^{11/2}. 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?


About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in General. Bookmark the permalink.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s