My last post was, amongst other things, a challenge for the community behind every modern computer proof verification system to start formalising “proper mathematics”. This term has some problems, so how about the equally vague but perhaps less offensive “fashionable mathematics”. What mathematics is fashionable? Just take a look at the work of the recent Fields Medallists. That’s a pretty good way of telling.
But fortunately, unlike many other fashions, “fashionable mathematics” is not controlled by the whim of big companies or some cabal. Fashionable mathematics is mathematics which justifies itself by its ability to answer questions which have been previously deemed interesting or important. Peter Scholze’s definition of a perfectoid space opened a door. In the last ten years, perfectoid spaces have been used to prove new cases of the monodromy-weight conjecture, to prove the direct summand conjecture, to give a new proof of purity for flat cohomology, a strengthened version of the almost purity theorem and so on (and I didn’t even mention applications to the Langlands philosophy). These are results whose statements do not mention perfectoid spaces, and some have been open for decades. This is what makes this kind of mathematics fashionable — it is giving my community new insights.
Each formal proof verification system (Lean, Coq, Isabelle/HOL, UniMath, all of the others) has its own community, and it is surely in the interests of their members to see their communities grow. These systems are all claiming to do mathematics, as well as other things too (program verification, research into higher topos theory and higher type theory etc). But two things have become clear to me over the last two years or so:
- There is a large community of mathematicians out there who simply cannot join these communities because the learning curve is too high and much of the documentation is written for computer scientists.
- Even if a mathematician battles their way into one of these communities, there is a risk that they will not find the kind of mathematics which they are being taught, or teaching, in their own department, and there is a very big risk that they will not find much fashionable mathematics.
My explicit question to all the people in these formal proof verification communities is: what are you doing about this?
Now you — I don’t mean an individual — I mean you as a community of Coq users or Isabelle/HOL users or UniMath users or whatever — you might decide that these things are not important, and hence the answer is that you are doing nothing. You might simply decide to reject the idea that formalising fashionable mathematics is important. And this is fine. But, in return, don’t expect us to come and join your community. You might not want us! This is fine! But we represent true potential for growth.
What some of us mathematicians believe is that at some point in the future, it’s not completely out of the question that one or more of these systems actually start becoming useful for our research. But what is completely clear is that if none of these systems actually know what the class group of a number field is then this is a rock solid proof that the systems cannot currently be used to help us prove even basic results about class groups of number fields, let alone new results.
I have had extensive conversations with people interested in univalent mathematics. I initially rejected univalent mathematics completely because its “abuse” (as I initially saw it) of the equality symbol was so obscene to me. Mathematicians use the equality symbol (i.e. ) to mean two things. Firstly, they use it to mean that and are actually the same thing (for example ). Secondly, they sometimes use it to mean that and are canonically isomorphic, and no I am not going to tell you what this means, but I can assure you that if is a ring and is the zero ideal, then . We don’t care that they’re not literally the same set, they are equal. But univalence takes this much further — univalence tells us that and are equal if they are “equivalent”, and if two things biject with each other (whether or not the bijection is “canonical”) these things are equivalent. This might be a nice way of doing homotopy theory, but this use of the equality symbol to denote a very weak kind of equivalence does not translate well, for me, into the rest of mathematics, and if you’re going to build all of fashionable mathematics in univalent type theory then maybe this will cause you problems. Will it? Nobody knows because nobody is doing it.
What I have noticed amongst the univalent people is that, more than any of the other communities I’ve run into, they really do not seem to care about doing “fashionable mathematics”. I would love to be spammed with comments telling me that I was wrong about this. But my impression is that there are a whole bunch of interesting type theory questions raised by the univalence axiom, and that these foundational questions are what the community is on the whole interested in. I have asked lots of univalent people how it could possibly be the case that Voevodsky, someone who made their name by discovering a homotopy theory for schemes, could spend 15 years working in univalent type theory and still not have a definition of a scheme at the end of it. It has been explained to me, on more than one occasion, that Voevodsky’s interests changed. This is fine. But I still want the schemes. Here is a message for you univalent people — if you do not actually build some fashionable mathematics at some point, then we will not come in our masses. Where is the definition of a scheme? Where is the proof that the class group of a number field is finite? Where are number fields, for that matter? Can you really show me that it does not matter that all number fields are countably infinite, and hence biject with each other, and hence are equal, in your system? I know that’s not how it works and there’s more to it than that. But I don’t want to hear protestations, I want to see the code. UniMath, Arend, any system you like. I know you’re good at higher topos theory but where is the arithmetic? Where is quadratic reciprocity?
Coq users: you have a mature system which has been around for decades and is tried and tested. You have formalised several very difficult proofs about undergraduate-level mathematical objects such as planar graphs and finite groups. You have done lots of computer science things which I do not understand too. But where are the MSc level mathematical objects? Where are the schemes? Coq is French! Schemes are French too! It’s a match made in heaven! Where are the statements of local and global class field theory? Assia Mahboubi is someone who is actually doing mathematics in Coq which “proper mathematicians” are interested in. She cannot do it alone! Where is the manual which tells mathematicians who have no idea what a type is but know what a Noetherian ring is, where to start? What if an undergraduate wants to try formalising the Hilbert basis theorem? What do they do? Ask on the mailing list? You know that undergraduates don’t actually use email any more, right? I am told by my teenage children that email is for old people. Where is the way in for us? [Note added 14th Feb: thanks to Théo Zimmermann for pointing out to me on Twitter that Coq has a Discourse forum. Young people wanting to learn Coq — try asking some beginner questions there. Ask how to make class groups of number fields! Let’s get more serious mathematics done in Coq! It’s an extremely powerful system! ]
Isabelle/HOL: Manuel Eberl is tirelessly generating 20th century analysis and analytic number theory. This is a highly respectable thing to do — he is planting the seeds. He is doing the basics. He cannot do it alone! Furthermore, HOL has no dependent types. Does this mean that there are entire areas of mathematics which are off limits to his system? I conjecture yes. Prove me wrong. Can you define the Picard group of a scheme in Isabelle/HOL? I am not sure that it is even possible to write this code in Isabelle/HOL in such a way that it will run in finite time, because you have to take a tensor product of sheaves of modules to define the multiplication, and a sheaf is a dependent type, and your clever HOL workarounds will not let you use typeclasses to define module structures on the modules which are values of the sheaves. So how will you do the tensor product? I don’t know. Does anyone know? Is this actually an interesting open research problem? Picard groups of schemes are used all over the place in the proof of Fermat’s Last Theorem. They are basic objects for a “proper mathematician”. What can Isabelle/HOL actually do before it breaks? Nobody knows. But what frustrates me is that nobody in the Isabelle/HOL community seems to care. Larry Paulson says that it’s easy to understand: different kinds of maths work best in different systems, and so you might want to choose the system depending on the maths you want to do. But do you people want to attract “working mathematicians”? Then where are the schemes? Can your system even do schemes? I don’t know. Does anyone know? If it cannot then this would be very valuable to know because it will help mathematician early adopters to make an informed decision about which system to use. [Notes added Feb 14th: Josh Chen told me on Twitter that Isabelle has a Zulip chat like Lean! Mathematician beginners — go there and ask some questions about how to do basic maths in Isabelle! Furthermore, Manual Eberl has sent me what he claims is a formalisation of sheaves in Isabelle. But he does not profess to know anything about sheaves — mathematicians who want to learn about sheaves could try using it! Ask him about it in the chat! Let’s get some 21st century mathematics formalised in Isabelle/HOL! ]
Finally — mathematicians. Is it not easy to believe that at some point in the future, one or more of these systems will be helping us to do mathematics? Are you interested in making this happen sooner? Then why not get involved? In your spare time, learn how to use one of these systems. If you have time, learn how to use all of them and then figure out which one has the most potential. How to learn a system? Think of a maths question that you want to state or prove (could be anything from solving a simple logic problem to stating the Poincare conjecture), and then start asking how to do it. If you want to try Lean then you can ask on the Lean Zulip chat (login required, real names preferred, be nice). Here you find a community of mathematicians and computer scientists who are working out how to communicate with each other, and are isolating specific problems in the way of getting fashionable mathematics into Lean, and then solving them. Somebody there will be able to answer your question. We know exactly what Lean 3 can do in theory and has done in practice, we know where the problems are and we are hoping that they are fixed in Lean 4. But it doesn’t have to be Lean. Try any system! Get involved! It’s fun! It turns theorem proving into solving levels of a computer game. There are some areas of basic mathematics where you have enough control to make this quite a fun computer game, and as time goes on more API will appear, and levels in more and more areas of mathematics will become available. Computer scientists are really interested in how we solve these levels, because they need data. Sarah Loos from Google AI explicitly raised this issue with me at AITP last year. She was bemoaning the fact that in a typical database, a theorem will have exactly one proof. Everyone knows that different proofs can add different value to a situation, by giving different insights. She wants more proofs! These people need our input! But we can’t use the systems so it’s hard for us to give it to them. Learn a system! Prove a theorem! Write a function!