The Coq mailing list

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

Yes, Diaconescu is formalised in the Lean standard library and this is how excluded middle is proved in Lean: https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html#the-law-of-the-excluded-middle

While I'm here let me respond to something Thorsten said:

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

It is certainly true, and I would also argue that the law of the excluded middle is completely embedded in "Fields Medal mathematics". The bright young mathematicians look up to the Fields Medallists, and are taught on day one that Prop = bool and hence that the law of the excluded middle is an axiom. This will be an extremely hard cycle to break. I agree that young people are more and more coming into mathematics departments with a knowledge of programming and this is what I want to tap into, but rejecting LEM would not be a suggestion which would be taken seriously by anybody in our department. In fact I do not know of a mathematics department anywhere in the world where undergraduates are not told that LEM is true right from the start, and most lecturers. It would be interesting to find examples of International Mathematical Olympiad questions which would be unsolvable without LEM. 

Kevin

On Mon, 6 Jan 2020 at 09:40, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

Thanks for the summary.

Do I understand correctly that the formulation of lean's choice
implies excluded middle (by Diaconescu) ?

About ad-hoc polymorphism: it has been done in coq in two ways:
canonical structures (Gonthier, Ziliani, Nanevski, Dreyer, How to make
ad hoc proof automation less ad hoc,
https://people.mpi-sws.org/~beta/lessadhoc/)
type classes (Bas Spitters and Eelis van der Weegen, Type Classes for
Mathematics in Type Theory,
http://dx.doi.org/10.1017/S0960129511000119)

On Sat, Jan 4, 2020 at 6:43 AM Ramkumar Ramachandra <artagnon AT gmail.com> wrote:
>
> Lean has much lower startup-cost for pure mathematicians, since the built-in features and mathlib are great for doing undergraduate-level group theory & topology, masters-level commutative algebra & category theory, but I think it plateaus quickly thereafter; future releases of Lean will probably fix this.
>
> Lean seems to have taken a top-down approach, by focusing on writing real proofs as quickly as possible, without compromising soundness [https://github.com/digama0/lean-type-theory/releases/tag/v1.0]. There are three axioms in Lean: propositional extensionality, quotient soundness, and choice; however, these don’t block computation, since computation is done by a VM. However, they break good type theoretic properties like strong normalization, subject reduction, and canonicity — this was a conscious design choice, and they decided that these properties weren’t as important to working mathematicians.
>
> Coq, on the other hand, has always been very particular about sound type theoretic foundations. The recent “Coq Coq Correct!” paper [https://www.irif.fr/~sozeau/research/publications/drafts/Coq_Coq_Correct.pdf] proves various metatheoretic properties of the Coq engine.
>
> Lean supports both constructive and classical reasoning, but I’m hoping HoTT will be integrated into mainline Coq and solve most of the setoid-related issues (not that I understand much about it).
>
> One would think that Lean is an engineering feat, since it’s written in C++ (and lean4 is written mostly in C): math-comp is 90k loc, while mathlib is 150k loc; and it takes over thirty minutes to build mathlib! Coq is much faster.
>
> Quotients are indeed a great feature to have, and makes formalizing commutative algebra painless; an example [https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/Zmod37.lean] of using quotients in Lean. However, quotients are tricky to implement without breaking certain metatheoretic properties that Coq’ers cherish, which is why it hasn’t been implemented yet.
>
> Lean’s inheritance [https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html#inheritance] is another good feature; it disallows diamond-inheritance, and seems like a bit of a hack, but Coq should definitely get some form of a well-thought-out ad-hoc polymorphism.
>
> Category theory in Lean has not been developed [https://github.com/leanprover-community/mathlib/blob/master/docs/theories/category_theory.md] with higher categories in mind; I’m not sure how one would define ∞-categories, since universes are explicit, and since there are no coinductive types: Coq’s impredicativity seems to be a better design choice.
>
> Footnote. Metamath Zero [https://github.com/digama0/mm0] might be of interest to the Coq community for high-performance checking.
>
> Ram