The Coq mailing list

[Thorsten Altenkirch <t.altenkirch AT googlemail.com>]

I realize that this discussion is about pragmatic aspects of proof assistants but I would like to use the opportunity to say something about foundational aspects where both Coq and Lean fail badly. There is the slogan nothing is as practical as a good theory and I would add a good theory is based on solid foundations.

Both Coq and Lean fail in properly supporting structures with a non-trivial equality. Lean doesn’t really offer an answer to setoid hell but just adds quotients as an axiomatic principle with no computational explanation. This is despite us knowing since a while (I wrote a paper on this in ’99) how to turn setoid hell into setoid heaven by working within the setoid model: that is if you want to talk about setoids all the time just accept that every type comes with its own eqaulity and build your type theory around this. 

But going further: setoids only support types with a propositional equality. We know that this is wrong, it is an unfortunate legacy of set theory formulated within the framework of predicate logic. It is wrong because equality of structures is a structure not a proposition. I recently attended a talk by Kevin in Nottingham where he exactly stumbled into this issue, trying to implement a construction by Grothendieck. It seems that Grothendieck had the right intuition but it doesn’t fit into the framework of set-theory inspired type theory. Now, if I remember correctly, Kevin and his students found ingenious solutions but never questioned the dogma that equality needs to be propositional! The particular irony is that they weren’t even working in set theory but in a type theory which had been designed artificially in a way that makes it hard or impossible to have a proof-relevant equality. And this is indeed one of the gifts Type Theory has to give to structural Mathematics! In this respect Lean is worse than Coq because it is explicitly anti-structural.

Now let me get to the point that most Mathematicians are not aware of constructive Mathematics. This may well be true but does this mean that they are right and that constructive Mathematics is irrelevant for Mathematics? This seems rather a sociologically issue than anything else. And fashions can change faster than you think especially once a new generation of Mathematicians take over who are not only influenced by the older Mathematicians but who are often also excellent programmers acquiring new intuitions. To not educate them as well in constructive Mathematics reflecting these intuitions is a criminal omission.

I don’t suggest that Mathematicians should immediately throw out all classical principles and adopt constructive Mathematics but they should be aware of both. Often a classical construction is like a rough sketch , a motivation for looking for a finer picture which can be expressed in a constructive setting. Instead of digging always deeper into higher levels of abstraction and generality, it can be very worthwhile to look at Mathematics form this perspective.

As an added benefit, intuitionistc Mathematics does have a philosophical foundation that classical Mathematics lacks. I know Mathematicians usually leave the room when the word “philosophy” is said but maybe they shouldn’t (always). What is a proposition? A very basic question. It is either true or false, that is Prop=Bool? I never understood this, if I have an infinite family of booleans who do I obtain one boolean which express that they are never false? Ah, I don’t obtain it it is just the case? What does this mean? Ah in the real world this is the case? But we are talking about Mathematical constructions – what do they have to do with the “real world”? Ah the world of ideas is like the real world? Does anybody seriously believe this (apart from Plato)? Anyway there is a nice way out of this dilemma: a proposition is something you can have evidence for. This is the intuitionistic explanation of propositions and it works perfectly fine. We can even justify the principle of excluded middle via the negative translation but we cannot save all instances of the axiom of choice. Maybe this tells you something.

What is my conclusion: yes today we should work with the proof assistants available and I am quite impressed with Kevin’s work and the way he uses Lean in his teaching (I recommend to everybody to ave a look at his number world on the web). But this shouldn’t stop us looking for tomorrow, for the proof assistants of the future. In the moment it seems to me that cubical agda is the one who comes closest to this vision from my point of vie. But yes, we need to combine the practical with the foundational. I view the formalisation of Mathematics which is going to happen one way or another as an opportunity also to develop mathematical foundations further. It would be such a shame if we use the tools of tomorrow to implement the Mathematics of yesterday!

From: <coq-club-request AT inria.fr> on behalf of Kevin Buzzard <kevin.m.buzzard AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Thursday, 2 January 2020 at 20:59
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Fwd: "Lean is like Coq but better"

[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.

rest omitted due to some strange space restrictions