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…

 

 

Advertisements
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

Proving trivial things with Lean [difficulty : quite easy]

If you want to learn Lean, you can do what I did and read a book and do all the exercises. I had a pdf copy which I would browse through, but if you try this route then I would thoroughly recommend having a computer with Lean installed to hand when reading, because if you don’t understand something you can experiment.

However, watching my teenage children learn has been an eye-opening experience. They seem far more focussed on just launching in and then googling when they get stuck. My children have learnt all manner of things in this way, from how to draw eyes to how to make animated computer art to how to write Machine Learning projects in Python. In short — they want to do the exercises before they have even opened the book.

This post is for those who want to learn Lean this way. Let’s see Lean working with mathematical statements in practice.

If you want to actually do some real learning, you must have access to a working version of Lean. If you don’t use Lean then all you will know at the end of this is that 2+2=4 and you knew that already. The simplest way to use Lean is just to run it in a web browser — click on that link and then just switch between tabs. A better way is to install it on a Windows/Mac/Linux computer, but this takes some time. Whatever you decide to do, here is some Lean code for you to cut and paste. Let’s start by proving that 2+2=4. Oh — Harrison said I should be using MathJax. Note to self: google for how to do this. Anyway, cut and paste this:


example: 2+2=4 :=
begin
trivial
end

or just click here (link opens in new window), and then click around and wait a few seconds for everything to load.

OK that was pretty trivial, although I am not particularly happy with how that code looks in this blog. Note to self — figure out a better way of displaying code.

If you’re using Lean online via your web browser, or VS Code, you should be able to move your cursor around this proof and see information about the state of the proof in another window (in VS Code hover your mouse over the symbols in the top right until you find the “display goal” one and click on it to open the window I’m talking about — in the browser version it’s just right there on the right).

You’ll see that in the middle of the argument we had a “goal”, which was “weird-sideways-T 2+2=4”. Then by the end we had no goals, which was because we had solved all the goals. The weird sideways T basically means: “anything to the left of it is something we are assuming, and anything to the right of it is something we are proving” (we didn’t have to assume anything here.)

Fiddle around and prove more things. That’s how we’re going to learn in this post. Try to prove that 2+3=5. Can we do big numbers? Can you prove 12321+12321=24642? Try to prove that 2+2=5. What happens? Can you prove that 3*3=9? That 5-4=1? Can you prove that 2-3=-1? This one is much harder that it looks! Can you prove that 2-3=0? Wait–what?

By default, Lean’s numbers are what a computer scientist might call “the natural numbers”, which apparently in their subject means \{0,1,2,3,4,\ldots\}. As a mathematician I was always taught that they started with 1 but never mind. Can you now see what is going on with 2-3 now? What do you think you will be able to prove that 7/3 is?

Even though you don’t have to, you can explicitly tell Lean that you’re talking about natural numbers, by writing (2:nat) instead of 2. If you’re using VS Code you can even write (2:\nat) and a really cool thing happens. Try it! The standard notation for the natural numbers is \mathbb{N}. It used to be \mathbf{N} in books, but when mathematicians wrote this on a blackboard it became \mathbb{N} (“blackboard bold”), and then at some point after LaTeX got popular in the 1990s the notation actually changed in books from the bold to the blackboard bold. Take a look at an old maths book at some point and notice that there’s probably no blackboard bold in it at all.

There is also standard notation for the integers in books — they’re called \mathbb{Z} and they are \{\ldots,-2,-1,-0,1,2,\ldots\}. There is also the rational numbers (\mathbb{Q}) and the real numbers (\mathbb{R}). However to get the rationals and the reals in Lean you’ll start having to import libraries so let’s not worry about that now.

Lean does understand negative numbers, but you will have to tell it explicitly that this is what we’re using. Try


example : (2:int)-(3:int)=(-1:int) :=
begin
trivial
end

That works, although it’s a bit ugly. You will get used to ugly. In fact you’ll begin to find it beautiful. When you’re bored of typing (2:int)+(2:int)=(4:int) you can see if \int works. You can also drop some of those ints. Try (2:int)+3=5. What about 2+(3:int)=(5:int). Not everything works! Why not? Remember that 2 by itself is a natural number not an integer. Hint: when adding two things together, Lean looks at the first one first — you have to start somewhere.

OK, let’s do algebra. We need a variable, and we will follow the time-honoured tradition by calling it x. Of course Lean wants us to know whether it is a nat or an int, because it’s fussy like that. So when we introduce the variable, we have to tell it. Try this.


variable x : int
example : x=x :=
begin
trivial
end

If you move the cursor up and down through the code you can see that in the middle we have a goal of x=x but we also have a hypothesis, which is that x is an integer. See the use of the colon? x:\mathbf{Z} means “x has type int“. We’re doing mathematics in a set-up called “type theory” so everything has a type. If you want to get distracted, then you can check the types of stuff with the #check command. Try this (some time after the variable command so Lean knows what x is)


#check 2
#check x
#check (2:int)
#check int

As I say, pretty much every object in Lean has a type. Did you notice that even int had a type? What is the type of the type of the type of the type of 2?

Anyway, let’s get back to algebra. See if you can prove that x+2=x+2. Can you prove that x+2=2+x though? Unfortunately, this apparently is non-trivial. We see on the right that our “trivial tactic failed”. Aah — so “trivial” is a tactic! There’s actually a whole section on tactics in the Lean reference manual, although actually that link is currently secret because the manual isn’t finished yet. The “trivial” tactic will only get you so far. There’s a much better tactic called “simp”, which is short for simple, which means that it will solve some goals which are bit more difficult than trivial. See if this works.


variable x : int
example : x+2=2+x :=
begin
simp
end

See how far you can get. You can even have more than one variable at once:


variables x y z: int
example : x+y+z=z+y+x :=
begin
simp
end

I think that’s enough for starters. Give it a go, get stuck, it’s quite confusing. Ask for help in the comments.

The bad news is that there aren’t that many powerful tactics at this point. The good news is that the Lean guys are writing new tactics all the time and adding them to Lean, so over the next few months maybe Lean will evolve and learn new moves tactics and by the end of term we will have caught them all done all the example sheet questions.

Posted in Learning Lean | Leave a comment