[daxfohl]

Actually maybe I take that back. I mean, it took how many centuries for humans to invent calculus? Maybe AIs left to their own devices in a reinforcement-learning context could do better.

The interesting thing though, is given free reign to prove whatever they want, they may go off and develop some entirely new field of mathematics and proving really deep stuff, but we just wouldn't recognize it as interesting. Like imagine if such an AI existed 200 years ago and invented Turing machines and proved P != NP, but it wasn't all that great at solving polynomials for whatever reason. We'd have probably thought it was all rubbish and threw it away.