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

Where is the fashionable mathematics?

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:

  1. 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.
  2. 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.

Univalent people.

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. A = B) to mean two things. Firstly, they use it to mean that A and B are actually the same thing (for example \sum_{n\geq1}\frac{1}{n^2}=\frac{\pi^2}{6}). Secondly, they sometimes use it to mean that A and B are canonically isomorphic, and no I am not going to tell you what this means, but I can assure you that if R is a ring and (0) is the zero ideal, then R/(0)=R. 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 A and B 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

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 users

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! ]

Mathematicians

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!

Posted in Algebraic Geometry, General, Learning Lean, undergrad maths | Tagged | 13 Comments

Lean is better for proper maths than all the other theorem provers

I apologise for the moronic title. I have learnt over the past year or so that the clever thing to do is to have stupid click-baity titles. That’s not the real title. Maybe a more sensible title is:

Checking “proper maths” on a computer. Which computer prover can do it best?

But actually even that is not a great title: I have had people expressing their concern with my use of the phrase “proper maths” — suggesting that I am perhaps implying that the kind of mathematics that some people do is not “valid” in some way. I am actually using the phrase with my British tongue firmly in my cheek, but I appreciate that this is not always clear so I should be careful.

I could just go with some completely well-defined

Checking EGA IV sections 8 to 11. Which computer provers can be made to do this?

Grothendieck’s EGA IV sections 8 to 11 is a great example of a “magic wand” in mathematics. It means that you can say “WLOG everything is Noetherian” and press on, the moment you realise you need a finiteness condition to proceed. You might even be able to reduce to the excellent case. Plenty of experts in arithmetic geometry have read the proofs, although the details are quite dry. I myself have bought the book, which of course is the next best thing. I have no idea whether young people have read the proofs. Some of the earlier ones are quite easy, they rely on little more than the observation that a finitely-presented map is the pull-back of a finitely-presented map between finitely-generated (and hence Noetherian, and also excellent) rings. But later on it gets thorny — the theorem which descends the property of flatness (Theorem 11.2.6) is hard won — but also very very useful. It should really be a tactic. Brian Conrad tells me that knowing the proofs (and not just the statements) enabled him to give alternative proofs of the algebro-geometric results in appendix A of Breuillard–Green–Tao.

This challenge is still perhaps too hard. But the correct challenge is much harder. The correct title is something like

Understanding the questions of modern mathematics. Which computer provers can be made to do this?

Think of any piece of what my “proper maths” colleagues would call respectable mathematics — e.g. formalising the definition of an algebraic stack, formalising the statement of the Poincaré conjecture, stating the Riemann Hypothesis. Formalise that in your prover — and then formalise a whole bunch of other pieces of respectable mathematics, and keep going until you have learnt what the limits of your prover are when it comes to modern mathematics. All these systems — Lean, Coq, Isabelle/HOL, Mizar, the other HOL systems, UniMath, Arend, and all the others — which of them can understand even the statements of modern mathematics? Can any of them? This is important to know! I’m not worried about the proofs — these systems are still missing definitions. Which of these systems can actually keep up with the “proper mathematicians”? This question is still really poorly understood, because (the penny has finally dropped) many of the users of these computer proof systems are simply not interested in this kind of mathematics. They may want to check that computer code has no bugs, for example, or do things which mathematicians were doing hundreds of years ago. This is why we have no real understanding of which systems mathematicians should be taking seriously. An MSc student at Imperial, Ramon Fernandez Mir, formalised the definition of schemes in Lean (pdf) (following work of myself, Hughes and Lau) but when we then looked to the other provers to see how they had done it, it turned out that none of them had. The communities are just doing other things.

Freek Wiedijk keeps track of 100 theorems to be formalised — but 95 of them are done now and FLT is just silly. We need new challenges. Here are ten off the top of my head:

  1. Formalise the statement of the Riemann Hypothesis.
  2. Formalise the statement of the Poincare conjecture.
  3. Formalise the definition of an algebraic stack.
  4. Formalise the definition of a reductive algebraic group.
  5. Formalise the definition of an adic space.
  6. State Deligne’s theorem attaching a Galois representation to a weight k eigenform.
  7. Do the sheaf-gluing exercise in Hartshorne (chapter 2, exercise 1.22).
  8. Prove sphere eversion.
  9. Do exercise 1.1.i in Elements of infinity-category theory by Riehl and Verity (note that infinity categories are used in section 5 of Scholze’s new paper with Cesnavicius so they’re probably here to stay).
  10. Define singular cohomology of a topological space.

Some are easy, some are hard, I just made the list up on the spot and tomorrow I could come up with ten different things. The list is also to a certain extent a reflection of my interests. I guess 1 is done in Isabelle and perhaps Coq, 2 and 3 are not done in anything as far as I know, although hopefully 2 can be done in Lean soon; 4 may be done in some system but it’s not the sort of thing computer people are typically interested in, 5 is done in Lean, 6 is I think a million miles away from anything in any theorem prover, 7 Kenny Lau did in Lean but it’s not in the maths library, it’s just bitrotting, 8 Patrick Massot mentioned in his talk in Pittsburgh, 9 because we have to start somewhere with infinity categories, and 10 because it is really hard to find any “proper” examples of any cohomology theories at all in any of the theorem provers. I have an MSc student, Shenyang Wu, working on group cohomology in Lean, he’s just defined cocycles and coboundaries this week, and it has been an interesting challenge. But unlike Freek’s list, I don’t think it’s good enough to get all ten done by the union of the theorem provers. The question is: which one prover can do all ten? I think all ten are within reach of Lean, even though it will take quite some time before we get there. But I am not convinced that the mathematical community in general is going to be taking any of these systems seriously until we show them that we can actually express modern mathematics like this in these systems. It is only when this starts to happen that mathematicians will be tempted in. And computer scientists do not seem to be motivated by these questions in general. That’s one reason that the area is moving far too slowly for my liking.

How many of these ten things can your favourite system do? Don’t you think it’s important that we find out the limits of your favourite system when it comes to modern mathematics? I’m not saying these things will be easy in Lean, but Lean’s maths (and more) library mathlib is somehow slowly steamrollering towards all of them in this slightly crazy/interesting way that open source projects work. The reason I’m backing Lean is that when it comes to the kind of questions like those above — accessible questions for theorem provers as they stand currently — I have seen Lean go from nothing to beginning to devour such questions, extremely quickly.

I am aware that many current users of these systems might not be interested in these questions. This is why we need new users. This is why we need documentation for mathematicians for all of these systems. Computer proof verification people — write documentation for mathematicians. Help us to learn your systems!

Mathematicians and theorem provers.

I have now watched so many mathematicians struggling with Lean, and sometimes not struggling with Lean, and it is now becoming clear to me what mathematicians can be expected to pick up quickly and what they will struggle with. One thing I have learnt about mathematics in the last two and a half years is that the formal mathematics that mathematicians do can be broken up into three kinds:

  1. Definitions. Things like the real numbers, or specific real numbers like pi. Also, abstract definitions like rings, homomorphisms of rings, schemes, and so on.
  2. Theorem statements. Things like Fermat’s Last Theorem, the irrationality of the square root of 2, the Birch and Swinnerton-Dyer conjecture, and so on. Just the statements.
  3. Theorem proofs. Proofs of the theorem statements.

All of these things of course have counterparts in the computer proof systems. Let me say something about what these things look like in a computer proof system. I’ll go through them backwards.

Theorem Proofs: These are the same as computer games. This is the mathematician’s favourite part. The natural number game is what happens if you take all the definitions and theorem statements out of the hands of the user, and just ask them to fill in the proofs, and give them enough of an API to make it fun. Bhavik Mehta made an impressive combinatorics repo and he told me that he never once had to think about how finite sets were actually implemented in Lean — he could just use the interface. Note that if you find yourself “grinding” (to use a computer game phrase), doing the same sort of stuff over and over again because you need to do it to make progress, then you can try to persuade a computer scientist to write a tactic to do it for you (or even write your own tactic if you’re brave enough to write meta Lean code).

But I have been formalising my undergraduate algebraic geometry course in Lean and occasionally running into missing API. This is just like some level in a computer game when you have to battle a big boss but you haven’t got the right equipment to make it easy, so you have to spend a lot of time hiding in corners and occasionally getting a hit in. For example I wanted the trivial fact today that if A, B and C were k-algebras, and A\to B is a k-algebra surjection with kernel I, and A\to C is a k-algebra homomorphism with kernel containing I, then there’s a k-algebra homorphism B\to C making the diagram commute. But this fact isn’t there, because the k-algebra API is not yet mature. This is frustrating. We will come back to this.

Theorem Statements: This is basically a simple translation problem, if all the definitions are there. For example if you want to say that a compact metric space is complete in Lean you just need to know how the people designing Lean’s maths library have formalised the concepts of metric space, compactness and completeness. Anyone who knows the relevant part of Lean’s maths library can do this — mathematician or computer scientist. Basically you have to know whether what you’re talking about is a predicate or a typeclass. For example example (X : Type*) [metric_space X] [compact_space X] : complete_space X is how one would say that a compact metric space is complete in Lean, and the proof is by apply_instance.

Of course one problem with theorem statements is that if the definitions are not there, you can’t make the statements. For example, as far as I know none of the systems can even state the theorem that the class group of a number field is finite, because although all the systems have groups, and the concept of finiteness of a group, none of them have the class group of a number field. This is completely standard “proper” undergraduate level mathematics and it just isn’t there in any of the systems, at least as far as I know. So of course this brings us on to

Definitions. This is the hard part. One reason it’s the hard part is that mathematicians are really good at defining a mathematical object to be three things at once, and then saying that a bunch of things are “true by definition”. An actual formalised definition is one thing, and then all the other ways of looking at it might correspond to little functions which pass from one type to another (perhaps equivalent) type. These little functions are of no importance to mathematicians, who cannot tell the difference between a subset and a subtype, or between the integer 3 and the real number 3, or between k^n and affine n-space, or between R[1/f][1/g] and R[1/fg], because in all these cases the two concepts are modelled in the same way in our brain. But the differences are unfortunately of great importance to computer scientists. The job of the Lean programmer is to turn a concept such as the real number 3 or an equivalence class of valuations or a perfectoid space, and to turn that concept into a string of 0’s and 1’s in a computer file in such a way that this string of 0’s and 1’s can be manipulated in the way a mathematician wants to manipulate it. This is where set theory/type theory comes in. This is like a programming language, saving us from having to actually play with 0’s and 1’s, or write machine code or whatever. We can turn a mathematical object either into a set or into a type, and then let the program do the rest of the job of turning it into 0’s and 1’s. A group G really is a four-tuple consisting of a set (also called G), a multiplication, inverse and identity, and some axioms. Or maybe just the multiplication, because we can work out the rest from the axioms. Mathematicians move freely from the group G to the set G, but to the computer scientists this might be a function application — or it might not, depending on how you set things up. An R-algebra homomorphism is also a group homomorphism and a map between sets. These things are not actually the same thing in some sense, however they are confused by mathematicians and this confusion causes no problems for us at all. Computer scientists on the other hand have got to fix one definition of an R-algebra homomorphism and then get some function coercion system going before they can treat this kind of thing working seamlessly. There is this whole host of tedious implementation issues which I really feel like I am not an expert at. Furthermore, this part is the hardest for mathematics undergraduates to learn, I think. Whether to make something a predicate or a typeclass, to extend another class or not, to use the old structure command or not — these are delicate questions in Lean and highly system-dependent in the sense that the same sorts of questions will come up in the other systems and the answers might be radically different. Our proofs are their programs, and if our definitions are bad then their programs will take a long time to run, their prover will become sluggish, and nobody likes lag in a computer game. Definitions are hard, and the computer scientists don’t even always know the right way to do them — sometimes I have been told to “try both ways and see what works best”. These fundamental problems do not seem to have been solved yet, and probably the best solution depends on which prover you’re using.

What is worse about definitions is that you can’t just make the definition — you have to make the API too. When I started with Lean, there were no complex numbers. It was a real freebie — the complex numbers could be defined as the type of ordered pairs of real numbers. I made the definition! And then I was told that I hadn’t finished yet — I needed to prove that they were a field, at the very least. I needed to define i, complex conjugation, the norm, and ideally polar coordinates as well, although this would need trigonometric functions and we didn’t have those at the time either. This sort of API-making is hard work and not particularly well-defined — you think you’ve done a solid job and then someone comes along and tries to use your definition and all of a sudden they are asking you to make ten more definitions or theorems, including perhaps some theorems which are “trivial in mathematics” and hence cannot be proved by mathematicians because the mathematicians have no clue what needs to be proved. For example after making the complex numbers, one has to prove things like: two complex numbers with the same real and imaginary parts are equal. The proof of this depends very much on the implementation — it might be true by definition, it might be true because of a lemma, or actually it might either be true by definition or true because of a lemma depending on the precise definition of how the assertion is phrased in the system. Mathematicians are not so well-placed to deal with these issues. Computer scientists moreover want these hidden little functions which we don’t notice to be fast and efficient, and this introduces some extra layer of run time analysis or whatever which is just a million miles from the mathematician’s model of formal mathematics — our model seems to me to run at infinite speed.

Finally, definitions might need theorems. To define the class group of a number field, it’s not at all hard to make the definition of the underlying set, but proving that it is a group has some content. If the mathematician cannot make the definition because they don’t understand the subtleties of what the programmer needs for the definition to run efficiently, but the computer programmer does not know the proofs of the theorems needed to make the definition, then we are at an impasse. This is one of the situations where the Zulip Lean chat room comes into its own — mathematicians come with questions about how to do things, and computer scientists learn enough about the question to start to be able to interpret it in their own terms and make useful comments about implementation issues. I have seen this happen time and time again.

Of course there is one thing I have forgotten, which mathematicians do: they have ideas and furthermore they reuse ideas which they or others have had. This part is the hardest to formalise. However I think it has something to do with tactics. I have realised that certain quite complex tactics seem to do things which human mathematicians find “trivial”. Lean now has several tactics which do what a “proper mathematician” would describe as “follow your nose”, or “exercise for the reader”. As we go on, and isolate more sophisticated “ideas” or “principles” or whatever they are, will be able to articulate these ideas in our favourite theorem prover? I don’t really see why not. It’s just hard to do right now because so much API and so many definitions are missing in all the provers.

Summary

I think we need to try to do all the maths, in all the computer proof systems. This is a simple way to find out where the weak points of the systems are when it comes to modern mathematics. We don’t have to worry that the proof of FLT is inaccessible. There is so much accessible mathematics to do. But each system has its own quirks when implementing new concepts and definitions. Mathematicians cannot be expected to choose the best implementations of a mathematical concept unless they have been trained by computer scientists. The Lean chat room fulfils a very important role here, helping mathematicians to get definitions right in Lean. The question is far more delicate than a mathematician might think. Which system is best for understanding the statements of modern research mathematics? Nobody knows. This has to change. Let’s find out.

Posted in General | Tagged , , , , , | 2 Comments

My algebraic geometry course

So something stupid happened. I had decided “no Lean” for the algebraic geometry course I’m teaching this term, and then I went to Lean Together 2020 and ended up on the plane back trying to formalise Martin Orr’s notes in Lean and now I’m seriously thinking about going for it and seeing how much we can do. It’s the theory of varieties. At the minute we’re doing affine algebraic varieties over algebraically closed fields. I might back off later if it gets tough, but I am eyeing the Nullstellensatz. They’ve done it in Isabelle. So it could well be possible in Lean 3. Can we state the Nullstellensatz in Lean 4? I saw people using Lean 4 last week. You still have to know what you’re doing, and probably using emacs is your best bet, but it is usable.

You won’t be using Lean 4 unless you’re an expert in this stuff, but here’s a challenge for mathematicians: read this proof. It’s my Lean write-up of lecture 1. That Lean file is 184 lines long, and it proves that the union of two algebraic subsets of k^n is also an algebraic subset of k^n. If you are a mathematician — give it a go. I bet you understand the first half of it. Then it gets technical because a proof starts, but even if you can’t understand the Lean code, I am still explaining in the comments what is going on. I mentioned in my last post how Hales and Koepke are thinking hard about making it easier for human mathematicians to use this kind of software. Until then, you need Rosetta Stones, and this Lean file is an attempt to give one. If you have Lean installed on your computer, then you can clone the repository for the course, run the code on your own computer and see Lean’s tactic state at every point. This makes it much easier to figure out what is going on. It is not always easy. However, it is sometimes easy, especially if you have played the natural number game. Look — there’s zero_mul on line 132. If you don’t know about zero_mul then you could play the natural number game, or try some maths challenges for the Lean curious.

How come everything goes so well up until the proof? Well, notation is a nightmare. Can this be fixed in Lean 4? Why does the goal often look incomprehensible? Why do I have to write mv_polynomial (fin n) k instead of k[X_1,X_2,\ldots,X_n]? Why do I see fin n → k instead of k^n? Why I am I taking intersections over all of the proofs that s\in S? That makes no sense to a mathematician. How can we make this better? It’s just a normal proof presented in a scary way — but I am sure that we can make it less scary with current technology. This is one of the things I hope to work on this term.

Posted in Algebraic Geometry, Imperial, Learning Lean, M4P33, undergrad maths | Tagged , , | 3 Comments

Lean Together 2020

I spent last week in Pittsburgh at Lean Together 2020. I felt privileged to be in the presence of Hales, Koepke and Avigad. These people are watching where Lean is going, and my impression is that they are happy. Massot, Gouëzel and Hölzl were also there, and it was very interesting to see them talking about manifolds (Patrick Massot and Sébastien Gouëzel are research mathematicians, but Johannes Hölzl is a computer scientist who now works for Apple in Munich and is formalising crypto). If someone had told Patrick 5 years ago that he would be going to a conference where (a) he would have technical discussions about the definition of a manifold and (b) give a talk about perfectoid spaces, I am not sure he would have taken them very seriously.

There were loads of great talks, and then of course there were some talks I didn’t understand at all. One person who truly made an impression on me was Ulrik Buchholtz. He taught me a lot about homotopy type theory. What I liked about him was that he had understood that whenever anyone says the word “constructive” I instantly hit the roof and start yelling that I simply do not care and neither do any of my friends, so he barely ever mentioned the concept and as a result I managed to be able to concentrate on what he was trying to tell me. He has a mathematical background, and explained his thoughts about how the univalence axiom is actually a good idea for mathematics. But honestly, first let’s think of new notation for it, because every mathematician knows that equality takes values in an impredicative Prop and that’s the end of it. I was always unhappy that Milne and Grothendieck used equality to denote canonical isomorphism, perhaps we just need a new notation for this kind of equality? Update a few hours later: Actually, on re-reading this post I realise that this is a lie. I thought Milne’s idea of using the equals symbol to denote a canonical isomorphism was a brilliant idea when I was a post-doc. The reason I’ve gone off it now is that I have no idea what a canonical isomorphism is so I can’t formalise the idea properly.

Sebastian Ullrich spoke about Lean 4! Summary: it’s going to be super-cool, notation will rock, and they even have 2 tactics! intro and assumption. I reckon you could prove P\implies P with those, and who knows what else. The elephant in the room: porting mathlib to Lean 4. People were optimistic — but we don’t really know anything.

Hales and Koepke spoke about natural language. They have examples of text which sounds like normal English mathematical text and can be read by their Haskell program and turned into some kind of tree data structure. The task now is to turn that data structure into valid Lean code. I guess Lean 4 will be the thing to target.

Cyril Cohen talked about how to make a big library of data structures (like the theory of groups, rings, fields, totally ordered monoids etc, all at once). He was using Coq but I am sure that we have things to learn from those guys.

Reid Barton raised what looked to me like a straightforward maths question about semialgebraic subsets of \mathbb{R}^n, and then noted that it was super-hard to prove in Lean. He says we need to write a new tactic to prove it.

Neil Strickland raised some very important points in his talk, regarding scalability of the mathlib project. I am pretty sure that several of them still have not been dealt with.

Manuel Eberl showed us all how much better Isabelle is than Lean at analysis, and then Fabien Immler showed us again. Is this because analysis is hard to do in dependent type theory? I don’t think so, because the Coq people are also pretty good at analysis. We are just behind.

Sylvie Boldo gave a wonderful talk about Lebesgue integration in Coq. Sylvie — it was a pleasure to meet you. Sylvie is one of the people behind the Coquelicot project. What can Lean learn from this project?

On Wednesday, we had four talks by people using SMT or SAT solvers in different ways. I was worried that I would find these talks incomprehensible because I really don’t know anything about SAT solvers, but all of them — Lsitsa, Keller, Heule and Ebner — were really enjoyable. Gabriel Ebner unveiled a hammer for Lean! I’m voting Mjölnir by the way.

Mario Carneiro talked about metamath 0. I wish I could say more about his work, but it is too foundational for me to understand it properly. All I know is that we had a proof of Dirichlet’s theorem on primes in an AP in metamath and then Mario pressed a button and we had one in Lean, and it had been written by a computer and was incomprehensible. Scary?

Markus Rabe talked about Google’s dream to build a mathematician. They want to write code that reads ArXiv and spits out some kind of tree data structure. They want to read human language. Hales and Koepke are offering an alternative — they suggest that, right now, humans will have to change (i.e. learn) if they want to communicate mathematics to computers themselves.

Finally, Imperial undergraduates Chris Hughes, Amelia Livingston and Jean Lo did me proud, with intelligent comments and questions.

To everyone I saw there, and in particular to the organisers Jeremy Avigad and Rob Lewis, and also to Mary Grace Joseph, thank you very much for an extremely enjoyable conference.

Posted in General | Tagged , , , , | 1 Comment

Lean has real manifolds!

And tangent bundles too! Thank you Sébastien Gouëzel! Tangent bundles would be hard to do in simple type theory (e.g. Isabelle/HOL) because they are naturally a dependent type, and if you work around this in the way that the HOL people usually do then you seem to have to abandon typeclasses (so sheaves of rings would be hard to work with).

I think that one measure of how appropriate a computer proof system is for human researchers is whether it can state the Clay Millenium problems. If a system isn’t strong enough to even state the problems then surely it is not going to be of much interest to most “working mathematicians”. Which systems can state all of them? None of the systems can. Manifolds are an initial but important step towards the statement of the Hodge Conjecture. Of course we also have to formalise some cohomology theories. I have an MSc student, Shenyang Wu, working on group cohomology, which I always felt was the most concrete and down-to-earth of the cohomology theories which I know.

But before we get too excited, let’s still remember that Lean does not (yet) have the Cauchy Integral Formula…

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

Rigorous mathematics

Lean offers rigour.

For years, people have been pointing me to Thurston’s work “On proof and progress in mathematics”, a work which I think of as a brilliant exposition of the importance of non-formalisation in mathematics. But it was only this week that I actually read the article Thurston was responding to — Jaffe and Quinn’s “Theoretical mathematics”. This paper opened my eyes. They have a word for how I now think about mathematics! They explain that I am now doing something called rigorous mathematics. This phrase gives me the language to explain what I am trying to tell mathematicians.

What is rigorous mathematics? It means mathematics which is guaranteed to be correct. Undergraduate-level mathematics is clearly rigorous mathematics: it has been checked from the axioms by many many people. What else? Perhaps SGA is a good example. It has been around since the 1960s and has been read by many people. The work of Grothendieck and others written up in this seminar was used in Ribet’s work on level-lowering, which was in turn used in Wiles’ proof of Fermat’s Last Theorem. But not all of our human literature is rigorous mathematics. We can basically guarantee that one of the papers published this year in one of the top mathematics journals will, within the next few years, be partially retracted, and nobody is asking the questions about whose job it is then to go through all the papers which cited it and to meticulously check that none of the citations were to parts of the paper which were wrong. I think defining rigorous mathematics in these human terms, trying to assert which parts of the literature are “rigorous”, is a hard problem. Perhaps Bourbaki is rigorous. Patrick Massot found a slip or two in it when formalising parts of Bourbaki’s Topologie Générale in Lean, but nothing remotely serious. Perhaps SGA is rigorous too — after all, hasn’t Brian Conrad read it or something? But actually Bourbaki and SGA both use different foundations, and neither of them use ZFC set theory (Bourbaki rolled its own foundations and then apparently ignored them anyway and just did mathematics, and SGA needs universes in places, but, as Brian Conrad has carefully checked, not in the places used to prove Fermat’s Last Theorem).

I am not sure I know a good answer for exactly which parts of the mathematical corpus as represented by our human literature is “mathematically rigorous”. Maybe the way it works is that anything published in a journal over 20 years ago and which hasn’t been retracted yet is mathematically rigorous. But probably some recently graduated PhD students would also say their work was mathematically rigorous as well. Perhaps the definition most mathematicians work with is that rigorous mathematics is “the part of published mathematics which the elders believe to be correct”.

There is another question too, of less interest to most mathematicians but of some importance when trying to figure out what we mean by rigorous mathematics, and that is the problem of saying exactly what the axioms of mathematics are. Are we allowed universes or not? Whose job is it to tell us? Scholze’s course cites, but does not use, a paper by Barwick and Haine which uses universes everywhere. De Jong puts some effort into explaining how the stacks project can be made to work in ZFC, but honestly who ever reads those bits of the stacks project? Scholze talks about infinity categories in his course and no doubt he can solve all set-theoretic issues — after all he did take the trouble to write section 4 of etale cohomology of diamonds. Emily Riehl and Dominic Verity are writing a book on infinity categories . I bet that book will be rigorous. Wouldn’t it be interesting checking it was rigorous in Lean? I think that this is an important question. Lurie needs infinity categories and his work is having wider implications across mathematics. The Clausen and Scholze work also needs infinity categories and is claiming to prove Grothendieck duality in a completely new way. Is this work definitely rigorous? What about this work of Boxer, Calegari, Gee and Pilloni, announcing some major new results in the Langlands programme but subject to 100 or so missing pages of arguments which are not in the literature but which experts know shouldn’t present any major problems (see the warning in section 1.4 on page 13). I have now seen a citation of that paper in another paper, with no mention of the warning. Is this what rigorous mathematics looks like? I am not suggesting that the work is incorrect, incomplete or anything, and I am not even suggesting that the human race is incapable of making the results in this 285 page paper rigorous. But is it, as it stands, rigorous mathematics? I have my doubts. When David Hansen stands up in the London Number Theory Seminar and claims that a certain construction which takes in a representation of one group and spits out a representation of another one is canonical — and then refuses to be drawn on the definition of canonical — is this rigorous? And if it isn’t, whose job is it to make it rigorous? I am well aware that other people have different opinions on this matter.

I think that every one of the computer proof systems — Isabelle/HOL, UniMath, Coq, Lean, Mizar, MetaMath and all the others, all represent candidate definitions for “rigorous mathematics” which are far better defined than the human “definition”. Which system is best? Who knows. I think mathematicians should learn them all and make their own decisions. I think Lean has got some plus points over some of the others, but I know people who think differently.

Perhaps a more liberal definition would be that rigorous mathematics is the theorems which are proved in the union of these computer proof checkers. So for example we could say that the odd order theorem was rigorously proved from the axioms of maths, as was the four colour theorem, the prime number theorem, the Kepler conjecture and the Cap Set conjecture. These are examples of theorems which I think all mathematicians would agree were rigorously proved. But we will need a lot more machinery before we can rigorously prove Fermat’s Last Theorem in one of these computer systems. In my mind, Fermat’s Last Theorem is currently a theorem of theoretical mathematics in the sense of Jaffe and Quinn, although I have no doubt that one day it will be a theorem of rigorous mathematics as well, because we human mathematicians have written some very clear pseudocode explaining how to make it rigorous. As for the ABC conjecture, I genuinely don’t know if Mochizuki’s ideas can be made into rigorous mathematics, although it seems that in general mathematicians are not happy with the pseudocode which has been produced so far. I can see a very simple way for the Mochizuki-followers to sort this out though, and we would happily talk to them on the Lean chat.

Posted in rigour, Uncategorized | Tagged , , , , , , , , , , , , , , , , , , , , | 10 Comments