The Coq mailing list

[Xuanrui Qi <xuanrui AT nagoya-u.jp>]

On a side note, I thought it was the case that in commutative algebra
there is at least some awareness of constructive methods. I am by no
means a working algebraist, though, so I might be mistaken.

-Xuanrui

On Mon, 2020-01-06 at 22:36 +0100, Bas Spitters wrote:
> 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