> Those problems can’t be formally verified with an automated theorem prover.

It certainly seems like any problem that is amenable to reinforcement learning will be solved.

It does, yes. So designing objections functions and making sure you can afford the training rollouts becomes really important in defining which problems are tractable. It will be really interesting to see how that shapes the kinds of problems people choose to work on