Automated theorem proving is a different problem entirely and it's obviously not ready yet to take the place of human mathematicians. I'm not in disagreement with you here.

However there's no conflict between being 'insightful' and 'intuitive' and being computer-verifiable. In the ideal case you would have a language for expressing mathematics that mapped well to human intuition. I can't think of any reason this couldn't be done. But that's not even necessary -- you could simply write human-understandable versions of your proofs along with machine-verifiable versions, both proving the same statements.