[digama0]

The verification of entire proof libraries (like the entire Coq standard library, or the Isabelle Archive of Formal proofs) usually ranges from hours to days, as do some of the larger computer science projects like seL4 and CakeML.

You are right, verification is much faster than coming up with proofs, and that explains the majority of the disparity. But then why are we reinventing proofs so much? This is clearly needless work, and there are a thousand ways to solve the problem but even recognizing that it is a problem is difficult in certain circles.