>>11700706Claims about the expressivity of the underlying type theory. In a nutshell, he said that Lean's foundations are better than Coq's.
First things first, they are fairly similar, and this kind of differences is not what makes a proof assistant successful or not. As usual for programming languages, and even more specifically in the case of proof assistants, tooling often ends up being more important than the underlying system. So a minute difference in the type theory is unlikely to reduce the sheer horror and grunt work that computation formalization is.
Second, as a matter of fact, one of the Coq devs proved that Lean proof terms could be actually translated automatically to Coq.
https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581The point is that Lean makes dubious choices when it comes to the underlying theories. For instance, they decided against decidability of type-checking, which has other consequences on the overall properties of the language, including subject reduction and strong normalization. Coq makes this choices opt-in (you want a broken type theory, you have to ask explictly for it) while Lean embraces it and provides no way to safely encapsulate those unsafe features. If I had to take a guess, I'd say that Lean was implemented by people that were not really experts in type theory, and that initial flaky design choices will result into long-term issues.
