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.
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Notes for future OT posters:
1. Please add the 'open_thread' tag.
2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)
3. Open Threads should be posted in Discussion, and not Main.
4. Open Threads should start on Monday, and end on Sunday.