> An AI-generated solution always provides ... proof that there is a solution

This is only true in the most trivial sense. A solution is a solution, sure... but how do you know it's a solution, and not an incoherent jumble of words? A human has to review and vouch for it.

Just because the AI gives you an arxiv-worthy PDF, or a Lean proof which compiles, doesn't mean it proves what the AI says it does. The AI could give you the same PDF/Lean code and says it proves the opposite, how would anyone know the difference?

You can't advance human understanding unless you produce things that humans can understand.

This is definitely true in an information theory sense: having more knowledge is always better than less knowledge. However, it may not be true in math as a social human endeavor, and having answers without interesting paths to get there may not expand human mathematics in the same way.

If Fermat had a book with larger margins, would Weil have devoted so much time to proving the Taniyama-Shimura conjecture? No one can say.

It demotivates mathematicians. That’s a pretty large negative!