James Davenport’s plea for providing more insights on the proof and how one got it done and … if a computer can’t solve it, is it really not provable. Shouldn’t it rather return “I can’t solve it”?
An interesting comment wrt. to the fact that William Farmer and Alan Bundy pointed me to, that is that the way mathematicians present and illustrate a proof (in publications, books, and even lectures) is not the way we actually retrieved the proof.
And it contributes to another interesting discussion, that is whether or not trusting and accepting automatically computed proofs (see the Flyspeck project).