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.