> Note that this proof while impressive does not add any value to mathematics as a human pursuit.
I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.
> one might naively expect that the natural question to ask with regards to a given problem X in a field is "What is the answer to X?". But in many cases the more valuable question is "What can be learned from studying X?"
And later
> But the currently fashionable practice of pointing a powerful AI tool at the task of answering a problem X, unguided by any human expert in the field X resides in, has created an unprecedented divergence between the production of answers, and the production of insight, to the point where the two questions have become _negatively correlated_:
That seems narrow minded. Theres both "learnings directly related to the thing studied" and "learnings downstream from the thing studied". If you imagine mathematics being a huge sudoku puzzle of unknowns you are trying to fill in, each previously empty square you are able to fill in (or gain a smaller bound on) has implications in all sorts of other areas.
It's important to remember that most mathematics is not science - large parts of it are mostly esthetic pursuits that bring joy to certain mathematicians, and sometimes happen to have unexpected benefits to science or engineering (like how number theory suddenly became important to cryptography in the 20th century).
Fermat's last theorem is a great example - it is in itself a completely irrelevant observation, not used (so far) in any larger theory. It was only pursued because (a) Fermat casually claimed to have easily proved it (almost certainly being mistaken about it), and (b) it sparked the curiosity of mathematicians because it looks so simple but turned out to be so hard.
So what does humanity gain by knowing that the theorem holds? Basically nothing. What does humanity gain from the process of proving it? As far as it is known for now, basically nothing (though it is somewhat likely that the complex theories created to prove it will find other applications). However, those that have worked on it, and the guy who did prove it, gained a huge amount of personal insight into mathematics, and surely grew as mathematicians, and will hopefully use those skills in working on other problems that may prove more directly useful. Plus, they had a great time doing it.
What this means is that, if the proof had been discovered entirely by AI, basically nothing would have been gained. LLMs don't learn by doing, so no personal experience growth would have come from this; and as I mentioned, both the result and the proof are, so far, quite irrelevant even for mathematics more broadly. So it would have been actively detrimental, or at best neutral, compared to letting human mathematicians work on this problem, in a way that is never the case in science or engineering, where any bit of knowledge is in itself useful to at least some extent.
I don't see how this can be stated with such certainty. We don't yet know what the implications of large scale autoformalization and proof verification will be on the human pursuit of mathematics. I'm open to the idea that it might be a benefit to the human pursuit once the human pursuit adapts.