AI 与人类社区：数学研究的未来走向

This is a response to the following blog posts, in particular the first one:

Kevin Buzzard, “To grieve, or not to grieve”
- Of all the essays I’ve read about the future of math research post-AI, I like Kevin Buzzard’s in particular. His work on math formalization, in which I was very interested even before AI, accidentally laid the foundation of the current revolution. His prediction, like many similar posts, builds on the assertion that AI can’t do theory development in math. Which might be true, but IMO is beside the point, as I discuss below.
Timothy Gowers, “Why I didn’t sign the Fields medallists’ letter”, on Terry Tao’s blog
- Since writing this, I realized that Tao has been hosting a ton of guest writers on his blog, all offering their own commentary about the future of math post-AI. Some of them say very similar things to what I argue here. Oh well. It’s my blog, and I like my framing, though it may not be as original as I thought.

We live in a world full of incomprehensibly massive neural networks, each possessing vastly superhuman intelligence, that have demonstrated an ability to solve mathematics problems far beyond any individual mathematician. In fact, these neural networks are responsible for nearly all mathematics theorems ever proved, as well nearly all scientific, technological, and political progress throughout all of human history. The neurons in these neural networks are called humans, and the edges between them are language. I am speaking, of course, of communities.

These neural networks don’t get the recognition they deserve because (1) they’re very slow and (2) they’re hard for us to see, embedded in the middle of them as we are.

Why I Think This

“If I have seen further, it is by standing on the shoulders of giants”

– Isaac Newton

“Science advances one funeral at a time”

– Max Planck

Consider scientific research communities, which I think are probably the clearest and most intentional implementation of this community-as-a-single-intelligence construct. Scientists will recognize that the way science advances is by one scientist’s theory gaining acceptance by her peers. In fact, I’ve heard the role of a scientist directly defined as “answering questions that are interesting to the research community.”

The process, for readers unfamiliar with Kuhn et. al.: when a scientist’s new theory is published, other scientists read it and the associated evidence, and they find it compelling or not, depending on their life up to that point. Over time, and if the theory is true, evidence supporting the theory accumulates—one can never definitively prove that a scientific theory is true, but, per Kuhn, scientists will encounter opportunities to disprove it and fail to do so. Eventually, the prevailing theory becomes the favored explanation of every scientist in the research community for their collective experience, and they begin using its language. If a few stubborn holdouts in the community never come around, they eventually, per Planck, die. The success of a theory manifests in the evolving language used by these peers in their correspondence with each other.

The scientific method is not the only process for accomplishing this, of course. Mathematicians engage in theory building, and a mathematician’s theory gains acceptance among her peers to the extent that it allows them to prove their own theorems. The success of the theory manifests in the evolving language used by these peers in their proofs and other correspondence with each other.

Indigenous communities in the northwest Amazon rely on bitter cassava for roughly 80% of their caloric intake. This hardy and nutrient-rich root vegetable contains high levels of cyanogenic glucosides that will you kill you over about 20 years of eating it. These indigenous communities developed complex, multi-day detoxification processes that make it safe to eat for an entire lifetime, despite no individual understanding of the underlying mechanism. When Portuguese traders brought bitter cassava to West Africa in the 16th century, communities there ate it without treating it, and many people became very ill and died. Over four centuries, these communities developed their own unique detoxification processes as well, likewise without understanding the underlying mechanism, and all now consume it heavily. Calling these traditions “theory” requires stretching the word’s meaning quite a bit, but there’s no question that the language used by these communities evolved as they developed these traditions.

(The broader theory of cultural evolution provides more examples.)

If this is how humans get things done—if community and language are as essential to us as honey to bees, responsible for our continent-spanning societies, microchips, CRISPR, online bullying, and Juicero—what effect can we expect AI to have? LLMs, as they’re implemented today, don’t have the kind of persistence that would allow them to be a “node” in this larger neural net. Current AI doesn’t have a “life experience” the same way a human does, and convincing an AI to accept your theory can’t change the discourse in a larger scientific community.

What about creating new language, or theory development? Buzzard observes that, in math, AIs haven’t been doing this ¹ ². I’m not sure whether that will last forever. But, even if LLMs gain the ability to do theory-building, their theories will still have to gain acceptance from a community of humans, otherwise there’s no way for these theories to persist.

I think that for this to change, the way AI works will need change in a fairly fundamental way, which doesn’t seem (to me) to be on the agenda of any frontier labs. Maybe, eventually, AIs will have lifelong memories and identities within larger communities. Maybe those communities will contain humans, or maybe AIs will form their own communities that work similarly to ours but are more powerful. It’s all science fiction today, though.

Until then, humans have their role. In math, we’ll need communities of human experts fluent in the evolving frontier of mathematical language for the machinery of human progress to continue running. I think we should organize our societies so that those people can continue being paid to do math full-time. Frankly, though, I doubt they’ll stop doing math—for that to happen, they would have to stop talking about math completely, which I don’t expect. The good news is that LLMs, with their superhuman ability to acquire, use, and teach language, may make those communities more accessible than ever³.

An AlphaGo Zero of mathematics? - Many HN commenters (e.g. one old example) compare “AI can’t do theory development” to past arguments that chess AIs would never learn to be “creative” like human players, and predict that LLMs will, similarly, render such claims absurd.

This led me to observe an interesting (I hope) analogy: DeepMind created several versions of AlphaGo, culminating in AlphaGo Zero, which learned the game exclusively through self-play and developed its own principles and strategies. Perhaps, for LLMs to demonstrate similar creativity in math (and do the “theory building” that Buzzard describes), we would need create an “AlphaGo Zero” of math—some kind of LLM that retraces the development of mathematics since Euclid on its own. Is this proposal coherent? Is it possible? I don’t think so, but I don’t really know. If it’s impossible, then maybe LLMs really will never do theory building, and the impossibility is why. ↩︎
If computers are checking the proofs, how will humans come up with new math? - many commentators have complained that with AIs writing proofs, humans won’t be forced to do the kind of intellectual exploration and reckoning that leads to new math. Another observation is that one could level the same criticism at Buzzard’s project to formalize research mathematics. Without the need for them to review new proofs, how will “the elders” (to borrow Buzzard’s language from his 2019 talk) stay on top of the field and come up with new math of their own? Therefore, is the problem AI, or the use of computers in mathematics at all? ↩︎
What about math, though? - I’m really not a mathematician, except insofar as I think software is a kind of applied math (more on this in future posts, I hope). I wonder, though, if mathematicians may indeed find their discourse looking more and more like software development discourse looks today, with less discussion of whether any given theorem can be proved and more discussion of how it can be proved, whether existing abstractions admit an elegant proof, and what kinds of proofs new abstractions enable. Somewhat like our endless discussion of Javascript frameworks. ↩︎