I was wondering about that too. They are perhaps most important tools for both CS and pure mathematics.

It’s very interesting that Lean has exploded in the mathematics community. Kevin Buzzard talks about it a lot, but I haven’t seen a talk which explains why Lean succeeded in creating a gargantuan math library whereas Coq only recently got respectable math library in “MathComp” (I am also including Analysis library).

I would like to know apart from social reasons what technical choices lead to Lean dominating (ordinary/regular/pure) mathematics.

I hear “quotients” but no one actual explains with a concrete example.