Types

Lean uses something called type theory. This can be a little bit counterintuitive to mathematicians. For example there are lots of different kinds of 7. The core Lean library provides us with the natural number 7 = 7:nat, and the integer 7:int. If you have access to the maths library then (after e.g. import topology.real or wherever they have put the reals nowadays, I heard it’s moving to analysis.real) you have access to at least two further kinds of 7, namely 7:rat and 7:real, the rational number 7 and the real number 7. Mathematicians implicitly regard all of these 7’s as the same. Lean is a bit more wary about this kind of thing, although sometimes it will secretly change the type of something from nat to int to rational if it thinks that this is the only way to make things make any sense.

But I’m not here to talk about that, I’m here to talk about types. You can see the type of something with the #check command. Let’s take a look at some types. Note that anything after the -- signs means a comment.


#check 4 -- nat
#check nat -- Type
#check (7:int) -- int
#check int -- Type
#check Type -- kind of interesting. But not relevant to us.

If you’re using VS Code and you can find a little icon in the top right hand corner of one window that looks like four thin straight lines and says “Info View : Display Messages (Ctrl+Shift+Alt+Enter)” when you hover over it, then either by clicking on it or by typing Ctrl+Shift+Alt+Enter you can open a new little window where you can see the answers to all these checks. Alternatively you can just hover your cursor over the #check to see the answer.

I think Type is a kind-of weird name for an *example* of a type, because there are types like nat which are still types but which are not equal to Type. I guess the point is that Type is quite a general kind of type. If something has type Type, I like to think of it as a set. For example 4 is a number, not a set, so its type is nat and not Type; but the set nat of all natural numbers is a set, and indeed its type is Type.

Here are some more interesting types.


variable f: nat -> nat -- a function from the naturals to the naturals
#check f -- some sort of function type.
#check f 5 -- it's got type nat.

Note that we haven’t even defined the function f! So we wouldn’t actually be able to evaluate it, but even though it’s not been defined we can still figure out where it’s going from and to. This is called “type checking” I think. It’s some sort of basic sanity test which you can do in quite complicated situations to check that everything has the type it’s supposed to have.

Now here’s one of the most interesting types that there is.


#check (2+2=4) -- Prop
#check (forall x y : nat, x = y ) -- Prop
#check (forall x y : nat, x = x ) -- Prop
#check forall x y z n : nat, not ((x>=1) ∧ (y>=1) ∧ (z>=1) ∧ (n>=3) ∧ (x^n+y^n=z^n)) -- Prop

A “Prop” is a very common type, and it’s the type that true/false statements have.

It’s very easy to construct things of type nat. For example any non-negative integer that you can think of has type nat.

We just saw above that it’s also quite easy to construct things of type Prop. For example 2+2=4 has type Prop, as does the formulation of Fermat’s Last Theorem above.

But it turns out that (2+2=4) is *also* a type!

So can we build something of type (2+2=4)?

Sure we can:


theorem t : (2+2=4) := by trivial
#check t

There’s a proof of the trivial theorem that 2+2=4. What this means in Lean is that t is actually a thing of type 2+2=4, and it was constructed using the function by trivial. You could use begin/end instead:


theorem t2 : 2+2=4 :=
begin
trivial
end

#check t2

That’s a bit weird. Actually it’s not weird at all, it sort of makes things symmetric. For example 4 has type nat and nat has type Type, which is some sort of generic type that begins with a capital letter. Similarly a proof of 2+2=4 has type 2+2=4, which has type Prop, which is some sort of generic type that begins with a capital letter.

Because (forall x y : nat, x = y ) is simply not true, we can’t construct a proof of it. So there’s an example of a type for which we can’t construct any elements of that type! In fact there’s an even easier type with this property:


#check false

The type false is a Prop which has been specifically designed so that it is impossible to construct anything of that type. Very counter-intuitive if you’re coming to this from a world like C++ or something, where types are actually designed so that you can build useful things of these types.

The difference between a theorem and an example in Lean is that theorems name the objects they’re constructing (proofs of propositions) and examples don’t. So we can prove 2+2=4 a third time like this:


example : 2+2=4 := by trivial

and here what we did was that we constructed an element of type 2+2=4, didn’t give it a name, and then threw it away.

When you are in the middle of a big proof, you have a bunch of hypotheses with names, and a goal. For example here’s a very elaborate proof of some easy fact.


example : forall x : nat, x <= x+x :=
begin
intro x,
have H : 0<=x,
apply nat.zero_le,
-- at this point one could say "H is the hypothesis that 0 <= x"
-- but one could also say that H is an object of type 0<=x
-- or in other words a proof that 0<=x.
have H2 : x+0<=x+x,
apply nat.add_le_add_left,
assumption,
have H3 : x+0 = x,
trivial,
rewrite H3 at H2,
assumption
end

If you step through the proof, you can see that extra hypotheses slowly appear — these are objects representing proofs of mathematical true/false statements.

Functions are the same as logical implications.

Those of you who are paying attention might notice that Lean doesn’t distinguish between a mathematician’s “function arrow” \to and their “implies sign” \implies . This is because, to a computer scientist, they’re the same thing! For example the squaring function on the natural numbers is f : nat -> nat, and the input is a natural number (i.e. something of type nat) and the output is a natural number (i.e. something else of type nat). But if P and Q are Propositions, then a function f : P -> Q takes something of type P and returns something of type Q. Now something of type P is a proof of P, and something of type Q is a proof of Q, and this means that a function P->Q is something which takes a proof of P and returns a proof of Q — so in particular it means that if P is true (a notion which I am going to conflate with “provable”) then Q must also be true! In particular we can really think of this function as a proof that P\implies Q.

This is called the Curry–Howard correspondence apparently.

Advertisements
Posted in Learning Lean | Leave a comment

Jeremy Avigad’s Logic and Proof course

Jeremy Avigad runs a Logic and Proof course at Carnegie Mellon, which uses Lean. He teaches Lean in a methodical way which might be perfect for some people. The link I posted is still a work in progress — I believe his course is running right now and some things aren’t quite finished, or need certain libraries which may or may not be installed by default — but the course certainly contains some very illustrative examples of how to use Lean to do some basic mathematics.

Note that this is a course running in a computer science department, so there is more emphasis on things like the lambda calculus than one would normally see in a mathematics course. On the other hand I am well aware that some readers of this blog are on a joint mathematics and computer science degree…

 

 

Posted in Learning Lean | Leave a comment

Sheet 1 Q2,Q3

I’ve solved Q2 and Q3 of M1F Sheet 1 and pushed the solutions to github. Q4 I somehow want to persuade Xena to do herself, but I don’t quite know the best way to do this. These questions were much easier than Q1.

It’s really hard learning this new language but honestly I cannot begin to stress that things which seemed so so complicated to me two months ago now look much easier.

Thanks everyone who came this evening.

Posted in M1F | Leave a comment

More easy Lean proofs [difficulty : quite easy]

Pure mathematics is all about proofs, so we have to learn how to do proofs.

Let’s start with a super-abstract proof. Let’s just take three random mathematical true/false propositions P, Q and R, and let’s say that we know that P implies Q, and that Q implies R. Can we deduce that P implies R in Lean? Let’s take a look at this. Oh — to get the cute little arrow try writing “\to ” and to get the cool and sign try “\and “.


-- anything after two minus signs like this is a comment.

variables P Q R : Prop — P, Q, R are now true/false statements.

— Reminder : ∧ means “and”.

theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) :=
begin
admit
end

Here “admit” means “I haven’t done that proof yet”. Sort-of like admitting defeat.

If you click here you’ll open a version of Lean running in your browser, with the above code pasted in.

OK so here is the strategy for proving this. First of all, we establish that P → Q and that Q → R. We want to prove that P → R, so we assume P, we deduce Q from P → Q and then we deduce R from Q → R

In Lean, it looks like this.


-- anything after two minus signs like this is a comment.

variables P Q R : Prop — P, Q, R are now true/false statements.

— Reminder : ∧ means “and”.

theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) :=
begin
intro H, — H is “P implies Q and Q implies R”
have HPQ : P → Q,
exact H.left,
have HQR : Q → R,
exact H.right,
clear H, — we don’t need it any more

— We now have hypothesis HPQ, which is P -> Q
— and hypothesis HQR, which is Q -> R.
— We want to prove P -> R so let’s assume P
— and deduce R.

intro HP,
have HQ : Q,
exact HPQ HP, — apply P->Q to P to get Q.
— now we can get the goal
exact HQR HQ
end

This is hard to understand if you do not have the code running in a Lean session, so try it out, or, even better, get Lean running on a computer near you and cut and paste it in (who knows if this will work).

We can skip steps. Here are some shorter versions.


variables P Q R : Prop

theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) :=
begin
intro H, — H is “P implies Q and Q implies R”
intro HP, — we want P -> R so let’s assume P.
have HQ : Q,
exact H.left HP, — apply P->Q to P to get Q.
— now we can get the goal
exact H.right HQ
end

(click here)
or even


variables P Q R : Prop

theorem basic_logic : (P → Q) ∧ (Q → R) → (P → R) :=
begin
intros H HP,
exact H.right (H.left HP)
end

(click here).

Try and figure out how this works. “Intros” is just introducing more than one thing at once. The thing in the brackets in the last but one line evaluates to a proof that Q is true.

Here’s another example. We need to talk about “not”. The idea is that not P is supposed to be the opposite of P — i.e. if P is true then not P is false, and if P is false then not P is true. There’s a really cute way to do this in logic — we can define not P to be P → false. This works because (true implies false) is false, and (false implies false) is true.

In VS Code or Lean online, you can write \not instead of not, and it will give you some weird symbol, which is the notation used by some computer scientists and logicians.

The contrapositive of the statement P → Q is not Q → not P. The contrapositive of a statement should follow from the statement itself, so we should be able to prove this:


variables P Q : Prop

example : (P → Q) → (¬ Q → ¬ P) :=
begin
admit
end

Try firing this up, and use the intro (or intros) commands to see how many hypotheses you can introduce. If you keep using “intro” to introduce as many hypotheses as you can all at once, then a funny thing happens!


variables P Q : Prop

example : (P → Q) → (¬ Q → ¬ P) :=
begin
intro HPQ, — HPQ is P implies Q
intro HnQ, — HnQ is “not Q”
— our goal is now “not P”, i.e. “P implies false”.
intro HP, — this is hypothesis P.
admit
end

Run this in Lean, click on “admit” and see what happens.

Rather weirdly, our goal (the thing we’re supposed to be proving) is now the word “false”, which apparently means that our job is to prove something which isn’t true. This sounds tricky, until you realise that we are allowed to assume a bunch of hypotheses which actually can’t all be true, so this is really just what a mathematician would call a proof by contradiction.

Our hypotheses include both P and “P implies Q”, so we can deduce Q from these. Another hypothesis is “Q implies false”, so if we put it all together we can indeed prove “false”! Try it yourself, or see this in action here.

For an even cooler finish, we can use “contradiction”, which proves anything you like from two contradictory assmptions. Here is the proof using the contradiction tactic.

I need to say one more important thing. Clearly every proposition is either true or false, so in other words we should be able to prove this:


variable P : Prop

example : P ∨ ¬ P :=
begin
admit
end

How do we do this? Well, we can’t 😀 Computer scientists have a name for this basic fact — it’s apparently called “the law of the excluded middle”. Amazingly, this basic fact is not built into Lean by default, as apparently some computer scientists try and do mathematics without assuming it. We are mathematicians, so we will assume it. We can (and definitely should!) add it in as an axiom in fact.


axiom em (X : Prop) : X ∨ ¬ X -- no proof required, it's an axiom.

variable P : Prop

example : P ∨ ¬ P :=
begin
exact em P
end

This works.

Without assuming this as an axiom, “P or not P” is actually an unprovable statement for a general proposition P, in Lean. This just reflects the fact that Lean is designed for computer scientists as well as mathematicians. In fact more generally there is a “maths library” for Lean, called mathlib, which is not loaded into Lean by default, but which we as mathematicians will definitely need. I do not know how to load this library into the online version of Lean but I do know how to install it on a computer.

Questions 2 to 4 on M1F example sheet 1 might need to assume the law of the excluded middle. In fact, worrying about whether something assumes the Law of the Excluded Middle or not is not really a question for mathematicians, we just assume it.

Posted in Learning Lean | 2 Comments

Note for Imperial undergraduates

The Xena project now has an internal site on blackboard, Imperial College’s VLE. You (Imperial maths and JMC UGs) should all be registered as being able to view it. Email me if you can’t access it. It (only) contains internal administrative information (times, dates, places of meetings etc). All the examples and the mathematics will be posted here on this public blog.

I have no idea whether this link will take you straight there:

possible direct link to internal Xena pages

It works for me. It might work for any Imperial maths or JMC undergraduate who is logged into Blackboard. If it doesn’t work, let me know, or even better, send me a link that works for you!

Posted in Imperial | Leave a comment

What Xena is not.

A lot of people have asked me questions about Xena and it makes me realise that I’ve not explained some of it clearly enough.

At this point, Xena is an almost-empty library of undergraduate level mathematics, written in a programming language called Lean.

By the end of term, Xena will “know” M1F in the following very weak sense: I will (hopefully) have typed up all of the lectures and all of the example sheet questions and solutions into her language. In return, she will have checked all the proofs and solutions for me. Here we are playing to Xena’s strengths. She is careful and pedantic, and she can remember stuff we’ve told her.

Xena is not going to be doing your homework any time soon. Although she is a careful checker, she is incapable of having her own ideas at this point.

On the other hand, Xena is quite capable of going through a list of theorems that she knows and attempting to use them to solve problems. Indeed she can look through such lists very quickly and efficiently and put them together in all manner of ways. That’s one advantage of digitising them! The fact that most of the ways she puts them together will be really stupid might be compensated for by the fact that she will be being stupid at a tremendously quick rate.

I have absolutely no idea how good she will be at being able to solve problems in practice though, and I suspect that, initially at least, she will be rather poor at it. This is one thing I will learn more about as the term goes on. The reason I don’t know is that I suspect that nobody really knows. There are a few data points, produced by teams of researchers. Let’s get another data point, and instead of using a small team of expert researchers let’s use a large team of people who are interested in learning how mathematics works because they want to pass a degree in it.

One personal goal I have for the term is to teach Xena M1F in this very weak sense explained above — I want her to check all the theorems in the course and to check all the problems on the problem sheets. But one consequence of this is that anyone else who learns her language will be able to attempt to solve the M1F problem sheets in this language, and they will know at the end of it if their solution is correct or not, because if it compiles then it’s correct and if it doesn’t then it’s incomplete or wrong.

If I can teach this language well enough that other people can start typing up other problem sheets from other courses in this language — then maybe people who are not doing M1F can start to benefit from Xena’s very careful approach to mathematics.

So when do all the fireworks start with machine learning and AI and trying to create some gigantic mathsbot which will prove the Riemann Hypothesis? All of this is currently just a completely out-of-reach dream, and if proof strategies do not scale well then it might well remain a dream.

On the other hand, I firmly believe that if a student were to first learn the language, and then attempt to engage with some course material — from any pure mathematics undergraduate course — then trying to talk to Xena about this material may well teach them something about the nature of the material that they may not have known before. It might, for example, make them think more deeply about what is going on in the material. It might help them understand it better. It might teach them subtleties that they had not appreciated. It will not do their homework for them, but it might help them learn the material. And at the end of the day, as an educator, I am very interested in facilitating learning. That is an important part of my job, and that is one of the reasons that I started this project.

Posted in General | Leave a comment

First question done!

I have finally typed up full proofs for Xena, for the first question of M1F sheet 1.

Here are the questions in traditional PDF format: Example Sheet 1.

Here’s a link to a live Lean session containing the Solutions to all parts of Question 1 of this sheet. Click around and see if you can make any sense of it!

If you’d rather look at the questions than see the answers, here is a link to a Lean version of Question 1 from this sheet.

Posted in M1F | Leave a comment