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 <http://doi.org/10.4444/100> > Anfang der weitergeleiteten Nachricht: > > Von: Bas Spitters <[email protected]> > Betreff: Aw: [Coq-Club] Coq vs lean for classical analysis > Datum: 23. Februar 2020 um 17:36:03 MEZ > An: Coq Club <[email protected]>, Kevin Buzzard <[email protected]>, > [email protected], lean-user <[email protected]> > Antwort an: [email protected] > > 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 <[email protected]> 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 -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/25ED45D7-CE88-4B08-BB93-EDD928D0E3AF%40kenkubota.de.
