patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
twk
danabra.mov
+2
-1
public/the-math-is-haunted/index.md
+2
-1
public/the-math-is-haunted/index.md
···
2
2
title: "The Math Is Haunted"
3
3
date: '2025-07-30'
4
4
spoiler: A taste of Lean.
5
+
bluesky: https://bsky.app/profile/danabra.mov/post/3lv7i6rjttc2t
5
6
---
6
7
7
8
For the past few months, I've been writing a lot of [Lean](https://lean-lang.org/).
···
27
28
28
29
What's going on here?
29
30
30
-
To a mathematician's eye, this syntax looks like stating a theorem. We have the `theorem` keyword, the name or our theorem, a colon `:` before its statement, the statement that we'd like to prove, and `:= by` followed by the proof (`sorry` means that we haven't completed the actual proof yet but we're planning to fill it in later).
31
+
To a mathematician's eye, this syntax looks like stating a theorem. We have the `theorem` keyword, the name of our theorem, a colon `:` before its statement, the statement that we'd like to prove, and `:= by` followed by the proof (`sorry` means that we haven't completed the actual proof yet but we're planning to fill it in later).
31
32
32
33
But if you're a programmer, you might notice a hint of something else. That `theorem` looks suspiciously like a function. But then what is `2 = 2`? It looks like a return type of that function. But how can `2 = 2` be a *type*? Isn't `2 = 2` just a boolean? And if `2 = 2` really *is* a type, what are the *values* of that `2 = 2` type? These are very interesting questions, but we'll have to forget about them for now.
33
34