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/

Here's another article I wrote that gives some intuition about the role of axioms in Lean: https://overreacted.io/the-math-is-haunted/

And here's a longer primer on Lean's syntax: 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

This is the best intro to Lean I know, plus it teaches you why a + b = b + a.

I love your posts! The Social Filesystem is amazing!

https://overreacted.io/a-social-filesystem/

        induction b with d hd
        rw [add_zero, zero_add]
        rfl
        rw [add_succ, succ_add]
        rw [hd]
        rfl