Wiles may be a great mathematician but he seems to not really understand the programs he is talking about:

“I think computers, if they were to develop mathematics themselves, would not be worried about smallness and elegance,” Wiles pointed out. They might generate proofs that contain thousands or millions of steps. “Why would they worry how long it is?”

Well that's a constraint you can program in your heuristics: use as few steps and as few concepts as possible.

But we have to wonder as well if some proofs do not require anyway a number of steps that is out of humans' reach