What are the pros and cons of proof assistants?

Automated for routine tasks of building proofs.

Require human guidance for more difficult aspects.

In general more flexible than Automated theorem prover.