But I guess a fundamental problem for an RL-based approach (and a pretty interesting question in itself) is how difficult it would be to say what makes any mathematics "interesting".
The interview touches on the Langlands program several times, and that is a good example: how "interesting" Fargues-Fontaine curves were perceived (even by their creators) changed substantially after Peter Scholze created a whole new world for that curve to live in. So how do we tell the computer that they're sort of halfway to something really interesting, and, perhaps even more importantly, how do we communicate it to humans once we're there? Even Scholze himself was skeptical when first presented with this direction, and those are the humans most intimately familiar with those theories. Imagine how hard it would be for any human to grasp what the AI had just done, let alone judge its relevance, after it's made progress on its own, using new mathematical objects it had just developed, solving problems it had set itself. It's not like DALL-E, where anyone can just go and say - yeah, that looks like a cat with a party hat, great job.