> 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.