Comment by mjfl

What is it with proof assistant designers and terrible naming instincts? "Lean" as a name collides with all sorts of business/engineering productivity frameworks "Lean software development", "lean business management", "running a lean startup". And of course Coq is phallic both in English and the original French. It must be the case that the people that design these things live in a separate plane of existence where these things don't bother them.