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”.
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 with a set, a function called multiplication (remember that is actually a set), another function (inversion) and finally an element called the identity element. Even is a set, because everything is a set. However asking what the elements of 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 , and it’s a set. But actually we are doing algebra, so we’re not actually thinking about as a set, and looking it, actually we can see that is some kind of ordered triple, and it is called , 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 (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 could genuinely represent more than one mathematical object. Perhaps somebody writing the library on natural numbers decided to define to be the set , and more generally they defined to be the set . Then someone doing topology defined a topology on a set to be a set of subsets of satisfying some axioms. It then turns out that is a topology on (check it! It’s really true!). Someone making the library for symmetric groups had to decide how to make the symmetric group on elements, and they decided it was going to be permutations of the set . Now think about what 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 , and then it turns out that is by complete coincidence an example of such a subset. Do we really want to genuinely represent more than one thing? What happens when we want to change the variable to be something else? “Let
x=x+1” is an actual thing in computer code! When changing the topology on our set , 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 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 and you can ask “what are you, ?” 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 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 is a variable, then the set will be an ordered pair , where is the actual set we are talking about, and 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 will tell us the “type” of the set . Now we can figure out if 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” 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 and a ring is a pair . So what we actually have now is an “invisible map”, which takes a field and spits out a ring . 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 to — 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”.
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 in and spits out the corresponding real number . 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 is a group then it is worth letting subgroups of 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.