How Math’s Most Famous Proof Nearly Broke (2015)

Re:How Math’s Most Famous Proof Nearly Broke (2015) by chestervonwinch on Friday December 21, 2018 @07:57AM (#18733023)

https://leanprover.github.io/

[ Parent | on HN ]

Re:How Math’s Most Famous Proof Nearly Broke (2015) by williamstein on Friday December 21, 2018 @10:14AM (#18733752)

LEAN has significant momentum right now. I was at the International Congress of Mathematical Software this summer (as a plenary speaker), and the other plenary was about LEAN, as were a bunch of talks. There are also excellent VSCode, Emacs, and CoCalc modes for using LEAN. The Zulip LEAN chat channel (https://leanprover.zulipchat.com/) is also very active.

[ Parent | on HN ]

Re:How Math’s Most Famous Proof Nearly Broke (2015) by tunesmith on Friday December 21, 2018 @01:39PM (#18735451)

How does LEAN compare to Coq/Isabelle/Agda?

[ Parent | on HN ]