trepplein

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/sca...

> Offtopic: Lean's effort seems strange to me. Usage of C++ as its implementation language gets me really nervous, I feel doubt in its reliability. Not only is this unfounded, it's unreasonable. I can interpret "reliability" in two ways: 1. The tool crashes a lot This isn't true in practice, and it throws an exception with about the same frequency that Isabelle throws an ML exception, for me. I haven't observed any segfaults but they do happen sometimes (and are usually fixed quickly, Leo is really awesome). Lean is written in pretty principled C++. 2. You don't feel safe trusting it when it says it proves something Any tool worth its salt in this space satisfies the "de Bruijn criterion" -- can have a small, independent checker. In this case, Lean's kernel is the calculus of inductive constructions with a non-cumulative hierarchy of univ