Regarding Lean I would recommend to check Lean4[1] instead. They rewrote it in Lean itself and now it has much cleaner design[2][3][4]. [1] http://github.com/l

Regarding Lean I would recommend to check Lean4[1] instead. They rewrote it in Lean itself and now it has much cleaner design[2][3][4]. [1] http://github.com/leanprover/lean4 http://github.com/leanprover/lean4 [2] https://leanprover.github.io/papers/lean4.pdf https://leanprover.github.io/papers/lean4.pdf [3] https://leanprover-community.github.io/lt2021/slides/leo-LT2021.pdf https://leanprover-community.github.io/lt2021/slides/leo-LT2... [4] https://leanprover-community.github.io/lt2021/slides/sebastian-lean4-parsers-macros.pdf https://leanprover-community.github.io/lt2021/slides/sebasti...