patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
nit
danabra.mov
+1
-1
public/beyond-booleans/index.md
+1
-1
public/beyond-booleans/index.md
···
50
50
51
51
When you write `2 + 2 === 4` in TypeScript, it immediately "collapses" into some `boolean` (with a possible value of `true` or `false`--in this case, it's `true`).
52
52
53
-
**But when you write `2 + 2 = 4` in Lean, it doesn't "collapse" into anything.** The *logical statement itself* is a distinct value. It doesn't "turn" into a `true` or a `false`. A proposition remains a proposition--a speculative claim; a logical sentence.
53
+
**But when you write `2 + 2 = 4` in Lean, it doesn't "collapse" into a verdict.** The *logical statement itself* is a distinct value. It doesn't "turn" into a `true` or a `false`. A proposition remains a proposition--a speculative claim; a logical sentence.
54
54
55
55
So how do you *know* if a proposition is true?
56
56