Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans

Lean is super cool. If you're curious how proof checking works (on the type system level), I wrote an article about that: https://overreacted.io/beyond-booleans/ https://overreacted.io/beyond-booleans/ Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/ https://overreacted.io/the-math-is-haunted/ And here's a longer primer on Lean's syntax: https://overreacted.io/a-lean-syntax-primer/ https://overreacted.io/a-lean-syntax-primer/ Finally, if this got this even a little bit curious, I strongly encourage you to play the Natural Number Game: https://adam.math.hhu.de/#/g/leanprover-community/nng4 https://adam.math.hhu.de/#/g/leanprover-community/nng4 This is the best intro to Lean I know, plus it teaches you why a + b = b + a.