my blog https://overreacted.io
twk
+1
-1
+1
-1
public/the-math-is-haunted/index.md
+1
-1
public/the-math-is-haunted/index.md
···
208
208
209
209
A proof checker only verifies the validity of the logical conclusions stemming from the chosen axioms. It lets you chain logical transformations--with `rewrite`, `rfl`, `exact`, and many other tactics--and prove increasingly sophisticated theorems about increasingly sophisticated mathematical structures.
210
210
211
-
If your axioms are sound and Lean itself is sound, your conclusions are sound. And that's true whether your proof is just a `rfl` or millions of lines of Lean code.
211
+
If your axioms are sound and Lean itself is sound, your conclusions are sound. And that's true whether your proof is just an `rfl` or millions of lines of Lean code.
212
212
213
213
---
214
214