Why does this tend to be the case, even when some of the smartest people in the world have historically predicted incorrectly that certain branches of math would forever be useless (e.g., number theory)? I can only offer my own theory on that, but my guess is that mathematics is simply a predictive framework based on pattern compression. A more powerful pattern compression framework accelerates every single field that relies on pattern recognition or prediction of the unknown based on patterns.
The output might make a cool screen saver as-is, but we probably need a way to evaluate it somehow.
Let me make up an example of where I could imagine this going. Something we essentially cannot do right now is predict coarse-grained phenomena from systems that involve millions or trillions or more of interacting components. Over hundreds/thousands of years of experiment and theory we've derived laws that essentially do this in a few special cases, but we have no systematic theoretical way of doing it in general, and frankly I think it's beyond human ability. Whatever deep patterns or structures exist for doing this in a general way I think are simply out of reach for us.
That's a misconception. Only a tiny percentage of mathematics has seen any applications whatsoever. There are vast libraries full of mathematics no one (in this discussion, anyway) has ever heard of that no one reads anymore and has never been applied to anything.
This idea of trying to "prove all the math" with AI makes as much sense to me as using chess engines to try to "solve chess."
And that's an issue why? It would seem to me that producing that also produced the mathematics that revolutionized the world repeatedly for centuries. I would go further and claim that, if you want the mathematics that revolutionizes the world, there's no way to get it without advancing mathematics as a field broadly. Those are not two separate activities, and thinking that they are is indeed a misconception.
> This idea of trying to "prove all the math" with AI makes as much sense to me as using chess engines to try to "solve chess."
You're right: "prove all the math" does not make sense on any level, and nobody serious would phrase any of this in that way. I certainly didn't.
The issue is SNR: signal to noise ratio. Generating exponentially more mathematics, particularly if the process is indiscriminate or optimized for something other than usefulness or mathematical relevance (such as optimizing for machine-provability), does not imply that we get exponentially more applications. We may end up halting the progress of applications altogether as the entire capacity of the world's mathematical apparatus is consumed by the interpretation and investigation of machine-generated proofs.
You can already visit arXiv and find vast numbers of not-yet-published mathematical papers. Most should never be published. None of this junk is benefitting humanity in the slightest.
Moreover, the disdain you have for low-value output in mathematics is not unique to you. Talented mathematicians don't like it either. Your mistake is assuming that AI will cause math to be dominated by low-value outputs. In fact, the opposite is likely the case: the marginal value of proofs will fall so low that the bar for meaningful research will become dramatically higher, not lower. I expect the goals of research mathematics to become extremely ambitious relative to the past, organized around substantial and enormous goals, not mass-generated slop as you're imagining.
Of course, yes, there will still be lots of slop, just like GitHub is full of AI coding slop, LinkedIn is full of slop, etc. But that's a generalized issue of the AI era, not unique to math.
I didn't say anything about low-value output. No one actually knows the value of any particular piece of mathematics within that deluge. Mathematicians don't have a magical ability to differentiate high-value mathematics from low-value merely by reading paper titles and abstracts.
The dirty secret in the mathematical world -- that has been going on for a long time already -- is that papers get attention based on the reputation of the authors, not on the rigour or validity of the proof. The big headline-grabbing papers are getting read by mathematicians because AI researchers have leveraged media exposure to bypass the reputation network, but media exposure doesn't scale.
When everyone is using LLMs to generate proofs, only reputable mathematicians will be able to get their work read. And herein lies the crux of the problem: an exponential takeoff in the volume of output from respected mathematicians will leave a critical shortage of readers.
it could end up being far easier to reasonably direct and evaluate the research direction and output of AI systems than human mathematicians
That's baseless speculation. All indications so far are that LLMs produce proofs far longer and far more complicated than humans are capable of, such that only machines can check the proofs for validity. Digesting them into a human-readable interpretation of the results is an open problem.
False. You very plainly did. You simply used the term “junk” instead.
> That's baseless speculation.
It might be speculation (as is much of what you’re writing), but it’s not baseless. Obviously, it’s quite easy to direct AI agents, a single one of which can pivot across all of mathematics, unlike all human mathematicians.
> All indications so far are that LLMs produce proofs far longer and far more complicated than humans are capable of, such that only machines can check the proofs for validity.
I’m unaware of any clear evidence of this. Hence, it appears to be baseless speculation.
> Digesting them into a human-readable interpretation of the results is an open problem.
I’m unaware of any clear evidence of this. Hence, it appears to be baseless speculation. Moreover, and more importantly, to my knowledge there hasn’t been any meaningful result in AI mathematics so far that has posed any kind of blocking issue on understanding it yet.
I'm deeply suspicious. I do not yet have a concise statement for why, but a lot of literature on the sociology of knowledge work sort of points at my thoughts.
Section 5 of the Thurston article cited by Tao touches the elephant. Raduchel's article on the economics of software [2] also touches it.
I've tried to put words to this for a few years. I think I'm just going to start writing versions of it as see if that helps me shape the thought into something more concise.
So, in the spirit of this article's style, here are some postulates:
1. There is a sociological process happening in the production function during knowledge work.
2. That production function and the associated sociological process spans years or even decades, and must outlast many of the artifacts that are produced during the early years of the function.
3. You cannot get the right lines of code or the right theorems proved without running that sociological process alongside the artifact production process.
4. It is impossible to completely separate the sociological process from the artifact construction process. If you just iterate on artifacts then too much of the required hidden state is lost to make progress in the right direction. This is true even if you include distilled artifacts capturing pieces of the sociological process (eg meeting notes, documentation, commit logs, prompts).
5. So you need that sociological process, or something like it, to still happen.
6. For a lot of knowledge work that process plays out in extremely high-fidelity social interactions [3] that we have not yet captured in the datasets that would be required to reproduce those dynamics.
7. And even if we do collect that data, our current architectures and training algorithms and hardware would be useless given the size of the datasets.
So: the technology today gives us the ability to iterate on the production of artifacts. But it does not sufficiently simulate the social process which gives rise to the Right artifacts.
This isn't exactly what I actually think, but it's a version of the thing that I intuit when I watch heavy use of AI in both software projects and formalization projects. And simulating that process feels way harder than people are currently assuming.
[1] https://arxiv.org/pdf/math/9404236 Section 5.
[2] https://www.nationalacademies.org/read/11587/chapter/11 pp 166-168.
[3] there is a reason we still gather in-person around white boards, and why doing so is more crucial for some types of work than others.