Skip to Content.
Sympa Menu

coq-club - [Coq-Club] December 2020 AMS Notice by Kevin Buzzard

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] December 2020 AMS Notice by Kevin Buzzard


Chronological Thread 
  • From: Talia Ringer <tringer AT cs.washington.edu>
  • To: Coq-Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] December 2020 AMS Notice by Kevin Buzzard
  • Date: Sun, 29 Nov 2020 12:56:37 -0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=Pass smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-ej1-f51.google.com
  • Ironport-phdr: 9a23:0tAtFhRnUxSQ4DGinwqoz2CG59psv+yvbD5Q0YIujvd0So/mwa6ybBON2/xhgRfzUJnB7Loc0qyK6v+mADFQqs/a4DgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrrwjdrNQajIthJ6o+1xfErHhFcPlKyG11Il6egwzy7dqq8p559CRQtfMh98peXqj/Yq81U79WAik4Pm4s/MHkugXNQgWJ5nsHT2UZiQFIDBTf7BH7RZj+rC33vfdg1SaAPM32Sbc0WSm+76puVRTlhjsLOyI//WrKjcN9kLxXrRGhqhBm34LZYpyeOP5xc67ZeN8XQ3dKUMRMWCxbGo6zYIsBAeQCM+hFsYfyu0ADogGiCQS2Hu7j1iNEi33w0KYn0+ohCwbG3Ak4EtwQqnvUqNT1O70PWu6pzanIyzrDYO1M2Tzg74XIbgohofCKXbJ/b8XR01IiGB/ejlmKp43qJSiV1uQMs2id4OpgSeWvi2g9pw5vvzev294hh4/UjY0a1l7K7z92wJopJdKmUk57Z8apHZlfuSyaOIV7QsMsTW51tSsmybAItp61cTQXxJg5yRPSZPiKfouH7x//VeucPCt0iXBqdr6iiRu8/0auxvD8WMSyzV1EoC1FktzWuXAM0Rze8tKISv5m/ku73jaPzQ/T5+dZKk43jarWM4AtzqI0m5YJsknOHjX6lFvrgKKVbEkp+vWk5uL6abv8vJCcLZV7igTmP6QuhMO/BeM4PxALX2eB+OS80KTv8lP7QLlXl/E2nKnUvI3AKcQUoa65BABV0oI95BqlEzim19EYkWEGLFJDZh2Hk5DkN0/SLP38F/uygFShnC11y/zbPbDtGJXAImXbnLfkZ7l96kpcyAQpzdBY4pJZEq0BIOjyWk/3u9zXEAU5PheozOb8Etl82JkRWXmPAq+YNqPSvkOI5uUpI+WWeoAapSv9J+A/5/HylX85hUMdfa6x0JQLb3C4B+1qLFmdYXrxmdgMCnwKvwo7TOzyklKOSz9TZ3CoX6I9/D43EoymDZ2QDryq1ZeGxWKQGoBcLjRNDUnJGnP1fa2FXe0NYWScOJkyvCYDUO2dQosg3FmUtQn1xqAvevbO+ysXuIjL38Mz+OTIlRA0+iBzCYKQ33zbHDI8pX8BWzJjhPM3mkd60FrWjfkh3q5oUOdL7vYMaT8UcJ7Ry+sgVoL3UwPFO9qLEROoH4zgDjY2QdY8hdQJZhQlQonwvlX4xyOvRoQtufmTHpVto/DXxD7uLt19ynDJyK4nyVQqX5kXbDz0tutE7wHWQrXxvQCcnqeue74b2XecpmyYi3WHp0FZVgFsVqODUHwCNBLb

Notably, this has a really nice and nuanced frame, gets into history a bit, and sells all ITPs and not just Lean: https://www.ams.org/journals/notices/202011/rnoti-p1791.pdf


  • [Coq-Club] December 2020 AMS Notice by Kevin Buzzard, Talia Ringer, 11/29/2020

Archive powered by MHonArc 2.6.19+.

Top of Page