[edmccard]

>We'd ask it to produce a simplified version.

Yeah, that would work :)

Maybe the question I should have asked, is:

What if we ask a super-AI for a proof of the ABC conjecture, and the result is something too complicated for humans to verify?

My point, if I have one, is that when I read about "superhuman machine intelligence", sometime people seem to mean "capable of knowledge that humans couldn't figure out on their own but that humans can understand once they see it"; and sometimes they seem to mean "capable of knowledge that is beyond human capacity to even verify".

I think development machine intelligence of the first kind is extremely likely, but I'm more skeptical about the second kind.