Yes, we're in the low hanging fruit stage where folks can just say "here's the problem" and "keep going" until a result is found and it will work sometimes.
The low hanging fruit will run short. Ultimately mathematics is a field of subjective selections of problems and proofs as beautiful and interesting. Machines absolutely will struggle with what to study, what theorems are desirable, and when do be done with a proof.
While they may struggle on what to study, we'll be able to spin up millions of them.
> Machines absolutely will struggle with what to study, what theorems are desirable, and when do be done with a proof
And why do you think this would be the case? I'm not talking about today but in 1-2 years. For reference o1 was released less than 2 years ago, and we've had reasonable coding agents for 9 months or so.