This is largely because in modern mathematics, people ignore or won't build on proofs that are too complicated for them to follow, and rely heavily on trust and

This is largely because in modern mathematics, people ignore or won't build on proofs that are too complicated for them to follow, and rely heavily on trust and networking effects for the remaining proofs that are too useful to ignore. Plenty of results (including big results) are published in mathematical journals each year, which are "known" to be flawed or sketchy, but never have a formal rebuttal, and if you want to build on a proof that doesn't have much followup work, and are having trouble understanding its argument, you're expected to ask around and find out whether the proof is worth pursuing or not. Proof assistants would enable people to trust much more complex proofs from much more junior mathematicians, rather than essentially requiring the community to reprove the same results over and over until they're satisfied, and IMO this is holding back mathematics more than many mathematicians realize.