alt Hacker NewsAs I understand, he was specifically targeting problems that symbolic math software had given up on. He was only using symbolic software to solve the similarly shaped problems first, which allowed him to be fairly confident in his conjecture, as he became quite keen on how to slip his way from the output of symbolic math software from one solvable formula to a closely related formula that broke the software.
The symbolic math software couldn't perform the integration problems he posted. Integration lacks a deterministic algorithm and therefore permits constructing challenges for stack overflow and computer algebra systems. However, there is a deterministic algorithm to go the other way.
In other words, he was posting challenges to go from X -> Y (hard). However, going from Y -> X is easy. Therefore, since he had both X and Y before posting, he could verify the solutions perfectly well. The reason why constructing (X, Y) together is easier than going from Y->X is because you can always tweak Y a bit and then work backwards to see what X falls out.
There was certainly creativity in finding (X, Y) pairs where the symbolic software couldn't go from X -> Y. However, again this is more about trial and error iteration than producing brilliant insights from scratch, which is what it appeared Cleo was doing on Stack Overflow. Again, this is just a consequence of X -> Y being hard but Y -> X being easy. It was a wonderful parlor trick that took a good deal of effort to set up.