The Coq mailing list

[Kevin Buzzard <kevin.m.buzzard AT gmail.com>]

[trying again after subscribing]

---------- Forwarded message ---------
From: Kevin Buzzard <kevin.m.buzzard AT gmail.com>
Date: Thu, 2 Jan 2020 at 20:42
Subject: Re: [Coq-Club] "Lean is like Coq but better"
To: Timothy Carstens <intoverflow AT gmail.com>
Cc: <coq-club AT inria.fr>

Hello Coq people! Bas is right, I did say this, and I guess also that it is too simplistic a statement to be reasonable; clearly Coq is better than Lean at some things, for example it does have a proof of the odd order theorem.

I guess it's clear from the context of the talk though, that I am interested in formalising modern mathematics (and perhaps I should say that this is because I am beginning to distrust the mathematical literature, although I should say that I am *very much* in a minority here; mathematicians have a system, and it basically works, and sure we find errors in the literature, but this is how life has been for a long time and we're used to it now; besides, the important stuff is "probably all fine"). And for formalising modern mathematics I do think that Lean has changed some of Coq's design decisions for the better. I guess the two big things that I would flag if anyone were to ask me why I think Lean is better designed than Coq for modern research mathematics would be:

1) Lean has quotients baked into the kernel. I have talked to several people doing mathematics in Coq who tell me of "setoid hell". In modern fashionable mathematics quotients are everywhere.

2) Lean is designed to work in classical logic, and Coq is more tied to a constructive viewpoint (so I have heard). Probably most of the people on this list have a CS background and you might think that this is a funny issue to be fussy about -- but 99% of modern research mathematicians *do not even know what constructive logic is* and any attempts by computer scientists to justify the importance of constructive logic, perhaps based on the notion that mathematicians somehow want to "compute", will fall on deaf ears. At the top end of mathematics, mathematicians just want to reason. Those that want to compute use unverified (and sometimes closed source) software such as magma, sage, mathematica etc (and furthermore they're not the ones getting the Fields Medals). You might raise concerns about the rigour of our work when we use these systems (and I personally would most definitely share those concerns) but mathematicians in general are not interested in such objections.

Other things:

In Lean I can write proofs in tactic mode or term mode; Lean tactics are written in Lean. I think this gives us more flexibility.

Lean's maths library is currently one big library so there are no issues with incompatibilities of various imports, however this might well be because we are younger.

And finally, Lean's maths library seems to me to be going in the direction of where pure mathematicians want it to go, we are currently building MSc level pure mathematical definitions/theorems across algebra and geometry, and analysis will catch up in the end.

So those are the thoughts that are in my head about the relationship between Lean's type theory and Coq's. Again, I'm sure that Coq will be better at doing some things than Lean, but *speaking as a pure mathematician who wants to reason about complex modern mathematical objects* I have found Lean to be a very good fit.

---

Now I'm here, I may as well say two other things which are also important in this context.

1) It is worth noting that the talk that Bas linked to was a talk I gave at MSR, where Lean is being developed, and it is in my interest to let everyone at MSR know how good Lean is, so that they continue to fund Lean.

2) I am not naive enough to believe that Lean is the one and only correct system in which all mathematics should be formalised. In fact I am far more naive than that ;-) I believe that mathematicians should start to use *all* of the available systems, and in particular I would highlight the following systems: (1) Isabelle/HOL (2) Lean (3) Coq (4) UniMath, or maybe this new Arend system. I believe that mathematicians should become seriously engaged in formalising mathematics in all of these systems because it is clear to all mathematicians that *eventually* these systems will start playing a role in helping modern mathematicians to do modern mathematics, but it has become clear to me over the last two years that the computer science community, unsurprisingly, do not really know the kind of technical stuff which gets you a Fields Medal, and there seems to me to be a huge distance between the kind of mathematics which is being done in most of these systems, and the kind of mathematics which gets the Fields Medal Committee excited. Having learnt something about all of these systems, I think Lean offers the most hope -- but I could be wrong, and furthermore perhaps none of the systems today are appropriate and the moment we start formalising recent work of Scholze we will begin to understand what a modern mathematician needs from a computer proof verification system and then computer scientists will begin to be able to build the system we actually need. All I know is that for sure we need quotients ;-) But we also need a huge algebraic hierarchy and a type class system which will instantly know that a totally ordered field is an additive group or that if R->S is a ring homomorphism then any S-module is naturally an R-module. Lean 3's type class system has been absolutely pushed to the limits by MSc level commutative algebra and it is because mathematicians have been attempting to do MSc level commutative algebra in Lean, and complaining on the Lean chat when things get slow, that the type class system has been completely redesigned in Lean 4. If I have achieved one thing in this area then I could argue that it was that I was part of a group of people who pushed what Lean 3 could do to the limit and uncovered the fact that things need to be re-thought if one wants to do fashionable modern mathematics in Lean. Lean 3 has canonical structures like Coq, but they will be removed in Lean 4. We have decided to do things another way and I am not computer-sciency enough to be able to explain it to you guys but believe you me, if you want to know what Lean will do instead of canonical structures, and why some people think it's a better idea, you would be more than welcome to ask your questions in the Lean chat at https://leanprover.zulipchat.com/  (real names preferred, login required, be nice). It is a very welcoming community and I myself (and also Patrick Massot, another mathematician) sometimes wish there were more Coq users there, because sometimes we get the impression that the Lean people are solving problems that you Coq people have solved already.

I do not have the time to learn another system, but in my opinion one of the most exciting things that could happen would be if more people like me, with a classical mathematics background, start to teach mathematics undergraduates *all* of these systems. I am well aware that they are taught in many computer science departments and furthermore I know from personal experience that it is not easy integrating them into mathematics courses, because there are some things which a mathematician says are trivial and which a Coq user would agree, but there are other things which a mathematician says are trivial because the proof is "just draw a picture", and because this is apparently not rigorous enough for these computer systems, mathematicians now have to know how to find the formal proof in a library, which can be hard. I think that this can put off potential mathematician teachers.

The thing I have in some sense found most depressing about moving to this area (which again, let me emphasize, I think is surely the future of pure mathematics) is that some of these systems have been around for *decades* and yet they are still not being used in mathematics departments. I still genuinely remember being *stunned* when I defined a scheme in Lean (a fundamental construction due to Grothendieck from 1960) and then learnt that these objects had not been formalised in any of the other systems. In particular the fact that they have not been formalised in UniMath, a system which was in some sense designed by an algebraic geometer, makes me extremely suspicious about how appropriate HoTT is for doing mathematics. However I would love to be proved wrong about this.

I know that there are big ERC grants and other grants held in computer science departments whose aims are to do mathematics in these systems (for various values of "mathematics") but I still do not see them breaking through into the mainstream mathematical culture. Sure I see category theorists and type theorists and constructivists, some of whom might be employed in maths departments, using this software, but unfortunately this is not modern mainstream fashionable mathematics right now. It's the people I know who work in the p-adic Langlands philosophy -- those are the people I want to reach, and it will take a long time. I think that these systems need documentation for mathematicians, which concentrates on proving mathematical lemmas in e.g. group theory or ring theory, rather than tricky exercises about reversing lists twice. I think this software gamifies mathematics, and I think there is a huge crowd of young mathematicians out there who would love to be solving their example sheet questions using a theorem prover; once using this sort of software has been normalised by the young then I think the paradigm shift is inevitable. But I have only got one pair of hands.

I have said a lot, and perhaps I have said things which upset some people, but I am just saying what I honestly believe and at the end of the day I am really looking forward to the time when some people in my department are telling the students to solve their problem sheets in Coq/IsabelleHOL/UniMath just like I tell my students to work on the problem sheets in Lean. But it is hard making things change, even though it is clearly something which is destined to happen. I just want to make it happen more quickly so I am going around being noisy and saying sometimes-stupid things and just generally trying to raise the profile of software like yours amongst my people.

Kevin

On Thu, 2 Jan 2020 at 19:41, Timothy Carstens <intoverflow AT gmail.com> wrote:

I'm not Kevin, but it's a public thread, so -

My experience with Lean+Coq has been that they suffer from many of the same challenges, but in different ways

* Universes. Either you're gonna have explicit lifting (Lean) or you're gonna have a cumulative checker (Coq). One is tedious to use, the other is relatively complex under the hood.

* DLL Hell. Lean and Coq both have a hard time building a big collection of user-contributed libs, since minor changes to the engines break old code. I'm not a maintainer for either system but it seems like both engines rely on these really sensitive inference algorithms. Minor tweaks to these algo's just completely wrecks backwards compatibility for tactic-mode proofs.

* Tactic mode. Arguably this should be a rich programming environment with useful abstractions. Right now you can get that if you're willing to write a Coq plugin, but that's kinda heavy-handed, and it's certainly a highly-coupled (hard to maintain) way to go. Lean has a goal of offering a richer environment for tactics. IMHO everyone will eventually need to go in this direction.

* Few user libs, and even fewer that actually build on each other. This is a bad sign for both environments - healthy software ecosystems have towering stacks of libs and tools with meaningful dependencies.

* Performance. If you set out to write a high-perf pCIC checker, and you're an extremely experienced software engineer, you'll probably succeed. 3 years ago I'd say this was Lean's greatest strength, but in recent years Coq has gotten waaaaay faster, so maybe this isn't as relevant as it once was.

* Language server. Last I checked, both had an ad-hoc approach to this.

Coq has improved vastly in each of these areas in my ~7 years of working with it. There's still more work to be done, but not so-much that I'd advocate for completely starting over.

From the outside, it looks to me like Lean won't be "ready" until it has solved all of those issues to the team's satisfaction. Thus, every year or so they throw away their old code base and start from scratch, including how to organize things like the standard library (really fam, could we just do a good job with it and stop moving the chairs around??)

Anyway, that's my 2 cents ;)

Happy New Years! Wishing everyone deep insights and clever proofs,

-t

On Thu, Jan 2, 2020 at 9:36 AM Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

Dear Kevin,

You claimed
"Lean is like Coq but better"
https://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf

There was a bit of discussion among coq users about what this means.
Did you have any concrete suggestions on how lean is better, and how
Coq could be improved?

While I'm at it, let me announce this workshop next week to the coq-community:
https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/

Best regards,

Bas