Zulip Chat Archive

Stream: general

Topic: Wrote a blog post about Lean


view this post on Zulip Andrew Helwer (Apr 06 2020 at 00:48):

General theme is how it has clarified my thinking about proofs, and I wish I'd learned it while learning about proofs in the first place! https://ahelwer.ca/post/2020-04-05-lean-assignment/

view this post on Zulip Johan Commelin (Apr 06 2020 at 05:35):

@Andrew Helwer Nice! I enjoyed it. (Note that the community also hosts an online web editor that does include mathlib.)

view this post on Zulip Johan Commelin (Apr 06 2020 at 05:36):

https://leanprover-community.github.io/lean-web-editor/ (It can be a bit slow to start, because it has to download Lean and precompiled mathlib.)

view this post on Zulip Andrew Helwer (Apr 06 2020 at 14:59):

Sweet, I've updated the post to use the community editor!

view this post on Zulip Johan Commelin (Apr 06 2020 at 14:59):

@Andrew Helwer Did you also see the hackernews discussion?

view this post on Zulip Johan Commelin (Apr 06 2020 at 14:59):

They spotted some typos over there

view this post on Zulip Andrew Helwer (Apr 06 2020 at 15:00):

Oh yes, the error with the sigma... classic. Also fixed!


Last updated: May 14 2021 at 03:27 UTC