> A computer might "figure out" that it's easier to give us something that looks like what we're looking for instead of what we're actually looking for.

As a mathematician, that seems like my idea of a dystopia. Shiver.

On the other hand, assuming that it doesn't go off and develop sentience on its own, how would a computer figure out such a thing? Assuming that it is programmed in such a way that it only produces correct proofs of (possibly uninteresting) theorems, there'll be no way for it to produce those 'easier' deceptitheorems in order to be rewarded for doing so.

Well, that's why I put "figure out" in quotes; it would probably be closer to an evolutionary process. Some instance of an algorithm stumbles onto a simple process for generating proofs that it deems okay to submit, and never gets its power yanked for doing so because the algorithm fakes us out.

The hypothesis class that the ML algorithm works within is proofs, checkable by something like Coq, so that can't actually be done.