patricktree.me
forked from
danabra.mov/overreacted
my blog https://overreacted.io
tweak
danabra.mov
+1
-1
public/the-math-is-haunted/index.md
+1
-1
public/the-math-is-haunted/index.md
···
147
147
148
148
Here, the goal of `two_eq_three` happens to be exactly the same as the statement of the `math_is_haunted` axiom, so we're using the `exact` tactic to close the goal.
149
149
150
-
Armed with `math_is_haunted` and more tactics, you can prove even more sinister things. For example, why don't we prove that `2 + 2` is actually `6`:
150
+
Armed with `math_is_haunted` and some tactics, you can prove even more sinister things. For example, why don't we prove that `2 + 2` is actually `6`:
151
151
152
152
```lean {6-7}
153
153
theorem two_eq_two : 2 = 2 := by