Here is an overview of my current thoughts on formal proof verification systems in modern mathematics.
3d computer modelling software such as Blender can make virtual versions of abstract 3d mathematical figures such as truncated dodecahedra and so on. This has random cool consequences. For example this means that 16 year olds can make random cool videos about fractals.
Lean is a system (one of many) where we can make virtual versions of far more complex mathematical objects. Mathematicians no longer have to imagine them in their minds — they can create them and manipulate them in a virtual world. This virtual world is really bad at allowing mathematicians to manipulate objects in the intuitive and fluid way that mathematicans think about concepts. However it is really good at checking that at the end of the day, any precise ideas which come out of the fluid experiments and manipulations which our brains seem to be so good at, are well-defined, clear, and correct. The virtual world is an exceptionally good place for mathematicians to be able to clearly discuss whether or not a given proof is correct, for example, and to very precisely pinpoint places where more details need to be supplied. The virtual world is black and white. It is a computer model of formalist’s world of mathematics, where if something compiles, it is correct, and if it does not compile, it is not correct. There is no longer any debate. It is pure mathematics, the way pure mathematics is meant to be done, and needs to be done. What are we, as pure mathematicians, without rigour?
The exciting thing about Lean in particular, is not that not only is this theoretically possible, it is actually happening. 15 months ago I had never used a theorem prover. But I made schemes with the help of some friendly mathematicians and computer scientists, that I met at the Lean Zulip chat, and we are now making perfectoid spaces. The speed at which new things are appearing is terrifying. We got modular forms yesterday. Group cohomology is easily within our grasp, we just need to find the manpower to do it. We don’t even have real manifolds yet, but we’ve got the upper half plane, and I bet you we’ll have real manifolds by this time next year. What area do you work in? You should be interested in knowing where we are up to. Come to the Zulip chat and ask us what needs doing before you can state your favourite theorem in your area in Lean. There is a non-zero chance that we can state it right now. There is a non-zero chance that your conversation with us will end up with a new feasible target for us to aim at. There is a non-zero chance that we will be able to state it in Lean by this time next year.
But why? Why bother formalising definitions of complex mathematical objects and statements (theorems, conjectures, questions) about these objects?
In some sense, my answer is — because it’s fun. And it’s going to happen whether or not you care, and the sooner that we as a community of pure mathematicians care, the sooner we will be able to have great new ideas about what to do with these virtual objects. Moreover, there is funding.
What I think the correct question is, is “What shall we try and do with these objects, now they are appearing?”. Here are some answers to that.
a) Maybe one day we will be able to make cool search.
b) Maybe one day we will be able to get AI to look at what we’ve done and suggest more stuff.
c) Maybe one day we can start trying to check proofs, or at least start thinking about how certain theorems imply other theorems.
d) Maybe right now we will be able to use these objects to make our teaching of undergraduate mathematics better. Undergraduate mathematics students at Imperial College London pay over £9000, and in some cases far far more, for the privilege of spending one year at this institution, and they deserve an exceptional service for this. I am integrating Lean into my teaching and every year is a new experiment. I am going to keep experimenting until I get it right.
d) Maybe right now we should try to make formalising statements of research theorems the new normal. Mathematicians changed from typewriters to LaTeX. They can change again. Formalising statements is quick, if all the right definitions are there, and if the mathematician has been trained. Let’s formalise definitions and then let’s train mathematicians to formalise statements of their theorems.
Why right now? Because now is good. Here is my personal story. As I already said, 15 months ago I had never heard of the Lean Theorem Prover, and I had never used anything like a theorem prover in my life. Then in July 2017 I watched a live stream (thank you Newton Institute!) of Tom Hales’ talk in Cambridge, and in particular I saw his answer to Tobias Nipkow’s question 48 minutes in. And here we are now, just over a year later, with me half way through perfectoid spaces, integrating Lean into my first year undergraduate teaching, and two of my starting second year Imperial College undergraduate students, Chris Hughes and Kenny Lau, are both much better than me at it. The links are to their first year undergraduate projects, one a complete formal proof of Sylow’s theorems and the other an almost finished formalization of the local Langlands conjectures for abelian algebraic groups over a p-adic field. It’s all open source, we are writing the new Bourbaki and I cannot see it stopping. I know many people don’t care about Bourbaki, and I know it’s not a perfect analogy, but I do care about Bourbaki.
Mathematics is built on rigorous definitions. Computers are now capable of understanding many more mathematical definitions than they have ever been told, and I believe that this is mostly because the mathematical community, myself included, just didn’t ever realise or care that it was happening. If you’re a mathematician, I challenge you to formalise your best theorem in Lean and send it to Tom Hales! If you need hints about how to do that, come and ask us at the Lean Zulip chat. And if if it turns out that you can’t do it because you are missing some definitions, find a computer scientist with some experience in using dependent type theory, explain the definition to them, and direct them to the Lean chat where they can find help on how to write the code which you need in order to state your theorem. Believe that this new technology will have a role to play in future pure mathematics research, even if we do not currently quite understand what it will be. It is here. It needs to be taught. Mathematicians — come and teach it what you are interested in and let’s see what we can make it do.
Xena 
Hi Kevin!
You pose the question “Why bother formalising definitions of complex mathematical objects and statements (theorems, conjectures, questions) about these objects?”; and you offer five responses. Answers A-C are all of the form “because one day we might be able to do X with them” [which, you imply, we can’t currently do]. The two answers marked D both seem to be begging the question: you don’t explain why it is beneficial to undergrads, or to paper authors, to use Lean or similar formal frameworks for their definitions and theorems.
Why should a working mathematician (such as myself) put in the effort to formalise the definitions of their favourite objects, or the statements of their favourite theorems — not in some potential future scenario, but *now*? How would it benefit them, or mathematics as a whole, to do so?
LikeLike
Hey David! I think that a working mathematician such as yourself should perhaps not put that effort in. I think you should find a mathematically literate computer scientist (of which there are loads) or a Lean-literate mathematician (of which there are far fewer) and tell them really carefully what an Euler system is, and get them to formalise it for you, and then they could formalise the statement of one of your recent theorems and then a computer would know what you have been doing recently. You could look over the formalisation of the statement, confirm that it looks like what you claim you are proving, ask questions of the computer scientist if you are not sure, and, once you are satisfied, you could then put your name on that formalisation statement and say that this is what you claim you did. And that would be kind of cool. And maybe you think it’s completely pointless. But there’s a way of looking at life where constructing a new Euler system is also completely pointless. I don’t look at life that way and neither do you. I regard your work with Zerbes and others as really important. I think it’s sufficiently important that we should formalise a statement of what you did and add it to Tom Hales’ database.
Here’s what’s going on. Computers are currently too stupid to read human text and spit out a formal statement of what the humans claim to have done. But a database would be interesting to have because AI works best with databases. So we have to make the database ourselves. And the easiest way to do that is to have a culture change, just like we had when I was a PhD student and was told that nowadays everyone is using something called TeX to write their thesis. I want to make formalising the statements of your theorems normal. My point is that it is pretty easy to teach now. What is missing is some definitions. Once the definitions are there and a good API for them, formalising statements of theorems will be easy. If everyone then starts doing it, making the database will be easy. Hence I want to teach lots of people how to do it. If you are not interested in teaching Warwick undergrads how to do it, and you are not interested in learning yourself, then I think it’s hard to find a good reason for you to learn it yourself.
In some sense, the reason I am working hard on Imperial’s students, is that part of me has given up hope of ever persuading the staff to learn it. The other reason I am working on the students is that it is teaching me how to teach it better. I’m setting problem sheets in Lean this year for the incoming freshers. I’ll teach them, not you, and then you just have to remember to tell one of them what an Euler system is.
LikeLiked by 1 person
> why it is beneficial to undergrads
The broad objective of undergraduate courses is to train methods of thinking and ways of doing, rather than specific facts (apart from the 1% of students that will become expert in that particular field, which are of course also important).
Currently the new “way of doing” is for computers to move beyond bookkeeping and calculating, and towards generating content – either verification (presumably not far off) or new discoveries (perhaps a little longer).
For what it’s worth, I dare say any future non-academic employer will be a hundred times more excited about graduates teaching a computer maths, than stating Sylow’s theorems.
LikeLike
I guess what I am offering to Imperial’s undergraduates is just a chance to learn something about what this software is and what it can do. I know very little about what non-academic employers are looking for; all I know is that if a student of mine goes off into a non-academic job then the company they go to work for essentially never asks me for anything other than an extremely short reference, if that.
LikeLike