coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bas Spitters <b.a.w.spitters AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>, Kevin Buzzard <kevin.m.buzzard AT gmail.com>, coq+miscellaneous AT discoursemail.com, lean-user <lean-user AT googlegroups.com>
- Subject: Re: [Coq-Club] Coq vs lean for classical analysis
- Date: Sun, 23 Feb 2020 17:36:03 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-yb1-f175.google.com
- Ironport-phdr: 9a23:dG8hPx+4V7PYyv9uRHKM819IXTAuvvDOBiVQ1KB+0u8eIJqq85mqBkHD//Il1AaPAdyHraIUwLqG+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCeybL9oLxi7rgrdu8oVjIB/Nqs/1xzFr2dHdOhR2W5mP0+YkQzm5se38p5j8iBQtOwk+sVdT6j0fLk2QKJBAjg+PG87+MPktR/YTQuS/XQcSXkZkgBJAwfe8h73WIr6vzbguep83CmaOtD2TawxVD+/4apnVAPkhSEaPDMi7mrZltJ/g75aoBK5phxw3YjUYJ2ONPFjeq/RZM4WSXZdUspUUSFOBZ6yb5YUD+oZI+lXs5X9qVUJrRu7HwasBeXvwSJMinL52aA21uIsGhzE0gM9BdIDqHvbrNv3O6kSX+67z7TGwyvfYP5NxTfx9JLFfgw9rf2QX799d9fax0k1FwPCi1WdsZHoMCmO1u8Qrmab9+tgVf6zi2E5sQFxuSWky8A3hYXTnI0Z0F7F+T9iwIYtJN24VFJ7bsC+EJtLrCyaOI52TdkjQ2Fsoio11roGuZuicSUM1Z8pyRnfa/mdfIiJ5BLuTOmRITZkhHJlZbKwnAy+8UmnyuHkSsa00ExFri5AktbSrHANzAbf6tOZRfdl+EeuxziO1xzU6uFCO0w7j7bUJ4Q8wr4zjpYTsF7MHjTslErokaCWa10o+vWu6+TmfLXqv4ecOJVuigH/KaQig9GwAeUlPQcQRWib/vi82Kft/U3jWLlKgfw2krXZsJDHPssXvLK2AwhQ0oo79xa+ATam0MgEnXYZNlJJYg6Ij4/sO13WIfD4C+2/g1W2nztxyfDGJLvsCYjOIHjbiLrtY6px5kpGxAcwzd1T/YxYBqwFLf7pR0P8ttzVAxkkOAKu2ennEs9y1oYGVGKPHKCZNKTSvEeN5u01IumMYJYZuTbmJPQ4/vLug2I1lF0dcKWz0psXb3e4HvtiI0qHe3bjntABEWISsgo/SuzllkGCXCZNa3quW68w/DI2BYK8AYvdW4yghKaN0Dq5E5BWfmxGD0qDEXbsd4WKQfcMbyeSL9d6nTAeT7etUYEg2Qu1tA/iyrpnMvbU9TMCtZL4z9V16OjTmgsz9TxwFciSz2aNT2RskmMSWzA2xLx/oVB6ylqbzad4hOVYGcVP6PNNTwc1LoXRz/d6CtD3QgLOZM2FSFegQtW8ADE+VMg9w9EUYxU1J9L3pRfalwGuHrVdw7eMHdk/9r/W93n3Pcd0jXjcgu1prFQ4Q80HH3C0lKdl+0CHBIPXkkPfkuCgaLYO1TTB3GiGxGuK+kpfVVg0Ga7CRDMaZ1DdoND970XPSKK1IbgmKQBG1NSZJ65Da9mvhlJDAL/nNd3YJn+qln34URKFz7XJcZHnYU0S2yLSDEULiQcO5W3APg87UHSPuWXbWRZnDhrUe0Lw7eRkszvvRAk9iR7MdFVgy6a44AU9ivmVSvdV1bUB7nRy4w5oFUqwioqFQ+GLoBBsKeABOIpssmcC7nrQsklGBrLlKqljglAEdAEu5hHh0hx2DsNLls149Sp2njo3ErqR1RZ6Tx3dxYr5Y+SFJWz7/RTpYKnTiAmHjYSmv5wX4fF9kG3N+QGkEk14rSdi2thRlmqWv9DEVVVPF532VUkz+l5xoLSIOiQ=
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.spitters AT 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
- Re: [Coq-Club] Coq vs lean for classical analysis, Bas Spitters, 02/23/2020
Archive powered by MHonArc 2.6.18.