The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Let me just quote John Baez today:
"I think of topos theory as being fashionable again, now that famous
mathematicians like Connes and Lafforgue who we don't think of as
category theorists are trying to use topos theory to tackle big
problems in number theory etc."
https://twitter.com/johncarlosbaez/status/1214225792307060736

Of course, synthetic mathematics is just one application of
constructive logic, the computational aspect is another one.

On Mon, Jan 6, 2020 at 9:58 PM Kevin Buzzard 
<kevin.m.buzzard AT gmail.com>
 wrote:
>
> 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