M1F, Imperial undergraduates, and Lean

M1F is the “introduction to proof” course which I have taught for the last few years at Imperial College London. When I started this blog just over one and a half years ago, one of my goals was to see whether Lean could handle the solutions to an M1F exam. At the time it was pretty clear that it wasn’t ready — a random sample of M1F exams showed that most of them mentioned either the complex numbers, or functions such as the exponential, sine and cosine function. None of these were in Lean at the time.

I wrote some basic complex number code myself, and PR’ed it to the maths library; it was my first serious PR. A team led by Chris Hughes (at the time a first year) did sines and cosines and the exponential function. And now the inevitable has occurred: Abhimanyu Pallavi Sudhir, a current first year, has formalised the solutions to last year’s M1F final exam! Many thanks to Abhi — I was pretty sure this sort of thing should be accessible, but this is the proof. Apologies to Abhi for taking so long to get around to looking at his work. I believe that having concrete goals like this are a good way of driving Lean’s maths library in the direction which I want it to go in — formalising mathematics which is actually used by mathematicians. One reason I took so long to look at it was that I have been very focussed on the perfectoid project recently — but more of that in another post.

Funnily enough, one of the things in the exam which was the trickiest to do in Lean was the proof that 0.71 has no 8’s in its decimal expansion! Lean still does not have a theory of decimal expansions, although Calle Sönne and I will eventually get around to writing one (after exams). In the mean time, I wrote a definition from first principles which does the trick. Another irritating issue is the question about a set with two elements, which a mathematician can start with “WLOG the set is \{0,1\}“. I believe you — but this actually takes a few lines to justify in Lean. Something is missing here — a transport tactic of some kind. We’ll get there one day — the computer scientists are on the case.

20 months ago, formalising the solutions to an M1F exam seemed like a dream away. I’ve already mentioned three undergraduates who were involved in one way or another in realising this dream. All this made me start wondering about which Imperial undergraduates have contributed to Lean’s maths library, and what they have done. At the top we have Chris Hughes and Kenny Lau, who have made many many contributions. Kenny made a robust theory of localisations of commutative rings, essential for our work on schemes, and Chris proved the law of quadratic reciprocity and the fundamental theorem of algebra, amongst many other achievements. Both Chris and Kenny wrote their first year projects in Lean, and Chris is now a maintainer for Lean’s maths library! But here are a whole bunch of other Imperial undergraduates who have managed to get namechecked in Lean’s maths library as well:

  • Ellen Arlt (matrices)
  • Sangwoo Jo (number theory)
  • Guy Leroy (number theory)
  • Jean Lo (analysis, irrationals, operator norms)
  • Rohan Mitta (topology)
  • Blair Shi (matrices)
  • Abhimanyu Pallavi Sudhir (irrationals, analysis, hyperreals)
  • Calle Sönne (analysis, irrationals)
  • Andreas Swerdlow (algebra)

I must also mention Guillermo Barajas Ayuso, Luca Gerolla, Clara List, Amelia Livingston, Elliott Macneil, Ramon Mir and Ali Sever, all of whom wrote a substantial amount of Lean code which they did not PR; Clara on primes of the form x^2+ny^2 (completely solving the problem for n\leq 3), Luca on fundamental groups, Guillermo on analysis, Elliott on group theory and number theory, Amelia on group theory and Ali on Tarski’s formulation of 2d geometry. Ramon Fernandez Mir has written his MSci project in Lean! And last but not least, Keji Neri, who did a bunch of algebra over the summer with the Imperial summer students, even though he is a Cambridge undergraduate — the only one to have contributed to Lean’s maths library as far as I know. Oxford, Warwick, UCL, Bristol — where are you? Lean’s maths library is ready to digitise a huge chunk of your curriculum. Let’s do it — it will scare the grown-ups.

Finally, some news on Athina Thoma. Athina is the post-doc who has been observing the Imperial undergraduates and trying to figure out whether Lean helps them to learn proofs better. First great piece of news: she has had her contract renewed for another six months! Second great piece of news: slowly she and Paola Iannone are beginning to make sense of all the data they collected. I await with interest the paper they are writing, and the conclusions they will draw.

Advertisements
Posted in M1F, undergrad maths | Tagged , , , | 1 Comment

Happy pi day

Yesterday was pi day, and discussion of Lean’s support of pi came up on the chat. The discussion of pi is I think a great way of illustrating what Lean can and cannot do.

To start with, “Lean has pi”. Here it is in the source code.

lemma exists_cos_eq_zero : ∃ x, 1 ≤ x ∧ x ≤ 2 ∧ cos x = 0 :=      real.intermediate_value'       
(λ x _ _, continuous_iff_continuous_at.1 continuous_cos _)
(le_of_lt cos_one_pos)
(le_of_lt cos_two_neg) (by norm_num)

noncomputable def pi : ℝ := 2 * classical.some exists_cos_eq_zero

If you have ever thought about how pi might be defined formally, then maybe you can see what is going on here. The lemma cos_one_pos is the lemma that cos(1)>0 and the lemma cos_two_neg is the lemma that cos(2)<0. Cosine is defined as a power series and these are grotty power series computations. Now using the fact that cosine is continuous, and the intermediate value theorem, we can prove that cos(x) has a zero between x=1 and x=2. We define \pi to be two times an arbitrary zero of the cosine function between 1 and 2 (we choose a random one, using the computer science version of the axiom of choice, which says that you can choose an element from a non-empty set — just don’t get me started on this). The library then goes on to prove that in fact the cosine function has a unique zero in this range (because the cosine function is decreasing in this range) and now we have an unambiguous definition of \pi in Lean.

One has to constrast this approach with an approach taken by, say, a hand calculator, or a programming language like python or C++. In these languages, a value for pi will either be hard coded, or there will be an algorithm implemented which will generate pi to an arbitrary precision in as quick a time as possible. So, for example, a calculator can typically produce the value of \pi to ten decimal places (and a computer to far more if necessary), and then one could compute the value of \sin(\pi) to ten decimal places (or to far more) and see that it is 0.000000\dots.

But Lean is different. Lean is not a calculator. Lean is a theorem prover. It is true by definition that \cos(\pi/2)=0 in Lean, and it is a theorem in Lean that \sin(2\theta)=2\sin(\theta)\cos(\theta) and hence it is a theorem in Lean that \sin(\pi)=0. Note however that Lean has not done any numerical computation to prove this, it has deduced it from theorems and definitions. For this kind of question, one could regard Lean as performing better than the traditional “computational” model of a computer that we have — a computer can check that \sin(\pi) is zero to 10 or 1000000 decimal places, and the more places you want, the longer it would take. But it cannot prove the answer is zero. Lean can prove that \sin(\pi)=0 with no numerical computation at all.

But what if one did want to do a numerical computation of \pi? Well, this is the flip side of the story. Lean is not designed for this sort of question at all! It is a computer program which “knows \pi“, but actually what does it know about the value of \pi? Well, by definition, \pi is twice a number between 1 and 2, so we get

Theorem. 2<\pi<4.

So as you can see, in this regard Lean is lagging a bit behind the a hand calculator. It seemed like pi day was a good day to make things better.

And by the end of it, things had got about an order of magnitude better! Thanks to the efforts of Floris van Doorn, with some help by others, we now have

Theorem. 3.14<\pi<3.15.

Ongoing work by Kenny Lau might give us even more decimal places within the next day or so. But how might one go about proving such a theorem, given only a bunch of standard theorems about sine and cosine, and the facts that \cos(\pi/2)=0 and 2<\pi<4? Floris used the following trick:

\cos(x)^2=\frac{1+\cos(2x)}{2}.

Using this standard fact, and the fact that \cos(\pi/2)=0, he could deduce exact values for \cos(\pi/4),\ \cos(\pi/8),\ \cos(\pi/16),\ldots. Because \sin(x)^2+\cos(x)^2=1 he could deduce exact values for \sin(\pi/4),\ \sin(\pi/8),\ \sin(\pi/16),\ldots. He could also prove that if x>0 then \sin(x)<x (by using the power series for x\le 1 and the fact that \sin(x)\le 1 when x>1) and as a consequence could prove lower bounds for \pi! By using two terms of the power series for sine we can also prove that \sin(x)>x-x^3/6 for 0<x<1 and this gives us upper bounds.

Taking a random rational number and then squaring it, doubling it and subtracting one (which one has to do to get from \cos(x) to \cos(x)^2 can get a bit hairy once one has done it a few times. Lean had to prove intermediate goals such as

(2 : ℝ) ≤ ((((2 - (157 / 50 / 2 ^ (4 + 1)) ^ 2) ^ 2 - 2) ^ 2 - 2) ^ 2 - 2) ^ 2

and these are real numbers, which in Lean are big complicated equivalence classes of Cauchy sequences, so this looked a bit daunting at first — another reminder that Lean is designed to do proofs, not numerical computations. The norm_num algorithm strained a bit with these checks, however Mario Carneiro pointed out that with judicious approximations one can make life easier: the trick is to constantly replace fractions with large numerators and denominators with approximately equal fractions with smaller numerators and denominators before you square again. These dirty hacks got us through in the end.

The festivities are documented on the pi day thread at the Zulip chat (login required) or the archive of the Zulip chat (no login required), and Floris’ code is here (permalink) or get it at https://github.com/fpvandoorn/mathlib/blob/pi/src/data/real/pi.lean .

Using the decimal expansions library currently being developed by Calle Sonne and myself at Imperial, we can now prove that the first two digits of \pi after the decimal point are 1 and 4. We still have some way to go before we can catch up with Emma Haruka Iwao, but what if her code contains bugs? We have proofs 🙂

In fact in 2017, Bertot, Rideau and Thery did much better — they use Coq to get a million decimal places of pi, formally verified. Doing this work today made me understand far better what an achievement that was.

Posted in Uncategorized | Tagged , | 2 Comments

2+2=4

I am interested in teaching and outreach, and often get asked to give talks to schoolkids. I gave one today, to a room full of year 10 kids (aged 14-15), and I showed them Lean. This was the youngest group of students I’ve ever attempted to show Lean to. I decided to show them a proof that 2 + 2 = 4, starting from definitions of 2 and +. However by year 10 the students have not seen induction yet, so I started by showing them parts of a YouTube video with stuff in a line falling over (e.g. dominoes, humans). I then defined the naturals (I called them “numbers”) as an inductive type in Lean, showed how to define recursively the function which adds two to a number, and finally we proved 2 + 2 = 4 by unwrapping the definitions of 2 and + and so on.

I really didn’t know how it was going to go. But, to my relief, when we were doing the big calculation, I asked the audience to fill in the next line for all seven lines, and these kids managed to do it! I was very pleased.

Here are the pdf slides. In the actual talk the text appeared slowly (there were beamer pauses) and there were times when I spent a minute or two talking to the kids about what was going on.

On page 12 of the pdf I say “Let’s go and make some numbers using Lean” and this is what I coded up live. I finish by trying to formalise the statement that 2+2=4 but there’s a problem because although I’ve defined two and four I’ve not yet defined addition. We then go back to the pdf, and on page 15 I return to Lean and define addition like this. Then comes the moment of truth: the calculation on line 16 (which appears line by line in the actual presentation) and which I got them to do. Having made it through, I then showed how Lean could prove it with rfl, and claimed that this was because even though we’d only just taught it numbers it was already an expert in numbers. I then asked the audience what other kinds of maths did they think it was possible to teach Lean and immediately one kid said “all of it”. I agreed. I then made some provocative statements about why people like my daughter should not be forced to learn about cosines, and then asked if there were any questions. The first one was “How do I learn more about this stuff?”. But I did feel that I’d lost plenty of people in the room.

I think that age 14-15 is a little too young for this talk. These kids had self-selected — they were at Imperial for an open day (during a UK school holiday) so were probably interested in science. But I wonder if the material presented here would be a little more suited to kids a little older. I’m giving a couple more school talks in the future, so maybe I’ll find out soon enough.

Posted in Uncategorized | 4 Comments

Lean in LaTeX

Patrick Massot wrote a formatter, which can turn Lean code into beautiful LaTeXxy html. The undergraduates and I have been formalising Imperial’s first real analysis course M1P1 in Lean. Put them together and you get a 21st century proof of the sandwich theorem.

That last link is a link to a proof of the theorem that says that if three real-valued sequences (a_n), (b_n), (c_n) with a_n\leq b_n\leq c_n satisfy a_n\to\ell and c_n\to\ell, then b_n\to\ell. If you click on a line in the proof then it opens up the Lean code (which is probably incomprehensible if you don’t know any Lean) but the beauty is that if you then click on one of the grey rectangles either side of that line of Lean code then you get to see the tactic state, which a mathematician might well find easy to understand because it is written in standard mathematical language. This way a mathematician who does not know any Lean can still step through the formal proof, and can figure out how to get from each line to the next themselves, because each individual step is typically very short.

Ultimately this means that we can write formally-verified course notes for the Imperial analysis course which the first year undergraduates are currently attending, and the notes could be of use even to students who do not know the technicalities of how to use Lean and do not have Lean installed on the computers they have access to.

Posted in Imperial, undergrad maths | Tagged , | 2 Comments

A word on BIDMAS

Maybe it’s not called that in other countries, but in the UK BIDMAS (which I swear was “BODMAS” when I was at school, or maybe I just went to a weird school) was the rule that was used to figure out how to work out what things like 1+2*3-4/(5+6-7*8-9) meant. The BIDMAS rule was that B for Brackets came first, and then there’s this I which might stand for “indices” i.e. ^, and then division, multiplication, addition and subtraction. There seemed to be some disagreement amongst my own children (all of whom have learnt this at school over the last few years) as to whether the “DM” in BIDMAS meant that division had to be done before multiplication, or whether division and multiplication had equal “strength”. I ultimately realised that I was not entirely sure I understood this BIDMAS thing myself! I am pretty sure that BIDMAS doesn’t mean that addition must be done before subtraction, otherwise a-b+c would come out to be a-(b+c), whereas I am almost certain that it is supposed to mean (a-b)+c. [Interestingly though, it seemed to me that doing all divisions before all multiplications, from left to right, seems to give the same answer as treating division and multiplication with the same weight.]

We see from this discussion that these pieces of notation like + and *, and of course other symbols such as , and had better also have some sort of BIDMAS rule. Furthermore, we had also better know whether we evaluate them from left to right or from right to left, because sometimes this matters and sometimes it depends on the operator! For example 10-5-4 is (10-5)-4=1 and not 10-(5-4)=9, however if you type 2^1^2 into your favourite computer algebra package (or 2**1**2 if you’re using python) then the chances are you’re going to get 2^(1^2)=2^1=2 rather than (2^1)^2=2^2=4. Indeed, you can check that Lean thinks it’s 2:


#eval 2 ^ 1 ^ 2 -- Lean says 2
#reduce 2 ^ 1 ^ 2 -- still 2

How does this actually work then?

For any piece of notation like -, we need to know two things: First, its power (in the sense that BIDMAS says that * has more power than -; the power of an operator is a natural number) and secondly we need to know its associativity (we need to know whether a-b-c means (a-b)-c or a-(b-c)). It turns out that this is all you need to know. Lean’s parser is a so-called Pratt parser but all you really need to know is how Lean figures out the power (technically called the “left binding power”) and associativity of all the operators you run into. These operators include functions like nat.add, and notation like + (note in particular that even though nat.add 2 3 means the same as 2 + 3, the parser treats them differently). Note also that even though (a+b)+c=a+(b+c), Lean still has to know exactly which one is meant by a+b+c; the fact that they are equal is a theorem rather than being true by definition.

The first rule you need to know is that functions have very high power — they eat the next thing they see and that’s it.


#eval nat.add 3 nat.add 4 5 -- error

Functions are greedy. They eat the next thing presented to them and only afterwards check that it has the right flavour. The first nat.add eats 3, and then it eats the second nat.add and chokes because nat.add isn’t a natural number. You have to fix it with brackets, which have the highest power of all:


#eval nat.add 3 (nat.add 4 5) -- evaluates to 12

So that’s brackets and functions. Now what about notation? When notation is defined, its power is also defined. You can see the power of some notation by looking at at the numbers printed out with Lean’s #print notation command. For example


#print notation +
-- _ `+`:65 _:65 := has_add.add #1 #0

It’s the 65’s we need to understand here. The first number 65 tells you that `+` has power 65. The second number 65 tells you that + is left associative, that is, a+b+c=(a+b)+c by definition. Why? Well, in practice that second number is either equal to the first one (meaning the notation is left associative) or one less (meaning right associative). For example


#print notation ^
-- _ `^`:80 _:79 := has_pow.pow #1 #0

The power notation has a higher power than addition, as expected, but 79 is one less than 80, meaning that it’s right associative, as we saw above. Functions and brackets have power over 1000, by the way.

To learn more about left binding power and how Pratt parsers really work, e.g. to learn what the second number actually means and why it’s either equal to or one less than the first number, try the links on the Wikipedia website. But for Lean users who just want to figure out how things are being parsed, this trick should pretty much always tell you what you need to know. It’s worth just typing


#print notation

and looking at all the output — you’ll learn that ^ has power 80, * and / have power 70, and + and - have power 65, which tells you that Lean knows BIDMAS (and that addition and subtraction do indeed have the same power). Interestingly, we also learn that = has power 50. Had it ever occurred to you that = also needed a binding power? Lean also needs to know what P = Q = R means! It turns out that = is left associative, so 1 = 2 = (1 = 2) is true, by reflexivity.

If anyone has run into Lean’s (or Haskell’s) $ as an alternative for brackets, the way it works is that f $ x is just defined to be f x, but $ has power 1, which is so low that everything else gets evaluated first. For example


#eval nat.add 3 $ nat.add 4 5

works! Lean evaluates the $ at the very end, after it’s figured out that nat.add 4 5 is 9, so this time the addition succeeds.

The one gotcha I have run into is that the comma in ∀ (x : X), P x also has a super-low power (it has power 0 in fact), meaning that the innocent-looking


example (P Q : ℕ → Prop) :
∀ x, P x ∧ Q x → ∀ x, Q x ∧ P x := sorry

doesn’t mean what I would instinctively think it meant: Lean brackets it as ∀ x, (P x ∧ Q x → ∀ x, Q x ∧ P x), because has power 25, bigger than the power of the comma. To get this:


example (P Q : ℕ → Prop) :
(∀ x, P x ∧ Q x) → ∀ x, Q x ∧ P x := sorry

you have to add those brackets in explictly.

Posted in Learning Lean, Uncategorized | Leave a comment

Column addition

Lean has two copies of basic number types such as the naturals or integers. The reason is that Lean users might want to do two completely different things with numbers such as these. Some people might want to prove theorems about numbers, such as associativity of addition, or Fermat’s Last Theorem. Other people might want to do actual computations with numbers, for example proving that 617 is prime or figuring out 10000 * 10000. One thing I learnt from Seul Baek at Lean Together 2019 is that these two concepts fight against each other! Computer scientists will understand this well, but as a mathematician I am only just coming to terms with it.

As a mathematician I really like Lean’s definition of the natural numbers:


inductive nat
| zero : nat
| succ (n : nat) : nat

[and I should say in passing that as someone who has now looked at a lot of web pages containing Lean code, I wish these code blocks looked better in wordpress].

The advantage of this definition is that if you are trying to prove a theorem about natural numbers, then applying the built-in induction tactic to the variable in question reduces the question into exactly the problems you expect — the base case and the inductive step. Actually the real advantage is that you can use the equation compiler to make definitions by recursion, and it just works.

But apparently computer scientists are not particularly fond of this data type:


#reduce (10000 : ℕ) * 10000 -- deep recursion error

Apparently, making a term that looks like succ (succ (succ (... succ zero)))))...) with a hundred million succs can take up a lot of space.

Computer scientists hence prefer storing naturals in binary format. This code is essentially from mathlib’s data/num/basic.lean:


inductive pos_num : Type
| one  : pos_num
| bit0 : pos_num → pos_num
| bit1 : pos_num → pos_num

inductive num : Type
| zero  : num
| pos   : pos_num → num

A pos_num is a finite string of binary digits starting with a 1 (e.g. 6 is 110 in binary and bit0 (bit1 one) in Lean), and a num is either a pos_num or zero.

Computer scientists can now implement computationally efficient versions of addition and multiplication on num, for example after defining succ on pos_num in the natural recursive way, they can make definitions such as


  def add : pos_num → pos_num → pos_num
  | 1        b        := succ b
  | a        1        := succ a
  | (bit0 a) (bit0 b) := bit0 (add a b)
  | (bit1 a) (bit1 b) := bit0 (succ (add a b))
  | (bit0 a) (bit1 b) := bit1 (add a b)
  | (bit1 a) (bit0 b) := bit1 (add a b)

No surprises here — addition is defined by recursion on length of binary expansion, and in the obvious way. Multiplication is also defined, basically as long multiplication:


  protected def mul (a : pos_num) : pos_num → pos_num
  | 1        := a
  | (bit0 b) := bit0 (mul b)
  | (bit1 b) := bit0 (mul b) + a

OK so great, now we can do ten thousand squared:


import data.num.basic

#reduce (10000 : pos_num) * 10000 -- ugly output corresponding to 10^8 in binary

But actually we have to be careful here — what if I have made a typo in my definition of add on pos_num? I had better check that my definitions of add on nat and pos_num coincide! To put it another way — we need to prove that column addition is actually a valid algorithm for adding two numbers! Without this, Lean will not be able to prove anything about nats using the computationally efficient num.

This boils down to constructing maps between nat and num and verifying that these maps commute with addition.

To define a map from nat to num one has to “put a nat structure on num”, i.e. define zero and succ for num. This is not hard. To define the map in the other way, one has to define bit0 and bit1 on nat and this isn’t hard either.

But to prove that these maps are bijections is already some work. It suffices to prove that the composition in both ways is the identity. I tried this myself in Lean and the harder way was to show that if you start with a num then go to nat and back, you end up where you started. The problem with nums is that the version of induction you have is induction on length of binary representation, which is not so well-behaved; you first have to prove lemmas about the maps from num to nat and nat to num commuting with succ, bit0 and bit1.

After this, one wants to prove that the computer science definition of + is the same as the mathematics one. I jumped straight in, and soon I ran into a goal of the form (a+1)+1=a+(1+1) on num, so I figured I’d prove associativity for pos_num in general (after all, I’d already proved it for nat):


theorem challenge (a b c : pos_num) : (a + b) + c = a + (b + c) := sorry

But this turns out to be quite subtle! I would be interested in hearing from anyone who manages to do this directly. The inductive hypotheses you generate from induction on pos_num initially seem to be useless. Here is a link to the Lean web editor where you can try it yourself (or just cut and paste everything into VS Code if you have Lean installed locally).

I talked to computery-minded people at Lean Together and they were unanimous: don’t prove this directly! Prove associativity of nat, prove that the addition on nat and num agree, and deduce associativity on num from associativity on nat. I had actually rolled my own nat for this exercise, and all of a sudden I had to prove things like (a+b+1)+(a+b+1)=(a+a+1)+(b+b+1) on my nat with no high-powered tactics like ring available to me 🙂 Lucky I had a journey from Amsterdam back to London to do all this stuff on, and I already knew how to prove commutativity and associativity of addition on nat. Even more luckily, associativity of addition on num was not needed to show that addition on nat and num coincided. Whilst I do not really understand the details, I seemed to need associativity for num when proving that addition commuted with the map from nat to num, but when I gave up on this approach and instead tried to prove that addition commuted with the map from num to nat everything came together. I had already proven that these maps were bijections, so I could deduce that addition commuted with the map from nat to num from previous results.

The moral

When your schoolteacher taught you column addition back when you were a kid, you were wise not to ask them why column addition was associative, because the direct proof seems tricky!

PS it’s not impossible though 🙂

Posted in Learning Lean, number theory | Leave a comment

Learning Lean by example

I am interested in Lean for lots of reasons, and one of these reasons is that I am convinced that somehow it can be used to teach university mathematics students about proof in a new way. However I have run into two problems in practice.

First, Lean has a high learning curve, at least if you go about learning it the way I did, which was by trying to do undergraduate maths example sheets in Lean; the main problem is that the questions are in the wrong order, and one is constantly running into things which are easy in maths but hard in Lean (usually because the infrastructure is not yet there).

The second problem is that the resources are not yet there; the existing Lean literature is very good, but doesn’t ever actually get on to doing mathematics, it spends most of the time talking about types and the equation compiler and so on rather than actually working with fields like the real numbers — perhaps this is unsurprising, because the teaching literature tends to stick to core Lean whereas the real numbers are defined in the maths library.

I am going to change this by writing teaching material for mathematicians, but this will take time; I plan on working hard on it this term. I started by going through the material which I have generated whilst learning Lean myself, and some of this I now realise is quite good for beginners. I am just going to post some of this stuff on this blog and tag it “Learning Lean” to see if it’s of any help to anyone.

Here is some code which defines two inductive propositions on natural numbers. The first one is “I am even”. It’s defined like this — 0 is even, and if `n` is even then `n+2` is even; and that’s it. One can really work with this definition; I give some examples in the code below.

The second inductive proposition is “I satisfy the Collatz conjecture” (otherwise known as the 3n+1 problem). Recall that this conjecture says that if you start with any positive integer, and then halve it if it’s even, or multiply it by 3 and add 1 if it’s odd, then eventually you’ll get to 1. It’s cute, but not hard to see, that one can define this as an inductive proposition. I goof around with it a little in the below. I have documented the code; one can just cut and paste it into any Lean session and one doesn’t even need the maths library.

Click here to run the below code with the Lean Web editor (NB I have problems with firefox, but it works in Chrome for me). Or just cut and paste it into a Lean session.


-- Inductive propositions.

-- Example 1: even numbers.

-- inductive definition of "is_even" predicate on the real numbers
inductive is_even : ℕ → Prop 
| even0 : is_even 0 
| evenSS : ∀ n : ℕ, is_even n → is_even (n + 2)

open is_even  

theorem four_is_even : is_even 4 :=
begin
  -- goal now `is_even 4`
  apply evenSS,
  -- goal now `is_even 2`
  apply evenSS,
  -- goal now `is_even 0`
  exact even0  
end

-- can do it with functions too
theorem six_is_even : is_even 6 := evenSS 4 $ evenSS 2 $ evenSS 0 even0

theorem one_is_not_even : ¬ (is_even 1) :=
begin
  intro H,
  -- H : is_even 1
  -- clearly H can not have been proved using either even0 or evenSS
  -- so when we do this
  cases H,
  -- there are no cases left, so the proof is over!
end

-- cases can also be used to pull down higher odd numbers
theorem five_is_not_even : ¬ (is_even 5) :=
begin
  intro H5,
  cases H5 with _ H3, 
  cases H3 with _ H1,
  cases H1,
end

-- example of usage
lemma even_iff_SS_even (n : ℕ) : is_even n ↔ is_even (n + 2) :=
begin
  split,
  { -- easy way
    exact evenSS n,
  },
  -- other way a bit trickier
  intro HSSn,
  cases HSSn with _ Hn,
  assumption
end

-- Example 2: the Collatz conjecture.

/-- collatz n means the collatz conjecture is true for n -/
inductive collatz : ℕ → Prop
| coll0 : collatz 0
| coll1 : collatz 1
| coll_even : ∀ n : ℕ, collatz n → collatz (2 * n)
| coll_odd : ∀ n : ℕ , collatz (6 * n + 4) → collatz (2 * n + 1)

open collatz


theorem coll10 : collatz 10 :=
begin
apply coll_even 5,
apply coll_odd 2,
apply coll_even 8,
apply coll_even 4,
apply coll_even 2,
apply coll_even 1,
apply coll1
end

theorem coll10' : collatz 10 :=
  coll_even 5 $ coll_odd 2 $ coll_even 8 $ coll_even 4 $ coll_even 2 $ coll_even 1 coll1

-- if m is odd then 3m+1 is always even, so we can go from m=2n+1 to 6n+4 and then to 3n+2 in one step.
lemma coll_odd' (n : ℕ) : collatz (3 * n + 2) → collatz (2 * n + 1) :=
begin
  intro H3n2,
  apply coll_odd,
  -- unfortunately applying coll_even will tell us about collatz (2 * (3 * n + 2))
  -- rather than collatz (6 * n + 4), so let's fix this
  rw (show 6 * n + 4 = 2 * (3 * n + 2), by rw [mul_add,←mul_assoc];refl),
  -- with tactic.ring imported from mathlib this line could just be
  --  rw (show 6 * n + 4 = 2 * (3 * n + 2), by ring),

  apply coll_even,
  assumption
end

-- now we can go a bit quicker
theorem coll10'' : collatz 10 :=
begin
  apply coll_even 5,
  apply coll_odd' 2, 
  apply coll_even 4,
  apply coll_even 2,
  apply coll_even 1,
  apply coll1
end

-- Of course one should really be using a home-grown tactic to figure out which
-- of coll_even, coll_odd and coll1 to apply next.

/- this is the Collatz conjecture -/
theorem collatz_conjecture : ∀ n : ℕ, collatz n := sorry
-- Nobody knows how to prove this.
Posted in Learning Lean | Leave a comment