The skills needed to formalize the proof and come up with the proof are probably quite distinct. There are many people now who understand the proof well. Also, even if Wiles would be the best person to do it, he might be more inclined to spend the next five years on new mathematical ideas rather than on convincing a computer program his old ideas are correct.