I think I already answered this in my comment. I claimed that I don't see much value in a magical black box theorem-proving oracle whose proofs could not, and would not, be understood by humans.

If you disagree (as the GP does, apparently), I ask you--what value do you see in it?