my blog https://overreacted.io
nit
+2
-2
+1
-1
public/beyond-booleans/index.md
+1
-1
public/beyond-booleans/index.md
···
320
320
321
321
322
322
323
-
*([Try it online in the Lean playground.](https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOAmApgGZwDOEIhAYgK4B2AxjMBPXABQAeAXHILiEASk5cA+gHNCogF6EoEOHy5xApkRwADMO6j0UtoUVxlgEyI4ARmE8AvDjhG4APTgAmPPTaNKYWjCRZdcESkFFQA8mhydEwsbJxIfEKKNna68MrWnABKhEjoAHRkwOxIwk6udqhIAG4GYpIycgoZWACecEhgYOhtZACOou709ITitnCVNUY6esNJcK1whFxIzHDZuQVFon3TovrtYyE0DMys7Mp1UrLyU7p7w3hAA))*
323
+
*([Try it in the Lean playground.](https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOAmApgGZwDOEIhAYgK4B2AxjMBPXABQAeAXHILiEASk5cA+gHNCogF6EoEOHy5xApkRwADMO6j0UtoUVxlgEyI4ARmE8AvDjhG4APTgAmPPTaNKYWjCRZdcESkFFQA8mhydEwsbJxIfEKKNna68MrWnABKhEjoAHRkwOxIwk6udqhIAG4GYpIycgoZWACecEhgYOhtZACOou709ITitnCVNUY6esNJcK1whFxIzHDZuQVFon3TovrtYyE0DMys7Mp1UrLyU7p7w3hAA))*
324
324
325
325
You're not always going to be so lucky to find proofs of precisely what you need in Mathlib, but that's not the point. Mathlib is just a bunch of open source proofs. Lean offers a language to express and verify such proofs, and to compose them.
326
326
+1
-1
public/the-math-is-haunted/index.md
+1
-1
public/the-math-is-haunted/index.md
···
30
30
31
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).
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
+
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](https://overreacted.io/beyond-booleans/), but we'll have to forget about them for now.
34
34
35
35
Instead, we'll start by inspecting the proof:
36
36