Maybe a case could be made that the key difficulty in programming will turn out to be in formulating what program to write. I'm not sure what the analogue is in mathematics. Generally it's pretty easy to formally state a theorem to prove, even if you have no idea how to prove it, right?

The mathematical counterpart may of the "recognizing important concepts and asking good questions" variety. A friend of my has an idea of how to formalize the notion of an "important concept" in a mathematical field, and possible relevance to AI, but at the moment it's all very vague speculation :-).