The system automatically generates candidate theorems it might try to prove, expressing possible answers, and attempts to prove them.
In this case, the version of the theorem it ended up being able to prove was the one with 2 in that position. (Which is just as well, since—I assume, not having actually tried to solve the problem for myself—that is in fact the unique number for which such a theorem is true.)
So the thing you end up getting a proof of includes the answer, but not because the system was told the answer in advance.
It would be nice to have this more explicitly from the AlphaProof people, though.
[EDITED to add:] Actually, as per the tweet from W T Gowers quoted by “O O” elsewhere in this thread, we do have it explicitly, not from the AlphaProof people but from one of the mathematicians the AlphaProof people engaged to evaluate their solutions.
I’m pretty sure what’s going on is:
The system automatically generates candidate theorems it might try to prove, expressing possible answers, and attempts to prove them.
In this case, the version of the theorem it ended up being able to prove was the one with 2 in that position. (Which is just as well, since—I assume, not having actually tried to solve the problem for myself—that is in fact the unique number for which such a theorem is true.)
So the thing you end up getting a proof of includes the answer, but not because the system was told the answer in advance.
It would be nice to have this more explicitly from the AlphaProof people, though.
[EDITED to add:] Actually, as per the tweet from W T Gowers quoted by “O O” elsewhere in this thread, we do have it explicitly, not from the AlphaProof people but from one of the mathematicians the AlphaProof people engaged to evaluate their solutions.