Does that mean AI is not doing something useful? If it provides a proof, it gives direction to human mathematicians who can then develop an understanding, give talks, be questioned about the topic, and teach. Is that not a useful service?
That said, getting a point solution and not knowing the path to get there, is certainly much less useful, and generalization is much harder. Again, more work for mathematicians, but maybe without the easy "I solved it" proof metric for rewards. Goodhart's law strikes again.
I think you have a point, but this is the reality we have to face. The genie is out of the bottle. Even if OpenAI stops publishing AI-generated proofs, it's only a matter of months before tools with similar capabilities are in everyone's hands.
Hopefully, this genie will grant us a few wishes