coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq)

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq)
Date: Sun, 11 Oct 2020 16:15:57 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f173.google.com
Ironport-phdr: 9a23:RscmER2Y//q0qNz1smDT+DRfVm0co7zxezQtwd8ZsesWKPnxwZ3uMQTl6Ol3ixeRBMOHsq0C1red6vy/EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oLBi7rQrdutQZjIZgN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhTwZPDAl7m7Yls1wjLpaoB2/oRx/35XUa5yROPZnY6/RYc8WSW9HU81MVSJOH5m8YpMBAeQBI+hWsorzqFkArRW5CgajGOzhxyRUhn/vx6A2z/4sHR3E0QEmAtkAsG7UrNLwNKoKX+y1zq7IzTPCb/NVxzj97JbHfQ46rPGDWLJ/a8vRyU01GwzZiVWQrILpNC6S2+QPtGib6etgVeGxhG4jtQ5+vCOixsgpiobTh4IVzkrI+jl+wIYwPNC1TlNwbtG4HpVKrS6aK5d2Td04Q2FuoCs3y7wLt5GlcSUUzJkq2xrSZv+HfYWI4h/uSeScLCpkiXxrdr+xiRi8/Euhx+D4WMe5zlZEozZHn9TCqn0AygLf586aQfVz+Ueh3CyA1wHV6uxcOEA0iLDUK5g9wrEqk5ocq0vDETX3mUX3iq+ZaF8o+u+y6+ToZLjtu5ySN5dshw3gLqgjntazDOc4PwQUQmSW+Piw2Kf+8UD7TrhGluM6n6jFvJzHIMkXu6q0DBNQ34ss6huzEyuq3dEWkHYZLF9IfRyKg5T0N17VJf31D+qwg1qikDpuyfDJIKbuDYnII3XNkbruYbhw5khBwwQp199f/YhbCrQZLfLzREDxsNvYAwc8MwOuwubnDMxx1poCWW6SG6OZPr7evF2G6+41LOmMY4gVuDn5K/c7/fLhkXg5mVoFcamo25sYdmy4E+x4L0mFZXfgmNQMHGcQsgYjTeHmlEeOXSNRanu8R6484ys0CIOiDYfNXICth7mB0T+5Hp1RYGBGC1OMHmnsd4qaRfgBcy2SIsp7nTwFUbitUZMu1RartAPi0bpoMvLU+jEEtZLkzNV6++rTlQgr+TNoC8SdznqCQnpvnmIIQj82xLpwrVZ8yleFy6h4guZXGcZd5/NTAU8GMsvzxm9mAta6dQPFdNqTVB7yTdyrHTg3CN0wx9UDeVpVANazlRPC2i+nGfkTmqDdV7Iu9aeJlXr2Icd+xnLL2YEuilAnRo1EMmjszvp98A7SBIPNnkixmKOjdKBa1ynIojTQhVGStV1VBVYjGZ7OWmoSMw6P9YygtxHyCoS2ALFiCTNvjMuLK69EcNrs1AwUS/LqOdCYaGW0yT7pWUS4g4iUZY+vQF0zmT3HARFdwQ8W9HeCcwM5A3X5+j+MPHlVDVvqJnjU36x+pXe8FBFmygiLawh4y+Pw9EdK3rqTTPQc2r9CsyAk+W15

On Sun, 11 Oct 2020 20:46:51 +0200
Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

> see zulip

So that's where the party's at. I've been hanging out in the wrong bar.

>
> Gaëtan Gilbert
>
> On 11/10/2020 19:44, jonikelee AT gmail.com wrote:
> > https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/
> >
> > About Coq, it says:
> >
> > Coq users have formalized a lot of mathematics in its language, but
> > that work has been decentralized and unorganized. Mathematicians
> > worked on projects that interested them and only defined the
> > mathematical objects needed to carry their projects out, often
> > describing those objects in unique ways. As a result, the Coq
> > libraries feel jumbled, like an unplanned city.
> >
> > “Coq is an old man now, and it has a lot of scars,” said Mahboubi,
> > who has worked with the program extensively. “It’s been
> > collaboratively maintained by many people over time, and it has
> > known defects due to its long history.”
> >

[Coq-Club] Quanta magazine article on Lean (with mentions of Coq), jonikelee AT gmail.com, 10/11/2020
- Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), Gaëtan Gilbert, 10/11/2020
  - Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), jonikelee AT gmail.com, 10/11/2020
    - Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), Gabriel Scherer, 10/12/2020
      - Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), Hugo Herbelin, 10/12/2020