Comment by creatonez

As 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.