Zulip Chat Archive
Stream: general
Topic: Wrote a blog post about Lean
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/
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.)
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.)
Andrew Helwer (Apr 06 2020 at 14:59):
Sweet, I've updated the post to use the community editor!
Johan Commelin (Apr 06 2020 at 14:59):
@Andrew Helwer Did you also see the hackernews discussion?
Johan Commelin (Apr 06 2020 at 14:59):
They spotted some typos over there
Andrew Helwer (Apr 06 2020 at 15:00):
Oh yes, the error with the sigma... classic. Also fixed!
Last updated: Dec 20 2023 at 11:08 UTC