There's a very big difference between solving one problem (if you through enough compute at it you obviously will succeed) and general proving being solved. The latter essentially means being able to replace all programmers, that'd effectively mean AGI in 5 to 10 years.

>>doing some GAN like system of both generating problems that yet can’t be solved and a solver to solve them seems to obviate the need for human training data.

I don't see how this is supposed to work, what if the generator just outputs unsolvable problems?