> AI can do proofs, but deciding which problems to solve, which math is useful, is by humans.
This is within a very narrow view before the emergence of always running “minds” within any given domain. The only reason they don’t exist now is because they’re expensive.
Pretty soon we’re going to have always running minds that are constantly thinking about every domain imaginable and coming up with their own proofs and improvements and everything else imaginable within those domains.
Isn't this basically the hitchhikers guide to the galaxy passage on the computer that spends millions of years to determine the ultimate answer to be 42 and then when people get upset at how meaningless that answer is offers to build another even bigger computer to figure out what the question was.