For one thing, the point of a proof is not its use merely for showing the validity or invalidity of a statement, but in the generation of new approaches/theorie

For one thing, the point of a proof is not its use merely for showing the validity or invalidity of a statement, but in the generation of new approaches/theories. Atleast that's my view of Math; this is not to say either that being able to verify proofs is bad (this is orthogonal), nor is to say that there aren't proofs that can't be worked out by pencil-paper. On a meta level, it seems unlikely that a computer will be able to create theories and abstractions while trying to solve such problem, given the current state of AI, in the conceivable future. I do believe such "unsupervised learning" is necessary for doing math. This of course is quite a different line of work than in PL/Verification where one only cares if something they've written can be proved to satisfy some properties. However, I've heard often that a proof of a program is often as long as the program itself; this is often reflected in the difficulty people have in parsing code without adequate high-level milestones.