Kevin Buzzard's intervention: Where is the fashionable mathematics? (Lean etc.)

[Ken Kubota]

My comment on Kevin Buzzard's intervention:

https://groups.google.com/d/msg/metamath/Fgn0qZEzCko/bvVem1BZCQAJ

Link list of the discussion threads:

https://owlofminerva.net/kubota/update-to-the-foundations-of-mathematics/

____________________________________________________

Ken Kubota

http://doi.org/10.4444/100

Anfang der weitergeleiteten Nachricht:

Von: Bas Spitters <b.a.w.s...@gmail.com>

Betreff: Aw: [Coq-Club] Coq vs lean for classical analysis

Datum: 23. Februar 2020 um 17:36:03 MEZ

An: Coq Club <coq-...@inria.fr>, Kevin Buzzard <kevin.m...@gmail.com>, coq+misc...@discoursemail.com, lean-user <lean...@googlegroups.com>

Antwort an: coq-...@inria.fr

With the discussion flaring up again, let me try to copy it to
discourse (using the email address above).

Regarding, what have people been doing to reach mathematicians. Let me
mention a few initiatives:
https://mapcommunity.github.io/
https://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath
Newton Institute:
https://www.newton.ac.uk/event/bpr
IAS:
https://www.math.ias.edu/sp/univalent
IHP:
https://ihp2014.pps.univ-paris-diderot.fr/doku.php
https://github.com/UniMath/SymmetryBook

Moreover, I believe Egbert Rijke has a point:"
- Our communities are simply too small
- Our papers don't get published unless they're about new stuff. "The
definition of a scheme in Coq" doesn't get favorable reviews.
- We *do* some fashonable maths: higher topos theory, higher group
theory, some big theorems..."
https://twitter.com/EgbertRijke/status/1226948002654380033?s=20

On Thu, Jan 9, 2020 at 7:02 AM Bas Spitters <b.a.w.s...@gmail.com> wrote:

Dear Kevin,

Thank you for your clarifications.
Let me try to see if I understand, you seem to be saying that lean
would have little advantages over coq for discrete mathematics such as
used in the Feit-Thompson theorem. In particular, the automation of
lean is not much stronger than that of Coq.

However, for classical real analysis you seem to be saying that native
quotients and choice have a big advantage. Here it is possible to make
a good comparison between the coq stdlib reals, coquelicot and
math-comp analysis on the one side and lean's math-lib on the other
side.
Could you explain how native choice/PEM is much preferable over a
choice *axiom* as is used in e.g. math-comp analysis.
https://github.com/math-comp/analysis
http://coquelicot.saclay.inria.fr/

Obvious differences with math-comp analysis are:
IIUC lean has dropped canonical structures and has a type class system
that is slightly different from Coq's. Moreover, lean's proof language
is more verbose than Coq's Ltac and in particular SSR.

Best wishes,

Bas