It is a bit similar to why we don't use program verification tools very much in software development. They are very complicated to use and while they do a good job at verifying existing code they don't help as much when writing code from scratch, because they tend to add extra obstacles at this stage.

From what I have seen, proof assistants in math are used when extreme rigour is desired (which is not always the case) and when working with extremely long computational proofs with hundreds of cases (where you need to work at a higher abstraction level; a human writes a program that outputs the proof and then the proof checker verifies that this extremely long step by step proof is valid)