pros/cons 

The main issue is proof automation. Curry-Howard based provers (Coq, Agda, Lean etc) are nice for teaching but if you want to get work done (e.g. you want to verify an OS kernel), you need to automate as much as possible. Isabelle/HOL currently has by far the most powerful automation. This is partly because, like Coq, it is an old system (unlike Lean and Agda) and lots of automation has been built in the past, but also because a lot of automation is much easier to adapt to provers based on classical logic (as opposed to the constructive logics that Curry-Howard needs (yes, I know that classical reasoning can be done within constructive logic)). Adapting proof automation that has been available for a while for Isabelle/HOL to Curry-Howard is at least in parts an open research problem. Lean has been created in parts because of the urgency of given Curry-Howard systems much better proof automation.

There is an additional dimension which is strength of the logic at hand. The logics Coq, Lean et al are based on are more expressive in various dimensions. Whether that's relevant to your use case depends on what kind of maths you are trying to formalise. If it is higher category theory, it matters a great deal, for program verification it tends not to be important b/c most program verification can be done in rather weak logics.