>>14179290This is interesting but you are being a bit retarded with your framing.
First, as you can see right now these theorem provers need to be adapted to solve particular problems. This means that at best what they can do is to find a proof for a problem (properly defined in its language) only after you give it all the pieces of the puzzle yourself.
It currently can't:
1) Attempt to solve arbitrary problems (you need to adapt it)
2) Know in which direction to focus its training if it wanted to discover new things
3) Know how to pose itself new problems that further its own learning.
All of those 3 are currently only done by real mathematicians. I believe that in the following 50 years we may get an NN that can do 1). In 100-200 years maybe it could do 2). And in 300-500 years maybe it could do 3).
So we have 500 years of human mathematics yet. And by contributing to mathematics today, you also contribute to the eventual creation of these math AIs that can actually advance math on their own.
Will be fun when we finally build this AI and we can just plug into it all the yet unsolved math probelms (RH, for example) and then after waiting for it to process a bit just get the answer.
