kevinbuzzard

The problem with metamath is that you basically have to be a fully signed-up masochist in order to do anything nontrivial with it. People have certainly done nontrivial things with it e.g Carneiro and the prime number theorem -- but it takes all sorts. If I want to prove (a+b)(a+2b)(a+3b)= a^3 + 6ba^2 + 11b^2a + 6b^3 in Lean I just type `ring`. Good luck proving that from the axioms of a ring directly in metamath, I challenge you to do it in fewer than 30 moves. I should also say that whilst Metamath has certainly formalised a whole bunch of mathematics, it has not remotely gone "a long way" by any reasonable measure which a mathematician would use. For example, how much of an undergraduate mathematics curriculum does it have? How much representation theory? None. How much differential geometry? None. How much commutative algebra? Epsilon. These are the measures which mathematicians use, not lines of code. It is time that formalisation started to appeal to mathematicians, and for this to happen it is essential that it starts to demonstrate that it can actually do a lot of the kind of mathematics which is recognised as "completely standard undergraduate material and hence trivial" by mathematicians. It is still the case that these systems cannot do certain things which were known to Gauss or Euler (for example it was only this year that Lean learnt the proof that the class group of an imaginary quadratic field was finite, and as far as I know no other system at all has class groups -- but we teach this to the undergraduates!). Just saying "large code base therefore we've gone a long way" is not the correct logic. The question is how much of it is recognisable as worth teaching to undergraduates in 2021, and conversely how much stuff worth teaching to undergraduates in 2021 is _not_ in any of these systems. That's where the problems begin to show up. In Lean we are well into a project of formalising an entire undergraduate curriculum and within about two years we will have finished.

Hi! Yes! Just pick a different one! The problem is that constructivists have been formalising mathematics for decades and have not really managed to break through into the mainstream mathematical community with their efforts. The difference with Lean's maths library is that we absolutely reject constructivism, which makes Lean far less suitable for certain kinds of computations but conversely far far better equipped for proving all the theorems in an undergraduate mathematics curriculum and then going on to tackle research level mathematical questions of the kind which most mathematicians recognise as "normal mathematics". My argument (I should say that I am the author of the blog post) is that this resolutely non-classical approach is far more likely to arouse the interest of mainstream mathematicians, who rejected constructivism 100 years ago and have never looked back. I can certainly see a role for constructive mathematics, however I know from experience that most working mathematicians reject it and hence the pragmatic approach is to reject it when formalising if we are to start appealing to the mathematical masses.

Yes, this is very old. This is a review of Lean 3; Lean 4 is about to appear and this deals with several of the issues flagged by Hales, for example speed.

blah blah blah type checkers blah blah blah can be run on different chipsets / OS's blah blah blah computers are several orders of magnitude more accurate blah blah blah not really the issue.

[just to be clear here, I am the author of the Xena project blog and my current research is in formalising number theory; before formalisation I was working in Scholze's area.]

Scholze's first application of the theory of perfectoid spaces was to prove weight-monodromy in many new cases (but not in all cases) -- this was his first breakthrough result really. Fun fact: in the first version of the post which he sent me, this weight-monodromy confession was not there. He then slept on it and sent a second version a day later, and it was only when I was converting the LaTeX into Wordpress format that I noticed that he had added this extra line. I quite agree that it is very rare for people, especially of his stature, to publically admit to errors, especially ones which never made it into print. Of course we will be working on this challenge in Lean, and we are currently optimistic, but who knows. It is certainly true that in the study group we had on the work at Imperial earlier this year, we did not work through the technical proof which Scholze is now challenging the formalization community to check. This is really Scholze's point I guess: once you have a Fields Medal it's very easy for other people to say "well this is a bit technical but let's face it, it's probably fine" (this is exactly what we did, for example). Voevodsky made similar comments around a decade ago -- and he managed to get false arguments published, perhaps partly because of his own Fields Medal. Scholze is flagging an explicit argument in his work which he believes needs to be carefully analysed, and I have seen with my own eyes that the academic system we have right now might not actually do it carefully enough. What is not at all clear, right now at least, is whether computer proof verification systems are up to the task. I think it will be interesting to see how this develops.

I seem to be associated with that quote (and of course I didn't say it -- indeed when I spoke to Quanta I used factorials plus one). When the article appeared I emailed Kevin Hartnett immediately to suggest replacing that line with something like "...using 1 plus the product of all known primes" but he seemed to be happy with what he'd written -- his argument was that what he wrote was ambiguous but not definitely wrong.

(disclaimer: I'm the author of the blog post). The argument the other way is that if a mathematician sees this convention, their reaction is likely to be "that's just silly, 1/0 is obviously 'halt and catch fire'", and any attempt to defend this by saying "it makes perfect sense viewed through the lens of type theory" runs the risk of the response "well I won't be doing my mathematics in type theory then". In the comments to the blog post (and in personal emails) people have suggested that instead of trying to defend the idea that 1/0=0 (which is what I was trying to do, given that I am now very much used to it) I should instead be complaining to the Lean designers to make the front end "work more like a mathematician expects". However this is difficult, because talking to mathematicians it becomes clear that they have different opinions about what "actually happens" when you put garbage in.

I totally agree that it's all over the place. I am a mathematician and have just thrown this together because I wanted my students to be able to learn Peano arithmetic (something I teach in my course) in a fun way. I am in desperate need of someone who knows something about UX.

I used Patrick Massot's Lean Formatter https://github.com/leanprover-community/format_lean to make the Lean web page with the analysis theorem on, and Mohammad Pedramfar's Lean game maker was very much inspired by the code in the formatter.

First let me point out that you can jump to any level at any time, so you lose your progress, but only in a weak sense, if you lose your browser tab. You do lose your proofs though.

The natural number game was made by passing a repository which contains essentially nothing but Lean code, through this generic tool https://github.com/mpedramfar/Lean-game-maker which makes the html pages from the Lean code. If there is anyone out there who understands the Lean game maker code (I don't, it was written by my co-author) and is interested in implementing some kind of client side storage then feel free to ping me either at my Imperial email address or at the Lean Zulip chat https://leanprover.zulipchat.com .

Automation of epsilon-delta proofs is in its infancy. Currently with an interactive theorem prover like Lean, you type in the proof yourself, so it's pretty much exactly the same as doing it on paper, except that you can't make a mistake. For example here is a website giving a proof of the squeeze theorem

http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html

and if you click on a line in the proof, and then on a little grey rectangle, you will see the state of Lean's brain at that point in the proof. But the proof is just the normal proof and a student writing the proof in Lean has to just write the normal proof, but in Lean's language rather than in mathematical English.

Lean's maths library development is essentially completely focussed on classical mathematics, which is why it has been so successful in drawing "working mathematicians" in. Such people do not care at all about the issues involving quotients, indeed quotients in Lean work just fine for them, and they don't care about constructibility either, because this is the prevailing culture in maths departments (although it is not, I am well aware, the prevailing culture in computer science departments). If you are interested in constructivism I would not recommend Lean. Many of the developments in mathlib are classical. That's why it's moving so quickly -- classical mathematics is much easier.

There is a huge amount of evidence of mathematics undergraduates using interactive provers, which they weren't doing before. There are very few profs using any interactive prover, because currently these things offer nothing useful to a prof. However, if more and more undergraduates adopt software like this, or at least try it and realise that it's not scary, then within ten years there will be profs using it. We're playing the long game. We need to make tools for the profs, like automation that can check tedious lemmas, or a database of theorem statements which is searchable by a mathematician who doesn't know how to use the software. These are some of the goals Tom Hales is targetting with his FABSTRACTS project. But it will take time. All I know is that the software is now ready to do modern mathematics.

Contains a section on the rational and real numbers. Mathematicians might want to start at section 11.5.

[Here](https://arxiv.org/abs/1907.01449) is a Lean formalisation of a 2017 Annals of Mathematics paper.

I was being intentionally provocative. On the other hand I feel like there are plenty of people in my (mathematics) department who would say that "normal" fields like geometry, topology, algebra, number theory and analysis are where the action is happening, and category theory is just a tool which we use to get "normal" maths done. On the other hand now Scholze is beginning to use infinity categories more in his work, this might change -- but it might not. Maybe in 10 years time there will be a book "infinity categories for the working mathematician" which we all read the first ten pages of and this is all that most of us need. Note that category theorists like Hyland and Johnstone have retired from Cambridge now and have not been replaced -- in the UK now you are more likely to find a category theorist working in a computer science department than a mathematics department. Whether or not it is "real mathematics", it is certainly a fact that in the UK at least it is an extremely small community, whereas our departments are full of number theorists, geometers, topologists, analysts and algebraists all of whom need to know essentially no category theory beyond the basic language of adjoint and representable functors.