The great virtue proof assistants, more than verifying correctness, is the ability to organize mathematical knowledge so that it is recorded and can be inspected to any level of detail by just following links.

Before I used proof assistants, I recorded my thoughts on paper notebooks, like everybody else. Then whenever I wanted to write a paper based on these thoughts, I had to both organize the thoughts and check them again. This becomes a problem if these were thoughts of 5 years ago. In TypeTopology I have thoughts recorded from 5 years ago, or more, that I didn't have time to publish yet, but I won't need to check them again or reorganize them too much when I find the time to write a paper based on them.

I find proof assistants, in particular Agda, the one I use, to be perfect blackboards/notebooks.

Another great virtue of proof assistants is that it allows for collaboration with people who you don't need to trust based on their reputation. If their code passes the proof assistant, then it is correct. So when I look at a pull request in TypeTopology from a new contributor I haven't met before, I can just "referee" it for style, relevance etc., leaving the correctness to the proof assistant.

As you know, it is easier to write proofs you've come up with than to read somebody else's proofs. It is invaluable that the proof assistant checks somebody else's proof for me, and I can concentrate on their ideas instead.