> Lean 3 is implemented in C++ and apparently is much faster than Coq. 1. The parent didn't comment in any way on Coq's performance, they barely mentioned Coq

> Lean 3 is implemented in C++ and apparently is much faster than Coq. 1. The parent didn't comment in any way on Coq's performance, they barely mentioned Coq at all. 2. Coq is implemented in OCaml, which produces pretty good code. If Lean is faster than Coq, that's more likely due to more optimized algorithms or data structures. 3. Your wording using "apparently" suggests that you don't even have practical experience with this, you just want to promote a software system you have never used? What is the point of a comment like this?