But what you think of when you say "insight into the problem" might be an antiquated notion. It may be that such a thing is a rough measure of (as you almost sa

But what you think of when you say "insight into the problem" might be an antiquated notion. It may be that such a thing is a rough measure of (as you almost say) how much more likely you are to prove something else (or how much easier it would be) -- without computer assistance. But the twist is that with computer-aided proofs, being well-versed in the ways of using computers to help prove things may begin to count as having insight; and Coq (or whatever) programs may come to be studied so that one may gain insight, just as human proofs are studied today.