Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean (e.g. a scala implementation [1]). Lean's power lies i

Lean allows for third party type checkers. There are relatively small alternative type checkers for Lean (e.g. a scala implementation [1]). Lean's power lies in its elaborator that breaks down complex tactic-based proofs to a core proof language. This elaboration process can be extended with custom tactics and custom syntax, making it way more powerful than metamath. [1] https://github.com/gebner/trepplein/tree/master/src/main/scala/trepplein https://github.com/gebner/trepplein/tree/master/src/main/sca...