my blog https://overreacted.io
link
+1
-1
+1
-1
public/the-math-is-haunted/index.md
+1
-1
public/the-math-is-haunted/index.md
···
202
202
203
203
204
204
205
-
With the bad axiom out, math is no longer haunted! (Or at least we could hope so.)
205
+
With the bad axiom out, math is no longer haunted! (Or at least we could [hope so.](https://philosophy.stackexchange.com/questions/28303/if-the-zfc-axioms-cannot-be-proven-consistent-how-can-we-say-for-certain-that-a))
206
206
207
207
It might feel a bit weird being introduced to Lean with "nonsense math" since most math that people do in Lean is usually rather sensible. But I think this is a potent illustration of what working with a proof checker is actually about.
208
208