Comment by cman1444
19 hours ago
I don't know, this just seems like gatekeeping of the term "research" simply because you don't like the way it's being done.
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.
Honestly it just sounds like you want to complain about things. It is literally in the dictionary definition of the word. We do research so that we increase knowledge and understand things better.
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.