Only a little but I'm hoping that some weekend reading up on Canonicity and Subject Reduction (now that I know these are the issues at play) will shed some light.
I'm interested in both Lean and Coq but what I'm most excited about is the (Lean-based) Mathlib project.
I can believe that Lean may have made the wrong call on quotients (I guess with `quot.sound`) though I am not qualified to decide. If this is so, I imagine that it will manifest in terms of a natural limit on how far a project like Mathlib can push its borders before it reaches some sort of natural limit (maybe where the complexity of formalising what we want to say dominates the inherent complexity of the statements themselves).
However from what I've seen, Mathlib is by far the most successful formalisation project in terms of what seems to matter most sociologically right now: attractiveness to mathematicians. Whatever its fate, I think it will help make formalisation of mathematics much more mainstream, and will teach us a lot. I still think that a univalent type theory looks like most promising candidate, but we'll have to wait and see.