my blog https://overreacted.io
Update index.md
+1
-1
+1
-1
public/beyond-booleans/index.md
+1
-1
public/beyond-booleans/index.md
···
58
58
59
59
Just kidding.
60
60
61
-
**In Lean, you must *convince* the computer it's true--by presenting a proof.** Turns out, not only `2 + 2 = 4` a value, it is *also* a type. A proof is a value *of* that type.
61
+
**In Lean, you must *convince* the computer it's true--by presenting a proof.** Turns out, not only is `2 + 2 = 4` a value, it is *also* a type. A proof is a value *of* that type.
62
62
63
63
Let's unpack this.
64
64