patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
oops
danabra.mov
+1
-1
public/the-math-is-haunted/index.md
+1
-1
public/the-math-is-haunted/index.md
···
252
252
- My absolute favorite mathematical book, Tao's Analysis, now has a [Lean companion](https://terrytao.wordpress.com/2025/05/31/a-lean-companion-to-analysis-i/) that is being [continuously developed and updated on GitHub](https://github.com/teorth/analysis).
253
253
- The "new members" channel on the Lean [Zulip instance](https://leanprover.zulipchat.com/) is very welcoming.
254
254
255
-
Although I don't plan to write introductory tutorials (you're much better served by the Natural Numbers Game and Mathematics in Lean), I'll probably write more about specific "aha" moments, such as the "`2 = 2` is actually a type" thing I alluded to earlier. Lean combines a bunch of mindbending ideas from a rich history of mathematics *and* programming, and I felt a lot of joy rediscovering them. I hope more people will try Lean for no particular reason--it's just *fun*.
255
+
Although I don't plan to write introductory tutorials (you're much better served by the Natural Numbers Game and Mathematics in Lean), I'll probably write more about specific "aha" moments, such as the “`2 = 2` is actually a type" thing I alluded to earlier. Lean combines a bunch of mindbending ideas from a rich history of mathematics *and* programming, and I felt a lot of joy rediscovering them. I hope more people will try Lean for no particular reason--it's just *fun*.
256
256
257
257
For a certain type of person, that is.