Formalising mathematics : workshop 1 — logic, sets, functions, relations

Here’s information about workshop 1 of the 8 workshops in my formalising mathematics course.

Mathematical background

At Imperial I lecture part of a standard “introduction to proof” course, a compulsory course for every beginning maths undergraduate. In my lectures we cover the basics of logic, sets, functions and equivalence relations. The idea is that the students see some abstract definitions (such as injective functions) and then some simple theorems (such as the composite of two injective functions is injective) and then try some problem sheet questions where they practice their skills at putting basic proofs together on paper.

My formalising course is for more advanced students (on paper it’s for PhD students but next year there’s a rumour that I will be teaching it to final year undergraduates), so I can assume that they know how to prove that the composite of two injective functions is injective in the traditional way. The goal of this workshop is to get students proving statements at this kind of level of difficulty, in Lean.

What I will assume

• You have installed Lean 3 and the community tools e.g. by following the instructions on the Lean community website.
• You know the pen-and-paper proofs of the results we’re talking about (e.g. that equivalence relations on a set are the same as partitions).
• (optional but helpful): you’ve had a go at the natural number game so you know the basics of what it’s all about.

The workshop

Start by installing the course repository by following the instructions in the README on that page. NB if you skipped the Lean 3 installation part, then you can still play along by using the links on the README, but you will have a degraded (slower) Lean experience and I cannot guarantee that the links will continue to compile correctly as Lean and mathlib evolve; on the other hand, the course repository will always compile.

[ Note for nerds: you can’t just clone the repo. You have to install it correctly using leanproject as explained in the README if you want access to Lean’s maths library (which you will need for some of the questions). ]

Open the repository using VS Code as explained in the README (you must use the “open folder” functionality of VS Code to open the entire repo, don’t just open a file or else again you won’t have access to the maths library), and find your way to the Lean files in src/week1.

[note for people who have not actually downloaded and installed Lean or anything — you can still play along with this part, you can click here and then wait for a while until Lean stops saying “Lean is busy…” and switches to “Lean is ready!”. You’ll have to allow cookies I think, and you won’t get the colours, but you gets what you pays for here]

Open the first of the Lean files — part_A_logic.lean. You will see some sorrys in the file — they’re in red (and there are corresponding little orange dots in the area where the scrollbar is). Let’s take a look at the first sorry in this file — it’s on line 68. In this puzzle, P is a proposition, which is a computer-science word for a general true-false statement (in particular, P might not be true: 2+2=4 and 2+2=5 are both propositions in Lean). The puzzle is to prove that . The sorry indicates that the proof is incomplete — it tells Lean that this proof is omitted right now.

Let’s figure out how to prove this theorem in Lean.

Your first Lean proof.

Here is the maths proof that we’re going to formalise. We are trying to prove that if P is any true-false statement, then P implies P. One proof of this is a boring “truth table” proof, where we just check the two cases where P is true and P is false. You can do this in Lean using the tauto! tactic, which will in fact solve pretty much all of the problems in this first logic file. But let’s solve it “constructively”, as the computer scientists call it.

Here’s the mathematical proof we’re going to formalise. Our goal is to show that P implies P. So let’s start by assuming that P is true. Our goal now changes into a new goal: we now have to prove that P is true. But this is exactly one of our assumptions, so we are done.

Let’s step through how this looks in Lean. We have our file on the left, and another window called the “infoview” on the right, which displays the tactic state (the goal and the hypotheses — i.e., the state of Lean’s brain). Right now the tactic state should look like this:

This means that P is a Proposition, and the goal (the statement after the sideways T) is to prove . Now, back in the Lean file, under the -- Prove this using intro and exact comment, type intro hP, so it looks like this:

Don’t forget the comma. Just after you’ve typed the comma, look at the infoview. It has changed — it now looks like this:

We now have a Proposition called P, and a new hypothesis hP which is the hypothesis that P holds, i.e., that P is true. The goal has changed too — our goal now is to prove that P is true.

Note that hP is just a name. We could instead of typed intro Nigel and then Lean’s infoview would display Nigel : P . Beginners can get confused about the difference between P and hP; I will say more about the difference later on, although I could make the following cryptic remark now that P is what is called a Type, and hP is a term of that type. We’ll come back to this. Let’s concentrate on finishing the proof right now.

Our goal is now to show that P is true. But this is exactly one of our assumptions, namely hP. So we can finish the proof by adding exact hP, under the intro hP tactic, like this:

If we take a look at the infoview just after typing that comma, we see that a good thing has happened:

You just proved a theorem in Lean! But actually there is still something wrong: you can see that the sorry on the left now has a red underline on it. Clicking on sorry shows you the text tactic failed, there are no goals to be solved. in the infoview. We are apologising unnecessarily. Delete the sorry, the error goes away, and now the proof is complete. If you look down at the bottom left hand corner of VS Code you will now see something like this:

That means that there are no errors in your file, and 39 warnings. Each theorem whose proof still has one or more sorrys in generates a warning, indicating that you cheated. You should always try and keep your files so that they have no errors, and your job in the workshop is to try and decrease the number of warnings, by filling in sorrys with proofs.

The difference between P and hP

If I were to say to you “What is Fermat’s Little Theorem?” then you would probably tell me that it’s the statement that is congruent to mod , if is a prime and is an integer. If you were writing a proof and you were working mod and had a number , you could replace it with and justify this in your work by saying you were using Fermat’s Little Theorem.

This is the way mathematicians speak. But something I noticed only after I started formalising is that here they are using the phrase “Fermat’s Little Theorem” in two different ways. When asked what the theorem is, the response above is a description of the statement of the theorem. But in the middle of a proof, if you want to invoke it, then you are really using the proof of the theorem. If I were to ask you what the Riemann Hypothesis was, then you might state it, but this doesn’t mean that you can just say “now by the Riemann Hypothesis” in the middle of a proof, at least not if you want your proof to be complete, because in the middle of a proof you are only allowed to use stuff which is proved in your arguments, not just stuff which is stated.

We saw hP : P above. One model of what is going on here is that P is the statement of the proposition we’re thinking about, and hP is the proof. I see beginners writing things like exact P in their proofs. But In the proof we have to use exact hP because we need to use the proof, not the statement. In fact what we are doing in this proof is constructing a function which sends proofs of P to proofs of P. Lean is a functional programming language, and under the hood the way Lean understands a proof of the form is as a function, or an algorithm, which takes as input a proof of P and returns as output a proof of Q. If you want to learn more about how Lean’s type theory models theorems and proofs, you can try this other blog post — it’s not too difficult — but you don’t really need to know about this stuff to get something out of this course.

A second proof.

Let me go through one more proof. Let’s prove that and together imply . The sorryed proof is around like 98 or so in the file (it might have moved a bit if you typed in the earlier proof). It looks like this:

The first surprise is that there is no “and” here. The way I have formalised this statement in Lean is like this: . In words, implies that (deep breath) implies . This is of course logically the same as saying that and imply . Also worth noting is that the Lean formalisation has a disconcertingly small number of brackets in. This is because the → symbol in Lean is right associative, which is just a fancy way of saying that if you see P → Q → R it means P → (Q → R).

Our goal is hence of the form “P implies something” so we can start with intro hP, (or intro Nigel or whatever you want to call the assumption that P is true). The goal now changes to the something, which is “(P implies Q) implies something”, so we can continue with intro hPQ, and now our tactic state looks like this:

We have two propositions, P and Q, and hypotheses hP (saying that P is true) and hPQ (saying that P implies Q). So, exactly as advertised, we know and , and we want to prove . Next we need to learn a new tactic, the apply tactic.

apply is a difficult word. Humans apply all sorts of facts to deduce other facts all over the place in mathematics. In Lean, apply has a very precise meaning, and we are in precisely the situation here where we can use it. If you try apply hPQ, for your next move in this puzzle game, the tactic state changes to the following:

The difference: the goal has changed! Our goal used to be to come up with a proof of Q. But P implies Q, so if we apply this fact then we see that it suffices to come up with a proof of P instead. That is what the apply tactic does — it reduces our problem to a simpler one by applying an implication. You can only use the apply h tactic if h is an implication, or a series of implications, which ultimately imply your goal.

The rest is easy — exact hP, or even the assumption tactic (which closes any goal which happens to be one of your assumptions) will work.

Try the rest on your own.

The rest is up to you. I have put model solutions in the solutions directory. You will need to know a few more tactics than these three — I have explained them in the week 1 README. Thanks for coming to my course, and good luck!

Post workshop thoughts.

There was far too much material for a beginner to complete within 2 hours. Most people did not even finish Part A. In some sense, there was a lot of material designed to hammer home a few basic tactics again and again. I don’t think it matters if students don’t make it through the material. I’m going to press on next week and do basic group theory and subgroups.