Comment by youoy

This all comes down to what we think mathematics is. There are two options here:

Mathematics is just the formal system: in that case we will never be able to beat the AI as humans. The goal is then to cover as much of the formal landscape with AI generated proofs to proof as much statements as possible. Success metrics are lines of lean and numbers of proven statements.

Or

The formal system is just a limited representation of what mathematics is: in that case probably some parts of the formal mathematical landscape are more important than others. Not all statements are born equal. And 90% of AI generated proofs will be just noise. Our job as mathematitians is to steer the AI to high mathematical value regions and turn formal proofs into mathematical proofs and insights.

From my point of view we have know since Godel that we are living in the reality of point 2.

Each of the two points implies a very different way of doing mathematics. So pick the one that you think is true and act accordingly.