Here's what I forsee. GPT3 (or the like) learns strategies to solve problems in a limited DSL (like isabelle). Prompt GPT3 with a problem (e.g. P = NP). Have it walk down the tree of proof possibilities (possibly using Q-learning), trim incorrect branches, and then out comes a proof. Somewhere in its modestly coherent glossolalia, GPT3 will figure out how to prove something "tough for humans" correct. Nice thing is, you might even be able to paralellize the search using independent agents.
Is there anyone working on this? Drop a line.