You are misunderstanding what mathematics research is. Its objective is the development of human understanding of mathematics. This requires open problems to research. AI are “solving” the open problems without creating any human understanding.
I'm pretty sure OpenAI's proofs, while difficult to understand, have a net-zero impact on human understanding of mathematics. It took the first Millenium problem years to verify its accuracy. It's only been days since OpenAI released its problems, surely it would take years to evaluate whether the solutions meaningfully advanced human understanding.
All mathematics researchers in the whole world have agreed upon that objective apparently?
Many of them - all but a couple of the living Fields Medalists - recently signed an open letter about this.
Many modern medicines do not have understood mechanisms of action, yet we know they work. Are the people who found them not conducting drug research?
Do we even have a different term for what the AI labs are conducting if it's not mathematical research?
Additionally, I would argue that any work that adds to the total corpus of known facts increases human understanding, even if the path to get to each fact isn't understood. It's hard to argue we'd be better off with less total information.
What the AI labs are doing is mostly AI research. They are trying to test the limits of AI's ability to do mathematical research. This has been a productive subfield of generative AI research. So far, AI can't do mathematics research unaided - it can't both produce an original result and explain it to people. But they are getting better - developing original results is itself a tremendous achievement, and it probably does prove some things that are important to AI research (such as that it should continue to be funded prodigiously). Developing tools to aid mathematics research is not itself mathematics research, though it may both require new mathematics research and also contribute to mathematics research.
The difference is the subject area that is being developed. Developing the Lean theorem prover was mostly computer science.
1 : studious inquiry or examination especially : investigation or experimentation aimed at the discovery and interpretation of facts, revision of accepted theories or laws in the light of new facts, or practical application of such new or revised theories or laws
2 : the collecting of information about a particular subject
3 : careful or diligent search
Nothing here requires human understanding to be the goal. In fact, it explicitly calls out "practical applications" as one of the purposes that can be aimed at.
The whole field of applied mathematics is for the purpose of finding practical applications. Therefore any research conducted in this field is not for the exclusive purpose of human understanding or knowledge.
I'm not complaining, you're just restricting the definition of mathematics research in order to discredit what the AI labs have achieved.