Comment by golol

I would expect that in their data which they train AlphaProof on they have some concept of a "vague problem" whoch could just look like

{Formal description of the set in question} = ?

And then Alphaproof has to find candidate descriptions of this set and prove a theorem that they are equal to the above.

I doubt they would claim to solve the problem if they provided half of the answer.