Division by zero in type theory: a FAQ

Hey! I heard that Lean thinks 1/0 = 0. Is that true?

Yes. So do Coq and Agda and many other theorem provers.

Doesn’t that lead to contradictions?

No. It just means that Lean’s / symbol doesn’t mean mathematical division. Let \mathbb{R} denote the real numbers. Let’s define a function f:\mathbb{R}^2\to\mathbb{R} by f(x,y)=x/y if y\not=0 and f(x,0)=0. Does making that definition give us a contradiction in mathematics? No, of course not! It’s just a definition. Lean uses the symbol / to mean f. As does Coq, Agda etc. Lean calls it real.div by the way, not f.

But doesn’t that lead to confusion?

It certainly seems to lead to confusion on Twitter. But it doesn’t lead to confusion when doing mathematics in a theorem prover. Mathematicians don’t divide by 0 and hence in practice they never notice the difference between real.div and mathematical division (for which 1/0 is undefined). Indeed, if a mathematician is asking what Lean thinks 1/0 is, one might ask the mathematician why they are even asking, because as we all know, dividing by 0 is not allowed in mathematics, and hence this cannot be relevant to their work. In fact knowing real.div is the same as knowing mathematical division; any theorem about one translates into a theorem about the other, so having real.div is equivalent to having mathematical division.

This convention is stupid though!

It gets worse. There’s a subtraction nat.sub defined on the natural numbers \{0,1,2,\ldots\}, with notation x - y, and it eats two natural numbers and spits out another natural number. If x and y are terms of type β„• and x < y, then x - y will be 0. There’s a function called real.sqrt which takes as input a real number, and outputs a real number. If you give it 2, it outputs \sqrt{2}. I don’t know what happens if you give it the input -1, beyond the fact that it is guaranteed to output a real number. Maybe it’s 0. Maybe it’s 1. Maybe it’s 37. I don’t care. I am a mathematician, and if I want to take the square root of a negative real number, I won’t use real.sqrt because I don’t want an answer in the reals, and the type of real.sqrt is ℝ β†’ ℝ.

Why can’t you just do it the sensible way like mathematicians do?

Great question! I tried this in 2017! Turns out it’s really inconvenient in a theorem prover!

Here’s how I learnt Lean. I came at it as a “normal mathematician”, who was thinking about integrating Lean into their undergraduate introduction to proof course. I had no prior experience with theorem provers, and no formal background in programming. As a feasibility study, I tried to use Lean to do all the problem sheets which I was planning on giving the undergraduates. This was back in 2017 when Lean’s maths library was much smaller, and real.sqrt did not yet exist. However the basic theory of sups and infs had been formalised, so I defined real.sqrt x, for x non-negative, to be Sup\{y\in\mathbb{R}\,|\,y^2\leq x\}, and proved the basic theorems that one would want in an interface for a square root function, such as \sqrt{ab}=\sqrt{a}\sqrt{b} and \sqrt{a^2}=a and \sqrt{a^2b}=a\sqrt{b} and so on (here a,b are non-negative reals, the only reals which my function would accept).

I then set out to prove \sqrt{2}+\sqrt{3}<\sqrt{10}, a question on a problem sheet from my course. The students are told not to use a calculator, and asked to find a proof which only uses algebraic manipulations, i.e. the interface for real.sqrt. Of course, the way I had set things up, every time I used the \sqrt{\phantom{2}} symbol I had to supply a proof that what I was taking the square root of was non-negative. Every time the symbol occurred in my proof. Even if I had proved 2 > 0 on the previous line, I had to prove it again on this line, because this line also had a \sqrt{2} in. Of course the proof is just by norm_num, but that was 10 characters which I soon got sick of typing.

I then moaned about this on the Lean chat, was mocked for my silly mathematician conventions, and shown the idiomatic Lean way to do it. The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the theorems where one puts the non-negativity hypotheses. For example, the statement of the theorem that \sqrt{ab}=\sqrt{a}\sqrt{b} has the hypotheses that a,b\geq 0. Note that it does not also have the hypothesis that ab\geq0, as one can deduce this within the proof and not bother the user with it. This is in contrast to the mathematicians’ approach, where the proof that ab\geq0 would also need to be supplied because it is in some sense part of the \sqrt{\phantom{2}} notation.

So you’re saying this crazy way is actually better?

No, not really. I’m saying that it is (a) mathematically equivalent to what we mathematicians currently do and (b) simply more convenient when formalising mathematics in dependent type theory.

What actually is a field anyway? For a mathematician, a field is a set F equipped with 0,1,a+b,-a,a\times b,a^{-1} where the inversion function a^{-1} is only defined for non-zero a. The non-zero elements of a field form a group, so we have axioms such as x\times x^{-1}=1 for x\not=0 (and this doesn’t even make sense for x=0). Let’s say we encountered an alien species, who had also discovered fields, but their set-up involved a function \iota :F\to F instead of our x^{-1}. Their \iota was defined, using our notation, by \iota(x)=x^{-1} for x\not=0, and \iota(0)=0. Their axioms are of course just the same as ours, for example they have x\times \iota(x)=1 for x\not=0. They have an extra axiom \iota(0)=0, but this is no big deal. It’s swings and roundabouts — they define a/b:=a\times\iota(b) and their theorem (a+b)/c=a/c+b/c doesn’t require c\not=0, whereas ours does. They are simply using slightly different notation to express the same idea. Their \iota is discontinuous. Ours is not defined everywhere. But there is a canonical isomorphism of categories between our category of fields and theirs. There is no difference mathematically between the two set-ups.

Lean uses the alien species convention. The aliens’ \iota is Lean’s field.inv , and Lean’s field.div x y is defined to be field.mul (x, field.inv y).

OK so I can see that it can be made to work. Why do I still feel a bit uncomfortable about all this?

It’s probably for the following reason. You are imagining that a computer proof checker will be checking your work, and in particular checking to see if you ever divided by zero, and if you did then you expect it to throw an error saying that your proof is invalid. What you need to internalise is that Lean is just using that function f above, defined by f(x,y)=x/y for y\not=0 and f(x,0)=0. In particular you cannot prove false things by applying f to an input of the form (x,0), because the way to get a contradiction by dividing by zero and then continuing will involve invoking theorems which are true for mathematical division but which are not true for f. For example perhaps a mathematician would say a/a=1 is true for all a, with the implicit assumption that a\not=0 and that this can be inferred from the notation. Lean’s theorem that real.div a a = 1 is only proved under the assumption that a\not=0, so the theorem cannot be invoked if a=0. In other words, the problem simply shows up at a different point in the argument. Lean won’t accept your proof of 1=2 which sneakily divides by 0 on line 8, but the failure will occur at a different point in the argument. The failure will still however be the assertion that you have a denominator which you have not proved is nonzero. It will simply not occur at the point when you do the division, it will occur at the point where you invoke the theorem which is not true for real.div.

Thanks to Jim Propp and Alex Kontorovich for bringing this up on Twitter. I hope that this clarifies things.

Posted in Learning Lean, M1F, M40001, Type theory, undergrad maths | Tagged , | 12 Comments

Equality, specifications, and implementations

Equality is such a dull topic of conversation to mathematicians. Equality is completely intrinsic to mathematics, it behaves very well, and if you asked a mathematician to prove that equality of real numbers is an equivalence relation then they would probably struggle to say anything of content; it’s just obviously true. Euclid included reflexivity and transitivity of equality as two of his “common notions”, and symmetry was equally clear from his language — he talks about two things being “equal to each other” rather than distinguishing between a = b and b = a.

One thing that has helped me start to understand why computer scientists make a fuss about equality is the observation that if you follow Peano’s development of the natural numbers (as I do in the natural number game) then you come to the following realisation: if you define addition by recursion in the second variable (i.e. a + 0 := a and a + succ(n) := succ(a + n) ) then life temporarily becomes asymmetric. The fact that a + 0 = a is an axiom. However the fact that 0 + a = a needs to be proved by induction. Now induction is also an axiom, so a mathematician would just say that despite the fact that the proofs have different lengths, 0 + a = a and a + 0 = a are both theorems, so the fact that digging down to the foundations shows that the proofs are of a different nature is really of no relevance.

To a computer scientist however, there is a difference in these proofs. This difference seems to be of no relevance to mathematics. But the difference is that, if you set the natural numbers up in this way, then a + 0 = a is true by definition, and 0 + a = a is not. Indeed, in Lean’s type theory (and probably in many others) there are three types of equality that you have to be aware of:

  1. Propositional equality;
  2. Definitional equality;
  3. Syntactic equality.

Let’s start by getting one thing straight: to a mathematician, all of these things are just called equality. In fact, even more is true: definitional equality is not a mathematical concept. All of these kinds of equalities are easy to explain, so let me go through them now.

Propositional equality: a = b is a propositional equality if you can prove it.

Definitional equality: a = b is a definitional equality if it’s true by definition.

Syntactic equality: a = b is a syntactic equality if a and b are literally the same string of characters.

For example, let’s go back to Peano’s definition of the natural numbers and the conventions for addition above. Then a + 0 = a is a definitional equality but not a syntactic one, 0 + a = a is a propositional equality but not a definitional one, and a = a is a syntactic equality. To show that 0 + a = a is not definitionally true, you have to ask yourself what the definition of 0 + a is; and because we don’t know whether a = 0 or not, 0 + a cannot be definitionally simplified any further (the definition of x + y depends on whether y = 0 or not).

[Technical note: syntactic equality does allow for renaming of bound variables, so \{a \in \mathbb{R}\, |\, a^2 = 2\} is syntactically equal to \{b \in \mathbb{R}\, |\, b^2=2\}. If you understand that idea that notation is syntax sugar then you’ll probably know that syntactic equality can see through notation too, which means to say that add(a,0) = a + 0 is also a syntactic equality. But that’s it.]

Of course 2 + 2 = 4 is not a syntactic equality; removing notation and writing S for “successor”, and working under the assumption that 2 is syntax sugar for S(S(0)) and 4 for S(S(S(S(0)))), we see that the left hand side is syntactically add(S(S(0),S(S(0)) and the right hand side is S(S(S(S(0)))). However it is a definitional equality! add(x,S(y))=S(add(x,y)) is true by definition, as is add(x,0)=x, and it’s fun to check that applying these rules a few times will reduce 2 + 2 to 4.

The reason that it’s important to understand the differences if you are writing Lean code, is that different tactics work with different kinds of equality. Lean’s refl tactic attempts to close the goal by showing that one side of an equality is definitionally equal to the other side. If your goal is X then change Y will work if and only if Y is definitionally equal to X. On the other hand Lean’s rw tactic works at the level of syntactic equality: if h : A = B then rw h will change everything syntactically equal to A in the goal, into a B. If h : a + 0 = b and your goal is a = b then rw h will fail because the equality a + 0 = a is not syntactic. However exact h will work fine, because exact works up to definitional equality.

Specification v implementation

The fact that a + 0 = a is a definitional equality in the natural number game, but 0 + a = a isn’t, is as far as I am concerned a proof that definitional equality is not a mathematical concept. Indeed one can clearly just define addition on the natural numbers by recursion on the first variable instead of the second, and then 0 + a = a would be definitional and a + 0 = a would not be. What is going on here was made clear to me after a conversation I had with Steve Vickers after a seminar I gave to the University of Birmingham CS theory group. Mathematicians have a specification of the natural numbers. We know what we want: we want it to satisfy induction and recursion, we want it to be a totally ordered commutative semiring (i.e. all the ring axioms other than those involving minus) and we can take it from there thank you very much. If you present me with an object which satisfies these theorems I can use it to prove quadratic reciprocity. I don’t care what the actual definition of addition is, indeed I know several definitions of addition and I can prove they’re all equivalent.

If you’re doing to do mathematics in a theorem prover, you have to make one definition. Mathematicians know that all the definitions of the natural numbers are the same. If you want to set up mathematics in set theory for example, then it doesn’t matter whether you decide to let 3 = \{2\} or 3 = \{0,1,2\}: any system which ensures that 3 isn’t any of the sets you’ve already made is clearly going to work. But in a computer theorem prover you need to make choices — you need to make implementations of 3 and of add — and the moment that choice is made you now have a dichotomy: some stuff is true by definition, and some stuff needs an argument like induction and is not true by definition.

The first time I really noticed the specification / implementation difference was when it dawned on me that Lean’s maths library had to choose a definition of the reals, and it went with the Cauchy sequence definition: a real number in Lean is an equivalence class of Cauchy sequences. An alternative approach would have been to define it as Dedekind cuts. As mathematicians, we don’t care which one is used, because we are well brought up and we promise to only ever access the real numbers via its interface, or its API to borrow a computing term. The interface is the specification. We mathematicians have a list of properties which we want the real numbers to satisfy: we want it to be a complete archimedean ordered field. Furthermore we have proved a theorem that says that any two complete archimedean ordered fields are uniquely isomorphic, and this is why we do not care one jot about whether we are using Cauchy sequences or Dedekind cuts. Lean gives me access to an interface for the real numbers which knows these things, and it’s all I need to build a theory of Banach spaces. As mathematicians we somehow know this fact implicitly. If I am trying to prove a theorem about Banach spaces, and I have a real number \lambda, I never say “Ok now for the next part it’s really important that \lambda is under the hood defined to be a Dedekind cut”. If I want the Dedekind cut associated to \lambda, I can just make it. I don’t care whether it equals \lambda by definition or not, because definitional equality is not a mathematical concept. All I care about is access to the interface — I’m proving a theorem about Banach spaces here, and I just need to have access to stuff which is true. The job of Lean’s file data.real.basic is to give me access to that interface, and I can build mathematics from there.

Computer scientists on the other hand — they have to care about definitional equality, because it’s often their job to make the interface! If two things are definitionally equal then the proof they’re equal is refl, which is pretty handy. Different definitions — different implementations of the same specification — might give you a very different experience when you are making an interface for the specification. If you really have too much time on your hands this lockdown, why not go and try proving that addition on the real numbers is associative, using both the Dedekind cuts definition and the Cauchy sequences definition? For Cauchy sequences it just boils down to the fact that addition is associative on the rationals. But you’ll find that it’s a real bore with Dedekind cuts, because Dedekind cuts have this annoying property that you need a convention for the cuts corresponding to rational numbers: whether to put the rational number itself into the lower or upper cut. Neither convention gives a nice definition of addition. You can’t just add the lower cuts and the upper cuts, because the sum of two irrationals can be a rational. Multiplication is even worse, because multiplication by a negative number switches the lower and upper cut, so you have to move a boundary rational between cuts. You can see why Lean went for the Cauchy sequences definition.

I ran into this “which implementation to use for my specification” issue myself recently. I notice that I have been encouraging students at Imperial to formalise courses which I have been lecturing, which recently have been algebra courses such as Galois theory. I am by training an algebraic number theorist, and really by now I should have turned my attention the arithmetic of number fields and their integers: as far as I can see, finiteness of the class group of a number field has been formalised in no theorem provers at all, so it is probably low-hanging fruit for anyone interested in a publication, and we surely have all the required prerequisites in Lean now. I thought that I would try and get this area moving by formalising the definitions of a Dedekind Domain and a discrete valuation ring (DVR). I looked up the definition of discrete valuation ring on Wikipedia and discovered to my amusement that there are (at the time of writing) ten definitions πŸ™‚

Now here I am trying to be a theory builder: I want to make a basic API for DVRs so that students can use them to prove results about local and global fields. So now I have to decide upon a definition, and then prove that it is equivalent to some of the other definitions — I need to make enough interface to make it easy for someone else to take over. As far as I could see though, what the actual definition of a DVR is, is of no real importance, because it doesn’t change the contents of the theorems, it only changes the way you state them. So I just chose a random one πŸ˜› and it’s going fine!

Equality of terms, equality of types

When talking about propositional and definitional equality above, my main examples were equality between natural numbers: 0 + a = a and what have you. Set-theoretically, we can happily think about 0 + a = a as equality between two elements of a set — the set of natural numbers. In type theory we are talking about equality between two terms of type T, where T : Type . But one can take this a level up. Say A : Type and B : Type (for example say A is the Cauchy reals, and B is the Dedekind reals). What does A = B mean? These are now not elements of a set, but objects of a category. Certainly the Cauchy reals and the Dedekind reals are not going to be definitionally equal. Can we prove they are propositionally equal though? No — of course not! Becuase they are not actually equal! They are, however canonically isomorphic. A fourth type of equality!

All this equality naval-gazing is important to understand if you are talking about equality of terms. This, we have nailed. For mathematicians there is one kind of equality, namely “it is a theorem that a = b“. For computer scientists there are three kinds, and understanding the distinction might be important for interface extraction.

But for equality of types, something funny is going on. Which is the most accurate? (A \otimes B) \otimes C \cong A \otimes (B \otimes C) or (A \otimes B) \otimes C = A \otimes (B \otimes C)? This is just more notational naval-gazing, who cares whether these things are isomorphic or equal – they are manifestly the same, and we can always replace one by the other in any reasonable situation because they both satisfy the same universal property. However, I am realising that as a Lean user I need to say very carefully what I mean by “a reasonable situation”, and actually the safest way to do that is to not prove any theorems at all about (A \otimes B) \otimes C other than the fact that it satisfies its universal property, and then instead prove theorems about all objects which satisfy that universal property. Mathematicians do not use this technique. They write their papers as if they are proving theorems about the concrete object (A \otimes B) \otimes C, but their proofs are sensible and hence apply to any object satisfying its universal property, thus can be translated without too much problem, once one has extracted enough API from the universal property. There is an art to making this painless. I learnt from Strickland the three key facts that one should prove about a localisation R \to R[1/S] of rings: the kernel is the elements annihilated by an element of S, the image of every element of S is invertible, and the map from R\times S to the target sending (r,s) to r/s is surjective. These three facts together are equivalent to the universal property of R[1/S] and now you can throw it away and build the rest of your localisation API on top of it. Indeed, when my former MSc student Ramon FernΓ‘ndez Mir formalised schemes in Lean, he needed this result from the stacks project to prove that affine schemes were schemes, but more generally for the case of rings only satisfying the same universal properties as the rings in the lemma. At the time he needed it (about 18 months ago) the proof only used the three facts above isolated by Strickland, and so was easy to prove in the generality he required.

However, in Milne’s book on etale cohomology, it is decreed in the Notation section that = means “canonical isomorphism”, and so there will be a lot more of this nonsense which we will have to understand properly if we want to formalise some serious arithmetic geometry in Lean.

Posted in Algebraic Geometry, General, Type theory | Tagged , , | 6 Comments

Teaching dependent type theory to 4 year olds via mathematics

We had a family Zoom chat today and I ended up talking to my relative Casper, who is 4 and likes maths. He asked me to give him some maths questions. I thought 5+5 was a good place to start, and we could go on from there depending on responses. He confidently informed me that 5+5 was 10, and that 5-5 was zero. For 5*5 he asked me “is that five fives?” and I said yes, and he asked me “Is that 5 lots of 5?” and I said yes, and then he began to count. “1,2,3,4,5. 6,7,8,9,10. 11,12,13,14,15. 16,17,18,19,20. 21,22,23,24,25. It’s 25!” he said. I guess he’s proved this by refl. Every natural number is succ (succ (succ (...(succ zero))...) so to evaluate one of them, you just break it down into this canonical normal form. He did not know what division was, so I thought it was time to move on from 5.

I figured that if he didn’t know his 5 times table we needed to be careful with multiplication, in case of overflow errors, so I decided I would go lower. I next asked him 0+0, 0-0 and 0*0 (“so that’s zero lots of zero?” Yes. “So that’s zero zeros?” Yes). He got them all right, and similarly for 1+1, 1-1 and 1*1. I then thought we could try 0 and 1 together, so I asked him 0+1 to which he confidently replied 1, and 0-1, to which he equally confidently replied 0.

This answer really made me sit up. Because Lean thinks it’s zero too.

#eval 0 - 1 
/-
0
-/

I am pretty sure that a couple of years ago I would have told him that he was wrong, possibly with a glint in my eye, and then tried to interest him in integers. Now I am no longer sure that he is wrong. I am more convinced that what has happened here is that Casper has internalised some form of Peano’s axioms for arithmetic. He knows β„•. In some sense this is what I have been testing. He knows that every natural is succ succ … succ 0, and then for some reason he has to learn a song that goes with it, with a rigid rhythmical beat and written in 10/4 time: “One, two, three four, five, six, seven, eight, nine, ten. Eleven, twelve,…” and so on ad infinitum, some kind of system which is important for computation but is currently not of interest to me. Also, Casper knows that there’s something called subtraction, and when given junk input such as 0-1 he has attempted to make some sense of it as best he could, just like what the functional programmers who like all functions to be total have done.

We then went onto something else. I asked him what 29+58 was and he essentially said that it was too big to calculate. I asked him if he thought that whatever it was, it was the same as 58+29, and he confidently said it was, even though he did not have a clue what the answer was. I asked him how he was so sure but I did not get a coherent answer.

I asked him what three twos were, and he counted “1, 2, 3, 4, 5, 6“. Three lots of two is 6. I then asked him what two threes were and he immediately replied 6 and I asked him if he’d done the calculation and he said no, two threes were the same as three twos. I asked him why but all he could say was that it was obvious. It’s simp. I asked him if he was thinking about a rectangle and he said no. So he knows simp and refl.

I then did quite a mean thing on him, I did overflow his multiplication buffer. I asked him what ten 3’s were. We spent ages getting there, and he needed help, because he hasn’t learnt how to sing the song in 3/4 time yet. But eventually refl proved that 10*3=30. I then asked him if he thought 3*10=10*3 and he was confident that it was. I then asked him what 3 tens were and whilst he didn’t immediately do this, he knew a song (in 4/4) which started at “one ten is10 (rest)” and finished at “ten tens-are-a hun dred.”. Using the song, we figured out pretty quickly what three tens were, and deduced that ten 3’s were 30 again. I then asked him what ten sevens were, and we talked about how how difficult it would be to sing the song in 7/4 and how long the song would be, and then we talked together through the argument that it was also “obviously” seven tens, so by the song it was seventy; apparently the fact that seventy sounds similar to 7 (even though thirty doesn’t sound that much like 3) is evidence that the patterns in the counting song can be helpful to humans who want to calculate.

I then remembered the junk subtraction answer, so I thought I’d try him on another function which returns junk in Lean, namely pred, the “number before” function on the naturals. I asked him what the number before 3 was, and he said 2. He was also confident that the number before 2 was 1, and the number before 1 was 0. I then asked him what the number before 0 was and he thought a bit and then said….”1?”.

pred is defined by recursion in Lean. We have pred (succ a) = a, and pred 0 is defined to be 0, because if you follow Lean’s “make all functions total, it’s easier for programmers” convention then it has to be something. But the choice of the actual value of pred 0 is probably not seriously used in Lean, and they could have defined pred 0 to be 1 or 37 and probably not much would break, and what did break would probably be easily fixed. Because of whining linter I recently needed to supply a junk value to Lean (it wanted me to prove that the quotient of a ring by an ideal was not the empty set) and I supplied 37 as the witness. pred is a fundamental function defined by recursion, as far as computer scientists are concerned. So why is it not even mentioned in the natural number game? Because you can’t really define functions by induction, you define them by recursion, and I don’t want to start getting involved in new recursive definitions, because this sort of thing cannot go within a begin end block. I could have decided to explain pred but I would have had to address the issue of pred 0 not being error and I realised that actually there was always a “mathematical workaround”. By this I mean the following. The natural proof of succ_inj uses pred, for example. The successor function is injective. The proof using pred is easy. But I tell people in the natural number game that succ_inj is an axiom, as is zero_ne_succ, and now we mathematicians seem to be able to develop a huge amount of theory without ever even defining subtraction. We don’t really want to use Lean’s natural number subtraction. We know that 0 β‰  junk is true by definition but unfortunately `0-0=0-1` in Lean, which is not right.

We then talked about the number line a bit, and I then told him about a level in the 2d Mario franchise where the exit is way off to the right but right at the beginning you can completely counterintuitively go off to the left and pick up some bonus stuff. I then told him that there were some other kinds of numbers which he hadn’t learnt about yet, and I said they were called the integers (note: not “the negative numbers”). I said that the integers included all the numbers he knew already, and some new ones. I told him that in the integers, the number before 0 was -1. I then asked him what he thought the number before -1 would be and he said “-2?” And I told him he was right and asked him what the number before -2 was and he confidently said -3, and we did this for a bit and chatted about negative numbers in general, and then I asked him what the number before -9 was and he said -10. I then asked him what the number before -99 was and he said -100 and then I asked him what the number before -999 was and he said he didn’t know that one and did I want to play Monopoly. I took this as a sign that it was time to stop, and we agreed to play a game of monopoly via this online video chat, and then it turned out that he didn’t know any of the rules of monopoly (he’d just found the box on the floor) and he couldn’t read either, so he just put the figures on random places on the board and we talked about the figures, and what we could see on the board, and what was in the monopoly box, and the maths lesson was over.

I was pretty appalled when I saw Lean’ s definition of int, a.k.a. β„€. It is so ugly. There are two constructors, one of_nat n which takes a natural number n and returns the integer n (an invisible function, set up to be a coercion), and the one called something really weird like neg_one_of_nat n which takes in a natural n and returns the integer -1-n, complete with hideous notation. This definition somehow arrogantly assumes some special symmetry of the integers about the point -0.5. The mathematician’s definition, that it’s a quotient of \mathbb{N}^2 by the equivalence relation (a,b)\sim(c,d)\iff a+d=b+c, a.k.a. the localisation of the additive monoid of naturals at itself (i.e. adding additive inverses to every element). This definition is a thing of beauty. The symmetry is never broken. It is the canonical definition. But even though this definition as a quotient is the most beautiful definition, classifying as it does the integers up to unique isomorphism because of the universal property of localisation (thanks so much Amelia Livingston), implementation decisions are system specific and int in Lean is the concrete inductive type with two constructors and there’s nothing we can do about this. So mathematically I am kind of embarassed to say that today I basically taught Lean’s definition of int to a kid, just as an experiment.

Another weird thing is that Lean has a really ugly proof of a+b=b+a in int but for some reason this is going to be “obvious” when negative numbers are taught to him in school, and will not need a proof. I guess ac_refl will do it.

When Casper had to go, I told him before he left to ask his parents what the number before -9 was. I think it’s a pretty tricky question if you’re caught off-guard. I told him that negative numbers were like mirror world. Is there educational research about how children model numbers? What different ideas do they have about β„• before they even start to learn their multiplication tables? Should we teach them induction now, before they are crushed by having to learn so many long and boring songs telling them things like six sevens are 42, because of the belief in the education system currently that memorising this is somehow important in the year 2020 when most teenage kids have a calculator app in their pocket.

Casper loves my daughter Kezia’s art. He says “everything is alive except the rainbow”.

Everything is alive, except the rainbow.
Posted in computability, Learning Lean, number theory, Type theory | Tagged , , | 8 Comments

Mathematics in type theory.

What is maths? I think it can basically be classified into four types of thing. There are definitions, true/false statements, proofs, and ideas.

Definitions (for example the real numbers, or pi) and true/false statements (for example the statement of Fermat’s Last Theorem or the statement of the Riemann Hypothesis) are part of the science of mathematics: these are black and white things which have a completely rigorous meaning within some foundational system.

Proofs are in some sense the currency of mathematics: proofs win prizes. Constructing them is an art, checking them is a science. This explains, very simply, why computer proof verification systems such as Lean, Coq, Isabelle/HOL, Agda… are much better at checking proofs than constructing them.

And ideas are the purely artistic part of mathematics. That “lightbulb” moment, the insight which enables you to solve a problem — this is the elusive mathematical idea.

Ideas are the part of mathematics that I understand the least, in a formal sense. Here are two questions:

  • What is a group?
  • How do you think about groups?

The first one is a precise “scientific” question. A group is a set equipped with some extra structure, and which satisfies some axioms. The formal answer is on Wikipedia’s page on groups. A group is a definition. But the second question is a different kind of question. Different people think about groups in different ways. Say G is a group generated by an element x satisfying x^5=x^8=1. What can you say about G? If you are a mathematics undergraduate who has just seen the formal definition of a group, you can probably say nothing. If you have a more mature understanding of group theory, you instantly know that this group is trivial, because you have a far more sophisticated model of what is going on. Ideas are complicated, and human-dependent. A computer’s idea of what a group is, is literally a copy of the definition in Wikipedia, and this is one of the reasons that computers are currently bad at proving new theorems by themselves. You can develop a computer’s intuition by teaching it theorems about groups, or teaching it examples of groups, or trying to write AI’s which figure out group theory theorems or examples of groups automatically. But intuition is a very subtle thing, and I do not understand it at all well, so I will say no more about these ideas here. I think that the concept of a map being “canonical” is an idea rather than a definition — I think different mathematicians have different ways of thinking about this weasel word. In this post I’m going to talk about how the three other concepts are implemented in type theory, in the Lean theorem prover.

Definitions, true/false statements, and proofs

In contrast to ideas, the other parts of mathematics (the definitions, theorems/conjectures, and proofs) can be formalised in a foundational system, and hence can be created and stored on a computer in a precise way. By this, I don’t mean a pdf file! Pdf files are exactly what I want to move away from! I mean that people have designed computer programming languages which understand one of the various foundations of mathematics (set theory, type theory, category theory) and then mathematicians can write code in this language which represents the definition, true/false statement or proof in question.

I am certainly not qualified to explain how all this works in category theory. In set theory, let me just make one observation. A definition in set theory, for example the definition of the real numbers, or \pi, is a set. And a proof is a sequence of steps in logic. A definition and a proof seem to me to be two completely different things in set theory. A group is a mixture of these things — a group is an ordered quadruple (G,m,i,e) satisfying some axioms, so it’s a set with some logic attached.

In type theory however, things are surprisingly different. All three things — definitions, true/false statements, and proofs — are all the same kind of thing! They are all terms. A group, a proof, the real numbers — they are all terms. This unification of definitions and proofs — of sets and logic — are what seems to make type theory a practical foundational system for teaching all undergraduate level mathematics to computers.

Universes, types, and terms.

In type theory, everything is a term. But some terms are types. Not every term is a type, but every term has a type. A colon is used to express the type of a term in Lean — the notation x : T means that x is a term of type T. For example, the real number Ο€ (pi) is a term in Lean, and the real numbers ℝ is a type, and we have Ο€ : ℝ , that is, Ο€ is a term of type ℝ. In set theory one writes Ο€ ∈ ℝ, in type theory we write Ο€ : ℝ. They both express the same mathematical concept — “Ο€ is a real number”.

Now Ο€ is a term but it’s not a type. In Lean, x : Ο€ makes no sense. In set theory, x ∈ Ο€ does happen to make sense, but this is a weird coincidence because everything is a set. Furthermore, the actual elements of Ο€ will depend on how the real numbers are implemented (as Dedekind cuts or Cauchy sequences, for example), and hence in set theory x ∈ Ο€ has no mathematical meaning; it happens to make sense, but this is a quirk of the system.

I claimed above that every term has a type. So what is the type of ℝ? It turns out that ℝ : Type. The real numbers are a term of a “universe” type called Type — the type theory analogue of the class of all sets.

Many of the mathematical objects which mathematicians think of as definitions either have type Type, or have type T where T : Type. As a vague rule of thumb, things we write using capital letters (a group, a ring,…) or fancy letters (the reals, the rationals) have type Type, and things we write using small letters (an element g of a group, a real number r or an integer n) have got type T where T is what we think of as the set which contains these elements. For example 2 : β„• and β„• : Type, or if g is an element of the group G then in Lean we have g : G and G : Type. You can see that there is a three-layer hiearchy here — terms at the bottom, types above them, and the universe at the top.

  • Universe : Type
  • Examples of types : ℝ, β„•, G (a group), R (a ring), X (something a set theorist would call a set), a Banach space, etc. Formally, we say ℝ : Type.
  • Examples of terms: Ο€ (a term of type ℝ), g (an element of the group G, so a term of type G), x (an element of X, so a term of type X). Formally, we say g : G.

This hierarchy is more expressive than the hierarchy in set theory, where there are only two levels: classes (e.g. the class of all sets), and sets.

There is a standard use of the colon in mathematics — it’s in the notation for functions. If X and Y are sets (if you’re doing set theory) or types (if you’re doing type theory), then the notation for a function from X to Y is f : X β†’ Y. This is actually consistent with Lean’s usage of the colon; Lean’s notation for the collection \mathrm{Hom}(X,Y) of functions from X to Y is X β†’ Y , which is a type (i.e. X β†’ Y : Type, corresponding to the fact that set theorists think of \mathrm{Hom}(X,Y) as a set), and f : X β†’ Y means that f is a term of type X β†’ Y, the type-theoretic version of f \in \mathrm{Hom}(X,Y), and the way to say that f is a function from X to Y in type theory.

(Not for exam) Strictly speaking, universes are types, and types are terms, but this is a linguistic issue: often when people speak of types, they mean types which are not universes, and when people speak of terms they mean terms which are not types. But not always. This confused me when I was a beginner.

Theorems and proofs

This is where the fun starts. So far, it just looks like a type is what a type theorist calls a set, and a term is what they call an element. But let’s now look at another universe in Lean’s type theory, the universe Prop of true/false statements, where our traditional mental model of what’s going on is quite different. We will see how theorems and proofs can be modelled in the same way as types and terms.

So, how does this all work? As well as the universe Type, there is a second universe in Lean’s type theory called Prop. The terms of type Prop are true/false statements. There is an unfortunate notation clash here. In mathematics, the word proposition is often used to mean a baby theorem, and theorems are true (or else they would be conjectures or counterexamples or something). Here we are using the the word Proposition in the same way as the logicians do — a Proposition is a generic true/false statement, whose truth value is of no relevance.

This will all be clearer with examples. 2 + 2 = 4 is a Proposition, so we can write 2 + 2 = 4 : Prop. But 2 + 2 = 5 is also a Proposition, so 2 + 2 = 5 : Prop as well. I’ll say it again — Propositions do not have to be true! Propositions are true/false statements. Let’s see some more complex examples.

The true/false statement that x+0=x for all natural numbers x is a Proposition: in Lean this can be expressed as (βˆ€ x : β„•, x + 0 = x) : Prop . A Proposition is a term of type Prop (just like the types we saw earlier were terms of type Type). Let RH denote the statement of the Riemann Hypothesis. Then RH : Prop. We don’t care if it’s true, false, independent of the axioms of mathematics, undecidable, whatever. A Proposition is a true/false statement. Let’s look at the part of Lean’s type theory hierarchy which lives in the Prop universe.

  • Universe: Prop
  • Examples of types : 2 + 2 = 4, 2 + 2 = 5, the statement of Fermat’s Last Theorem, the statement of the Riemann Hypothesis.
  • Examples of terms: ??

So what are the terms in this three-layer Prop hierarchy? They are the proofs!

Propositions are types, proofs are terms.

This is where the world of type theory seriously diverges from the way things are set up in set theory, and also the way things were set up in my brain up until three years ago. In trying to understand what was going on here, I even realised that mathematicians take some liberties with their language here. Before we start, consider this. The Bolzano-Weierstrass theorem is some statement in analysis about a bounded sequence having a convergent subsequence. I want to talk a little bit about how mathematicians use the phrase “Bolzano-Weierstrass theorem” in practice. A mathematician would say that the Bolzano-Weierstrass theorem is this statement about sequences having convergent subsequences. But if they are in the middle of a proof and need to apply it in order to continue with their proof, they say “by the Bolzano-Weierstrass theorem we deduce that there’s a convergent subsequence”. Nothing seems at all funny about any of this. But what I want to point out is that mathematicians are using the phrase “the Bolzano-Weierstrass theorem” in two different ways. When they say what it is, they are referring to the statement of the theorem. But when they say they’re using the Bolzano Weierstrass theorem, what they are actually using is its proof. The Birch and Swinnerton-Dyer conjecture is a perfectly well-formed true/false statement, you can certainly say what it is. But you can’t use the Birch and Swinnerton-Dyer conjecture in the middle of a proof of something else if you want your proof to be complete, because at the time of writing the conjecture is an unsolved problem. Making a clear distinction between the statement of a theorem, and the proof of a theorem, is important here. A mathematician might use the phrase “the Bolzano-Weierstrass theorem” to mean either concept. This informal abuse of notation can confuse beginners, because in the below it’s really important to be able to distinguish between a theorem statement, and a theorem proof; they are two very different things.

In the natural number game, I use this abuse of notation because I am trying to communicate to mathematicians. The statement βˆ€ x : β„•, x + 0 = x is a true statement, and I say things like “this is called add_zero in Lean”. In the natural number game I write statements such as add_zero : βˆ€ x : β„•, x + 0 = x. But what this means is that the term called add_zero in Lean is a proof of βˆ€ x : β„•, x + 0 = x! The colon is being used in the type theory way. I am intentionally vague about this concept in the natural number game. I let mathematicians believe that add_zero is somehow equal to the “idea” that x+0=x for all x. But what is going on under the hood is that βˆ€ x : β„•, x + 0 = x is a Proposition, which is a type, and add_zero is its proof, which is a term. Making a clear distinction between the statement of a theorem, and its proof, is important here. The statements are the types, the proofs are the terms.

  • Universe: Prop
  • Examples of types: 2 + 2 = 4, 2 + 2 = 37, the statement of Fermat’s Last Theorem — βˆ€ x y z : β„•, n > 2 ∧ x^n + y^n = z^n β†’ x*y = 0.
  • Examples of terms: the proof that 2 + 2 = 4 (a term of type 2 + 2 = 4), the proof of Fermat’s Last Theorem (a term of type βˆ€ x y z : β„•, n > 2 ∧ x^n + y^n = z^n β†’ x*y = 0)

Elements of a theorem

So our mental model of the claim Ο€ : ℝ is that ℝ, the type, is “a collection of stuff”, and Ο€, the term, is a member of that collection. If we continue with this analogy, it says that the statement 2 + 2 = 4 is some kind of collection, and a proof of 2 + 2 = 4 is a member of that collection. In other words, Lean is suggesting that we model the true/false statement 2 + 2 = 4 as being some sort of a set, and a proof of 2 + 2 = 4 is an element of that set. Now in Lean, it is an inbuilt axiom that all proofs of a proposition are equal. So if a : 2 + 2 = 4 and b : 2 + 2 = 4 then a = b. This is because we’re working in the Prop universe — this is how Propositions behave in Lean. In the Type universe the analogue is not remotely true — we have Ο€ : ℝ and 37 : ℝ and certainly Ο€ β‰  37. This special quirk of the Prop universe is called “proof irrelevance”. Formally we could say that if P : Prop, if a : P and if b : P then a = b. Of course if a Proposition is false, then it has no proofs at all! It’s like the empty set. So Lean’s model of Propositions is that the true ones are like sets with 1 element, and the false ones are like sets with 0 elements.

Recall that if f : X β†’ Y then this means that f is a function from X to Y. Now say P and Q are Propositions, and let’s say that we know P\implies Q. What does this mean? It means that P implies Q. It means that if P is true, then Q is true. It means that if we have a proof of P, we can make a proof of Q. It is a function from the proofs of P to the proofs of Q. It is a function sending an element of P to an element of Q. It is a term of type P β†’ Q. Again: a proof h of P\implies Q is a term h : P β†’ Q. This is why in the natural number game we use the β†’ symbol to denote implication.

Let false denote a generic false statement (thought of as a set with 0 elements), and let true denote a generic true statement (thought of as a set with 1 element). Can we construct a term of type false β†’ false or a term of type true β†’ true? Sure — just use the identity function. In fact, in both cases there is a unique function — the hom sets have size 1. Can we construct a term of type false β†’ true? Sure, there is a function from the set with 0 elements to a set with 1 element, and again this function is unique. But can we construct a term of type true β†’ false? No we can’t, because where do we send a proof of true? There are no proofs of false to send it to. So true β†’ false is a set of size 0. This corresponds to the standard truth table for β†’, where the first three statements we analysed were true and the last was false.

The proof of Fermat’s Last Theorem is a function

So what does a proof of βˆ€ x y z : β„•, n > 2 ∧ x^n + y^n = z^n β†’ x*y = 0 look like? Well, there is an arrow involved in that Proposition, so the statement of Fermat’s Last Theorem is some kind of set of the form \mathrm{Hom}(A,B), which means that in Lean, a proof of Fermat’s Last Theorem is actually a function! And here is what that function does. It has four inputs. The first three inputs are natural numbers x, y and z. The fourth input is a proof: it is a proof of the Proposition n > 2 ∧ x^n + y^n = z^n. And the output of this function is a proof of the Proposition x*y = 0. This is quite an unconventional way to think about what the proof of Fermat’s Last Theorem is, and let me stress that it does not help at all with actually trying to understand the proof — but it is a completely consistent mental model for how mathematics works. Unifying the concept of a number and a proof — thinking of them both as terms — enables you to think of proofs as functions. Lean is a functional programming language, and in particular it is designed with functions at its heart. This, I believe, is why theorem provers such as Lean, Coq and Isabelle/HOL, which use type theory, are now moving ahead of provers such as Metamath and Mizar, which use set theory.

Prove a theorem! Write a function!

Universe TypeProp
Type examplesℝ 2 + 2 = 5, (βˆ€ a : β„•, a + 0 = a)
Term examples37, Ο€add_zero, rfl
Cheat sheet
Clockroom
Posted in Learning Lean, Type theory, undergrad maths | Tagged , , , | 21 Comments

The Sphere Eversion Project

The perfectoid project.

Johan Commelin and I worked with Patrick Massot on the Lean perfectoid space project, but Patrick is not an algebraic number theorist, and he found our literature hard to read in places. He was constantly picking up on what I would regard as “typos” or “obvious slips” in Wedhorn’s unpublished (and at that time unavailable) notes — stuff which was throwing him off. Wedhorn’s notes contain an explicit warning on the front that they are not finished and you read them at your own risk, but Johan and I were between us expert enough to be able to explain precisely what was going on whenever Patrick asked about operator precedence or the meaning of some undefined \cdot . Torsten Wedhorn — thank you for your blueprint, now finally available on ArXiv . We learnt a lot from it — both about the definition of an adic space, and about how to write blueprints.

The point Patrick wanted me to understand was this: If I as a mathematician thought I really knew the definition of a perfectoid space, why couldn’t I come up with a precise and error-free and furthermore self-contained mathematical document that he, as a non-expert but as a professional mathematician, would be able to read without difficulty? Where was my plan for formalising perfectoid spaces? The answer to that was that the plan was in my head. Along the way, Patrick in particular learnt that there are problems with this approach.

The cap set problem.

In stark contrast to the perfectoid shambles was work of Sander R. Dahmen, Johannes HΓΆlzl, Robert Y. Lewis on the Cap Set Problem — see their ArXiv paper. Their main result is a complete computer proof formalisation of the main theorem in the 2017 Annals of Mathematics paper by Ellenberg and Gijswijt on the cap set problem. Sander, Johannes and Rob organised their workflow very differently. They started with a detailed pdf document written by Dahmen (a mathematician). This old-fashioned proof was self-contained, just did normal maths in a normal way, and didn’t mention Lean once. It is a document which will convince any proper mathematician who cares to read it carefully of the correctness of the proof. Dahmen’s work is a completely rigorous old-fashioned proof of the theorem. There is no doubting its correctness. But because it is complete, correct, and self-contained modulo undergraduate level mathematics, this means that people who are not necessarily specialists in mathematics can now begin to work together, using a computer system which knows a lot of undergraduate mathematics, and they can turn Dahmen’s blueprint into a proof of Ellenberg-Gijswijt stored as a virtual mathematical object in the memory of a computer. Such an object is far more amenable to AI analysis than the corresponding pdf file, because computers have a hard time reading natural language, even if written by mathematicians. Apparently we don’t always explain things correctly.

My point here is: Dahmen’s blueprint was an important part of the process.

The sphere eversion project.

But back to Patrick. He is conjecturing that Lean 3 is sufficiently powerful to formalise a complete proof of Sphere Eversion, the Proposition that you can turn a sphere inside-out without creasing it, as long as it is made out of material which has self-intersection 0, like light but bendier. There’s a video. 3D geometry is involved.

The amazing news is that Patrick has now written a blueprint for the proof. This is a normal mathematical document containing a proof of sphere eversion which anyone who knows enough maths to know what a manifold is, could check and see was a completely rigorous and self-contained proof. It is written by an expert in the area, and typeset in a clever way so it displays beautifully in a browser. It is an interactive blueprint. It is the beginning. It is half of the Rosetta Stone that Patrick is creating, which will explain one story in two languages — a human language, and a computer language.

Patrick has also started a Lean sphere eversion project on GitHub . This is a currently mostly empty Lean repository, which will ultimately contain a formal proof of sphere eversion if the project is successful.

Those two parts together form Patrick’s Sphere Eversion Project.

At some point in the near future, Patrick is going to need mathematicians to formalise parts of the proof. The people he’s looking for are perhaps people with degrees in mathematics who are interested in trying something new. Patrick and I, together with Rob Lewis and Jeremy Avigad, are still working hard on our forthcoming book Mathematics in Lean, an introduction to the skills that a mathematician will need in order to participate. Once you have learned how to write Lean, Patrick has some computer game puzzles which you might be interested in playing.

If anyone has questions, they could ask in the sphere eversion topic in #maths in the Zulip chat (login required, real names preferred, be nice), a focussed and on-topic Lean chat where many experts hang out. People who are looking for a less formal setting are welcome to join the Xena Discord server (meetings Thursday evening at 5ish).

The schemes project

What is so amazing about projects like these is that they are teaching us how to use dependent type theory as a foundation for all of pure mathematics. We have had occasional problems along the way. Every division ring is a ring and hence a monoid and thus a semigroup. Invisible functions piled up in type class inference. The perfectoid project helped guide us to the realisation that type class inference was becoming problematic at scales which mathematicians needed it to work, and the Lean developers have responded to this issue by completely redesigning the system in Lean 4.

But let me finish with my Lean schemes project — my first serious Lean project, written with Chris Hughes and Kenny Lau, both at the time first year undergraduates. The project is completely incompatible with modern Lean and mathlib, but if you compile it then you get a sorry-free proof that an affine scheme is a scheme. During our proof we ran into a huge problem because our blueprint, the Stacks Project, assumed that R[1/f][1/g]=R[1/fg], and this turns out to be unprovable for Lean’s version of equality: this equality is in fact one of Milne’s “canonical” isomorphisms. The Lean community wrestled with this idea, and has ultimately come up with a beefed-up notion of equality for which the identity is now true. Amelia Livingston is just putting the finishing touches on its implementation in Lean — many thanks indeed Amelia. It has been an extraordinary journey, and one which has taught me a great deal about localisation and how to think about it. I had never realised before that the rationals might not be equal to the field of fractions of the integers — whether those two fields are actually equal is an implementation issue of no relevance to mathematicians. What we need to know is merely that they are isomorphic and that there is a preferred isomorphism in each direction. This has design consequences which we are only just beginning to understand properly.

I wish the sphere eversion project every success. I am confident that it will teach us more about how to formalise mathematics in dependent type theory.

Posted in Imperial, Learning Lean, Type theory | Tagged , , , , , , , | Leave a comment

The complex number game

Mohammad and I spruced up the natural number game over the last few weeks. It now saves your progress, which is great (thanks Mohammad). Also coming along nicely is the real number game, currently written mostly by Dan Stanescu, but Gavin Thomson has just joined the party and I promise that I will be contributing in June when marking is over. Anyone who wants to get sneak previews of it should hang around on the Xena Discord server, which is where our Thursday evening Xena Project meetings are taking place this term; I’ll probably release a secret alpha this coming Thursday. Last Thursday on the Discord we had people any% speedrunning and racing the Lean tutorial project . This fits very well into my general worldview: I think that doing mathematics in Lean is like solving levels in a computer puzzle game, the exciting thing being that mathematics is so rich that there are many many kinds of puzzles which you can solve. Level creators are conjecture makers. If you are into puzzle games and know a little Lean then you might also want to check out the Codewars website, where support for Lean just moved from beta to official; right now there are over 50 approved Lean Kata, ranging from easy facts about odd and even numbers to some very tricky Diophantine equations.

Another project I’ve been involved in is the forthcoming book Mathematics in Lean. Again I am guilty of doing very little so far. What I’ve been trying to do is to formalise “random” basic undergraduate mathematics in Lean as best I can, using as much automation as I can, in order to see whether it is possible to write basic tactic proofs in “the way a mathematician would write them”, but none of this stuff has made it into the book yet. It is miserable when when you are trying to prove a theorem in Lean and you’ve reduced it to a statement which is completely mathematically obvious (e.g. the goal is to prove that two things are “the same”), but you can’t persuade Lean to believe this, so the art is to set things up in such a way that this issue doesn’t occur, and one way of doing this is by seeking advice from people who understand type theory better than I do.

So I’ve been doing several experiments, hoping that some of them will turn from ideas into chapters of this book, and one which I think went quite well was a construction of the basic properties of the complex numbers, which I liked so much that I’ve put into its own repo for now: The Complex Number Game.

This repo came about with me looking at the official mathlib file for the complex numbers, and “remixing” it, re-ordering it so that it was a bit more coherent, removing some of the more obscure computer-sciency lemmas, and heading straight for the proof that the complexes are a ring. My rewrite of the mathlib proof is heavily documented and the proofs of all the lemmas along the way are in tactic mode; in my view this makes things more accessible to mathematicians. The file data.complex.basic in Lean’s library has been examined and revisited so many times since 2017 that it is now in very good shape — in particular lemmas are correctly tagged with simp and this makes simp a very powerful tool.

If you want to play the complex number game right now, you have to install Lean first. I would love to share this game on CoCalc but right now I can’t get imports to work. I will come back to this in June.

If installing Lean really is not something you want to do, then you can play a crappier preliminary version using the Lean Web Editor (this is before I reorganised the material to make it more mathematician-friendly and turned more proofs from term mode to tactic mode). Or you can just watch me play it! I live streamed on Twitch a walkthrough of the tutorial level (the complexes are a commutative ring) last Thursday, and here is the video. This Thursday (28th May 2020) at 5pm UK time (1600 UTC) I’ll be on Twitch again, live streaming a walkthrough of the first two levels: sqrt(-1), and complex conjugation. I’ll be on Twitch for around an hour, and then we will retire to Discord for a Q&A and more any% racing. Mathematicians who are Lean beginners are welcome!

Someone else doing some remixing is my daughter Kezia Xena Buzzard (after whom the project is named). She made my new profile pic from Chris Hughes’ proof of quadratic reciprocity πŸ™‚

Posted in General, Learning Lean, undergrad maths | Tagged , | 4 Comments

Xena Project Thursday meetings start with talk tomorrow 21st May

Usually, the Xena project meets every Thursday evening (5pm to 10pm UK time) during Imperial College’s term time. Because students have been doing exams and the campus has been closed, there have not been any meetings this term so far, but now exams are winding down I am going to try and start things up again on Thursday evenings, from now until the end of June (i.e., the end of term).

We’re launching at 5pm UK time (=1600 UTC) on Thurs 21st May 2020 (check out the Xena project Google calendar) with a live demo by me of the new complex number game (which will be live on GitHub by tomorrow, assuming I’ve finished writing it). I’ll walk through the tutorial world, which proves that the complex numbers are a commutative ring. I’ll do it live on Twitch. Afterwards we can all retire to the Xena project discord server and plan world domination.

Posted in Learning Lean, undergrad maths | Tagged , | Leave a comment

Summer projects 2020

I had planned to work with a bunch of Imperial College London mathematics undergraduates this summer, formalising arbitrary mathematics in Lean. I did this in 2018 and it was really good fun.

Now it looks like the College will be closed over the summer, but the students seem to still want to do it, so we’ll have to do it remotely. This means that there is now no longer a requirement that the students have to be in London (it will be less ideal than in 2018, but we have to live with this anyway). On the plus side, it means that it will be easy to slot other people in, which means that I can open it up to mathematics undergraduates anywhere in the world, in theory. So that’s my plan. We can write collaborative code on CoCalc, I can give lectures and live coding sessions on the new Xena Discord server, we can chat and hang around with world experts on Zulip, all the infrastructure is there. I have put up a preliminary page here with some details, and more is to come. The plan is to meet on Tuesdays and Thursdays, during working hours UK time, starting on Tuesday 30th June 2020, and running to Thursday 27th August.

If you are an undergraduate mathematician and want to learn how to write proofs using a computer program, and have some time over the summer, then this might be a good way to meet other people with the same interests.

Ideally students will already know a tiny amount about Lean before we start. The natural number game is one place to start. During May and June I hope to record a series of “ten minute Lean” tutorials. Currently there is only one, because I have not really worked out how to YouTube, but I will get there. There are also some basic maths Lean questions on CoCalc and a growing list of Lean kata at Codewars, and once you have installed Lean and the amazing leanproject tool you can download the tutorial project which currently contains one tutorial, but more are in the pipeline. OK so I have a lot to do. But so do you! And we have two months to do it, right?

I think I would be naive to think that I am going to end up swamped. This is in some sense pretty niche material. But people will be able to help each other, once we all get going, and I think it will be fine. My university teaches maths undergraduates how to write python and how to write LaTeX, and I don’t see any reason why they shouldn’t learn to write Lean as well — I think that doing problem sheets in Lean is a cool thing to do. I give out some of my problem sheets in Lean format nowadays, and the best thing about it is that I don’t need to mark any Lean solutions because they are guaranteed to be correct πŸ˜€

If you know any undergraduates who might be interested — pass the news on! We’re going to be formalising any kind of pure maths at all, from “do the exercises in this basic group theory book” to “formalise the basic theory of C-star algebras”, from “formalise a solution to this recreational puzzle” to “prove the fundamental theorem of Galois theory” — anything, as long as it is well-defined pure maths, is fair game. It will be interesting to learn what maths is currently hard and what is currently easy to do in Lean, and the best way to find out is by trying.

This might just look like a bit of fun, but it is really a research project. Humanity really still does not understand what the best foundational system is for doing the kind of mathematics which mathematicians do, and indeed Larry Paulson and Martin Hyland both independently told me that the best system depends on the kind of mathematics you want to do. But I now believe that this is not an acceptable answer. When I was a 3rd year undergraduate there were 12 pure mathematics courses on offer at my university, and I sat in on all 12 of them, just to see what was going on in them. They covered algebra, analysis, topology, geometry, number theory, and logic. I noticed when I was a post-doc that my subject area, algebraic number theory, used stuff taught in every single one of the courses I had seen during that year. Number theory is 2000 years old and has learnt to borrow from many other areas of mathematics. I believe that one day computers will understand the kind of mathematics that is going on in my PhD thesis, but for that to be happening we have to see it all going on in one system. I believe that projects like the one I’m describing above will show us strengths and weaknesses in Lean. If you think about it this way, failure = success, because if you decide to formalise X and then it turns out 8 weeks later that a simple looking mathematical proof turned out to be really hard to do in Lean, then actually this might be an important data point.

Posted in Imperial, Learning Lean, Uncategorized, undergrad maths | Tagged , | 2 Comments

The invisible map

Let’s talk about writing computer code which corresponds to mathematics.

The basic idea: our code will correspond to mathematical definitions and proofs, and our code will compile if and only if our proofs are correct. Such systems do exist — but in this post, we will just imagine what this kind of code might look like, and how easy it would be for a mathematician to write it. The “de Bruijn factor” of a system like this is the ratio (size of program which proves a theorem in our system) / (size of LaTeX file which proves the same theorem), and ideally this number should be small.

The question we immediately run into is: what will our logical foundations be, or in other words which computer language we are going to use to write our computer code. Most mathematicians either know nothing about foundations (they just know that maths works, like Gauss and Euler knew), or they know that one possible choice for a foundational system is “set theory”.

Set theory

OK now let’s imagine writing code in a computer language corresponding to set theory. So what do we have? Well, we have one kind of object in this system, and it’s called a set. Everything is a set. Those set theory people have checked that what we call functions can be encoded as sets, an ordered pair or ordered quadruple of sets can be encoded as a set (in more than one way, so we just choose a way and stick to it), and even everyday objects such as groups and rings can be considered as sets. For example, a group is an ordered quadruple (G,m,i,e) with G a set, m:G\times G\to G a function called multiplication (remember that m is actually a set), another function i:G\to G (inversion) and finally an element e \in G called the identity element. Even e is a set, because everything is a set. However asking what the elements of e are is a “wrong question” in group theory somehow.

Ok so now we’re writing computer code, and we have variables because computer code has variables, and we have some variable M, and it’s a set. But actually we are doing algebra, so we’re not actually thinking about M as a set, and looking it, actually we can see that M is some kind of ordered triple, and it is called M, and so it is probably a monoid, or a module, or a metric space or something. Except that it isn’t, it’s just a set. We might accidentally call two things M (who hasn’t seen this happen in maths lectures!) and this might lead to hard-to-debug problems. What’s even worse, is that in theory the set M could genuinely represent more than one mathematical object. Perhaps somebody writing the library on natural numbers decided to define 3 to be the set \{0,1,2\}, and more generally they defined n to be the set \{0,1,2,\ldots,n-1\}. Then someone doing topology defined a topology on a set X to be a set of subsets of X satisfying some axioms. It then turns out that 3 is a topology on 2 (check it! It’s really true!). Someone making the library for symmetric groups had to decide how to make the symmetric group S_n on n elements, and they decided it was going to be permutations of the set \{1,2,3,\ldots,n\}. Now think about what S_n actually is if you do it this way — it will depend on your definition of ordered quadruple, but will ultimately be just a set whose elements are sets which will happen to be things like numbers, or sets of numbers, or sets of subsets of numbers, or sets of numbers which happen to also be numbers by coincidence. That’s all it is. And now imagine someone else doing some basic combinatorics who is looking at a question about collections of subsets of \{1,2,3,\ldots,n\}, and then it turns out that S_2 is by complete coincidence an example of such a subset. Do we really want M to genuinely represent more than one thing? What happens when we want to change the variable M to be something else? “Let x=x+1” is an actual thing in computer code! When changing the topology on our set X, could this mean that the meaning of the number 3 changes in a different part of our code? It might be funny that one way of setting up the natural numbers means that 3 is a topology on 2, but it might also have unintended consequences.

We can’t just let everything be a set. We will get impossible-to-debug errors. We need more structure. Here is an analogy.

Programming in assembly language

When I was a kid, I had an Acorn Atom computer, which could be programmed in two languages. One of them was BASIC. Variables in basic could be strings or integers, for example. A string couldn’t be an integer — this made no sense. But I could not write good graphical computer games in BASIC because it was too slow. So I had to learn the second language which this machine understood, which was 6502 Assembly Language. The 6502 processor was an 8 bit processor. In 6502 assembly language you had three variables A, X and Y, each of which was a number between 0 and 255, and you also had the concept of a “memory location”. A memory location was a 4-character hexadecimal string which pointed to a portion of memory on a computer chip which contained, guess what, a number between 0 and 255. Everything was a number between 0 and 255. Some of those numbers corresponded to whether a certain line of 8 dots on the screen were black pixels or white pixels. Some corresponded to links to hardware — for example the bit corresponding to the position 2^2 at memory location B002 was connected to the internal speaker, so by continually adding 4 to this memory location one could make the computer beep. But it was still possible to write code. When I wrote code, I had to decide that certain memory locations would represent coordinates of objects on the screen, other memory locations would represent the black and write pixel drawings which I would draw at these locations, other memory locations would represent the velocity of the objects I was drawing and so on. I would typically plan out on a piece of paper which type of object was being stored at each region of memory. It is possible to write code in this way, just like it is possible to write computer code which does mathematics in bare set theory. But we do not teach assembly language to first year computer science undergraduates because it is much easier to learn to use a language like Python or C++ where there is some kind of typing system, where you see a variable x and you can ask “what are you, x?” and get a useful answer such as “I am a list of real numbers” or “I am an integer”, rather than “I am a number between 0 and 255, so I hope you are keeping track yourself of what I am supposed to represent”.

Fixing set theory

OK so this is easy to fix. Let’s make a typing system for our set theory programming language. Let us actually give up on the idea of letting a variable M in our programming language represent a set. We will make it so that the only things we will allow as variables will be ordered pairs. If M is a variable, then the set M will be an ordered pair (n,X), where X is the actual set we are talking about, and n is a natural number. And then we will simply make a list:

  • 0 : set
  • 1 : group
  • 2 : ring
  • 3: field
  • 4: metric space

and so on. The idea is that the natural number n will tell us the “type” of the set X. Now we can figure out if M is a module or a metric space by looking at its type (the natural number). We will no longer have an issue with the “bare set” X coincidentally being interpretable as two or more things, because each time we use it, it will come with its type attached. Problem solved! That’s true — but another problem has appeared.

Is a field a ring?

Every field is a ring. Every mathematician knows that. Except that in our new “typed” system, it is no longer literally true that a field is a ring. A field is a pair (3,F) and a ring is a pair (2,R). So what we actually have now is an “invisible map”, which takes a field (3,F) and spits out a ring (2,F). The functions can be more complicated than this in fact — every ring is a group under addition, but remember that a ring is something like an ordered sextuple or whatever, whereas a group is only an ordered quadruple, so the function sends (2,(R,+,-,\times,0,1)) to (1,(R,+,-,0)) — it is a slightly more complicated function than you might think. Every metric space “is” a topological space but when you think about it, this invisible function is actually quite involved, because you have to make the topology from the metric. Mathematicians ignore these functions, and furthermore it is absolutely fine to ignore these functions in practice, but if you are writing a formal proof verification system then you have to decide how to deal with this. You either make it untyped, in which case it really is true that every field is a ring, but some fields might also be topologies by accident and you run the risk of really-hard-to-debug errors later on — or you make it typed, in which case it is no longer true that every field literally is a ring, but there is an invisible function which sends fields to rings. Such a system needs to have some good system of invisible functions — or coercions, as they are called in computer science: “take this object of this type, and let’s just pretend it has that type instead, by applying this function without even mentioning it”.

Invisible functions

Lean, and indeed all the other interactive theorem provers I have ever used (i.e. Coq and Isabelle/HOL), use some kind of typing system, because they are all designed by computer programmers, and computer programmers for some reason have an aversion to designing systems where natural programs might end up with incredibly-hard-to-debug errors. The typing system is baked into the core of these systems, and invisible functions are everywhere. The natural numbers are defined in these systems. By adding additive inverses we get the integers; by adding multiplicative inverses of non-zero elements, we get the rationals. In Lean the reals are defined to be equivalence classes of Cauchy sequences of rationals. Now ask yourself this question. Is a natural number a real number? No it is not. How can we fix this? Well here is a proposal: we could make a new hybrid object which contains all real numbers which aren’t natural numbers, represented as Cauchy sequences, and then stuffs in the original natural numbers in, in place of the real numbers which are actually natural numbers. We now have to deal with the complaints from the number theorists who are working with the rational numbers and want to represent a real rational number as an equivalence class of pairs of integers rather than a Cauchy sequence, and complaints from the computer scientists who now have to write a really ugly hybrid addition function on those reals, of the form “just add Cauchy sequences in the usual way — oh — except if the answer happens to be a natural number, in which case do something else”, especially because there is no algorithm to answer the question “is this real number a natural number” in general (take some problem where you have some integral coming from physics or whatever, and the conjecture is that that the answer is 42, and this has been checked to 1000 decimal places, but nobody can prove it: such questions do exist).

OK so here is another proposal: we just define an invisible function which takes a natural number n in and spits out the corresponding real number n. And guess what, it works. This function is invisible to mathematicians but in Lean it is there.

“A subgroup of a group is itself a group”

We finally get to what motivated me to write this post, which was a Twitter exchange I had with Tim Gowers, Andrej Bauer and others in March, during which point Tim said “I still don’t really understand the problem. A typical book on group theory will point out that a subgroup of a group is itself a group”. There is no problem Tim — a subgroup of a group can certainly be thought of as a group, and certainly for a mathematician it will do no harm to do so. But it turns out that typing systems turn out to be (a) really powerful and (b) really useful, and one thing we learnt in Lean over the past two years is that it turns out that if G is a group then it is worth letting subgroups of G have their own type! Mathematicians and computer scientists are working together using Lean and other systems, and are trying to figure out the best typing system for mathematics, and it is an interesting question which is as far as I can see not particularly well understood, although we are getting there. Types in Lean are unsurprisingly indexed by strings of characters, not natural numbers. For example Group is a type, and subgroup G is a type. And there’s an invisible function from subgroup G to Group. And it doesn’t matter. But it is actually there. Hence, in Lean, it is strictly speaking not true that a subgroup of a group is a group. But it doesn’t matter.

Something to cheer us up

Independent of all that, my teenage daughter is stuck at home and is doing art. Here is some.

Posted in Type theory, undergrad maths | Tagged , , , | 7 Comments

No errors.

Glasgow.

Before I start, a word on Glasgow. I am really disappointed that I will not be going to the Postgraduate Combinatorial Conference 2020 up there in April. Bhavik Mehta and I were going to run a one-day workshop on Lean. We told the students to warm up by playing the natural number game, we were going to do some simple graph theory stuff, and then Bhavik was going to show off his Combinatorics in Lean repo, where he proves, amongst other things, the Kruskal-Katona theorem. Bhavik is now working with a team in Cambridge on topos theory in Lean. As Mario once said — when I was complaining about breaking changes being made in mathlib — “you can’t stop progress”.

I went to Glasgow to speak at a very enjoyable BMC in 2001. I thought the indie record shops were great too. I had plans to go there twice in the near future — once to the PCC, and once to the joint BMC/BAMC meeting, where I was going to speak about Lean; of course this has also been postponed. I very much hope to get back to Glasgow in the near future — it’s been too long.

The other reason I am disappointed was that I was really looking forward to see how a room full of intelligent mathematics PhD students would react when asked to fill in a sorry with essentially no Lean training other than the natural number game, and then how much further we could see them go over the weeks beyond. I was very interested in watching them learn. I find it more interesting watching people learning in real life rather than in a chatroom. Maybe I should do more stuff in my Discord Lean server?

I have been thinking about teaching in general, and talking to learners who I meet on the Zulip Chat like Shing Tak Lam, who had mathematics and computer science A-level exams scheduled for May and is now faced with months off school. Shing decided they would try doing a question from one of the past STEP exams in Lean, and they’ve managed to do it! I think it is very interesting that they have, very early on, noticed our brand spanking new documentation — many many thanks to Rob Lewis and all the others involved in making it happen. It is opening doors for newcomers.

But let me get to the point: a tip for beginners who want to know why their code doesn’t work.

No errors

A few months ago I isolated what I think is a basic principle in teaching Lean to people — it’s the concept that when you’re working on your code, you should try to keep it from having any errors. If you are stuck on something, then you might well have an error in your code. But in this case you should have just one error, and you should be able to fix this error with one sorry. Errors are bad. Aim for no errors.

How do you know if you have no errors? Say you have just finished writing a tactic mode proof in Visual Studio Code or on CoCalc, and you are about to enjoy the buzz which goes with solving another level of the Lean maths game. Just before you do, I think you should just check that there are no errors anywhere in the file you are working on.

That picture of the bottom left hand corner of my VS Code window (it’s a level in the group theory game which I am designing) has a “tick” by the word “Lean”, meaning “I finished compiling and there are no orange bars”. There is also an x in a circle, and a 0 by it — “no errors”. If there are no errors, then you are winning. If there are no errors and also no warnings, you have won. In Cocalc just look at the All Messages window and it’s the same thing — look for a tick at the top, and then check for red errors.

Sometimes I see students whose file is absolutely full of errors. Their file is 400 lines long, getting really slow, and has 23 errors. They ask me why something doesn’t work, and I know from experience that the answer might be of the form “because something you wrote 100 lines up which caused an error and means that things aren’t the way you think they are”. Some people can get into a real state. They’re in a tactic mode proof and Lean is simply not printing the tactic state, or they have an error which just says sync. This post is to just cover some of the basic problems which I’ve seen people have, and how one might attempt to solve them.

The right way to proceed when you have a file with 23 errors is to click on this icon in VS Code

Opening the Lean Messages window in VS Code

to get the “Lean Messages” window. In CoCalc this is called the “All Messages” window and you don’t need to click anything — it should already be there. In this window you will be able to see all the errors and warnings in your code. In the online Lean web editor the icon you want is the same but they are in the top right. The warnings are in orange, the errors are in red. Let’s try and tidy up this output.

  • Some of the “warnings” might just be debugging output — output of #check commands for example. Why not just comment those out or delete them? If you want to know the output of a #check command, why not just paste it as a comment in your code like this?
/- trying to figure out how to use insert.

#check @set.insert

set.insert : Ξ  {Ξ± : Type u_1}, Ξ± β†’ set Ξ± β†’ set Ξ±

-/
  • Maybe some code is just old and doesn’t work and you don’t want to think about it right now. Just comment it all out with /- ... -/ or move it to another file. This might be a good time to think about whether the file you’re working on has a good name. Too many files called things like scratch73.lean or test1.lean is not a great way to organise your work in a project. Are you proving lots of theorems about groups? Why not call the file groupstuff.lean and move all of the non-group stuff to somewhere else?
  • Locate your first error. That’s the one we’re going to work on. If you’re in the middle of a proof and you don’t know how to continue — don’t leave it as an error. Say sorry. Get rid of all the errors you’re not interested in, until we find the first error which you do not understand. That’s the error we should be working on. If it’s not the one you want to work on — comment it out. If your code breaks when you comment it out, we might have just located the actual problem.

When you have located the first error, let’s take a look at what it is. Sometimes with beginners I see errors like invalid expression or sync (although sync is not usually the first error). These are errors which say that the structure of your tactic proof is messed up. A tactic proof is supposed to be a sequence of tactics separated by commas. A comma-separated sequence of tactics within a { } block is considered as one tactic. Two very common mistakes: to forget the tactic (“Why doesn’t mul_comm work?” “Because you have to use the rewrite tactic: write rw mul_comm “) or to forget the comma (which usually causes no end of confusion because Lean then thinks that the name of the next tactic is an input to the tactic before and there is probably no variable called apply). As a general hint: if you have invalid expression under a } then there is probably no { and you might want to delete it. In general if you have an invalid expression, try getting rid of it. Try adding a } or a , or an end to see if they’re valid expressions. See if you can make the expression valid. If there are unsolved goals, try sorry. If there are lots of goals, try { sorry }, — that might get rid of the first one, and if it’s the one you’re interested in then try working within those brackets. Try and tame the situation. You know that you can use #exit to completely abort Lean just after your first error? I had an error in a Lean file today and I just wanted to make 100% sure that it was isolated away from everything else, so I wrote this (and it took a little time to figure it out):

  ,sorry

  ,},sorry end #exit

I was in the middle of a tactic mode proof. After the sorry (which changed the error into a warning), I then figured out from experimenting and looking at errors that Lean wanted some combination of commas, sorrys and an end, and then I got out with #exit and all of a sudden compilation time shot down. I can now work on this error properly.

Once you just have one error, if you’re in tactic mode, you can now try and solve it. Safe in tactic mode you can switch back to info view in VS Code or the online web editor using this symbol

How to switch to info view in VS Code

(or just look at the window called “Info at cursor” on CoCalc) and you should be able to see the tactic state and any error messages which you generate.

The error won’t go away

If you simply cannot understand the error message, or if you understand the error but don’t know what to do about it, then ask on #new members. Change the error into a sorry, so that the code now compiles with no errors, and post all the code including all import statements — all the code up to and including the problem — to the chat and also quote the exact error. If an expert sees all your code and your error message then they might be able to solve it while they’re on their phone without even firing up Lean. I am really bad at second-guessing what people mean — they are talking about something so they obviously assume that we all know they have imported some file or other — but I don’t know my way around parts of the mathlib library at all. Please post working code when you are asking about errors. If I can’t cut and paste it and reproduce your issue — I am far less likely to open my mouth and try to say something helpful.

I learnt very on in my Lean career that it was really important to learn to read error messages. Errors are bad. Error messages is like losing life in Zelda. If you are on no errors, you are on 100% health. Aim for no errors. If there are no errors in your file — are there errors in your project? An error-free project is a healthy project. Aim to keep your projects free of errors, but feel free to litter them with sorrys. The perfectoid project was always full of sorrys while it was in development. We started by writing the definition of a perfectoid space and we sorried a part of it, and that sorry was there from the start. But whenever we pushed code, we did our best to ensure that it did not contain any errors.

If your code is too long, too amateurish, not remotely at mathlib standard, or runs on Lean 3.3.0 and the mathlib you happen to have on your computer — that is absolutely fine by me. If the goal was to fill in a sorry, and the sorry is gone, and there are no warnings and no errors, then you beat the level and you get the credit. Over on the Lean chat there are level-creators and level-solvers. I myself like to do both (current levels: commutative algebra related to the Nullstellensatz), but if you’re a beginner wanting to get into Lean, then you can start by finding some other levels out there in the wild, like these ones on CoCalc and all the ones which are thrown up every day by people asking questions on the Lean chat. Can’t go to school? Try solving some exam questions in Lean! Aim for no errors!

Posted in Learning Lean, Technical assistance, Uncategorized | Tagged , , , | Leave a comment