The science fiction author William Gibson's pithy observation that "the future is already here—it's just not very evenly distributed" has had different shades of meaning since it was first formulated. In its original context, Gibson meant it as a measure of technological progress: certain people have access to gizmos, gadgets, and virtual reality dugongs before that blessed day when those innovations trickle down to the rest of us.
There has always been an economic valence to this quote: its first full appearance includes a mention of the “elite.” Over time, though, what I might call the post-Gibson interpretation of this insight tended increasingly towards economic inequality and left the technological aspect behind, since economic security is the axis along which "difference" has seemed to vary the most meaningfully across society since, say, the dawn of the iPhone, and "progress" stopped feeling like the right way to describe how technology has been changing once we all started to pack more computational power in our pockets than what was necessary to take humans to the moon. The most salient ways the rich differ from us these days no longer seems to lie in the technological horsepower they can harness, but more in the privacy they can rely on, the laws they can break, the impunity with which they can disregard the social compact, the scorn they can have for the future of the planet, and more. Or so I've heard.
But the uneven temporal and spatial impact of technology qua technology is having its moment again. Your experience of driverless cars is a lot different if you live in the Bay Area or Boston; the quality of your drinking water and the size of your electric bill depends on your proximity to a data center; and so on at ever finer scales, intruding on the neighborhood level, depending on how down your neighbors are with Flock cameras.
This extends into the world of work. Because the capability of artificially intelligent systems is deeply tied to whether or not there are easily quantifiable correct answers available to a question, your economic anxiety is different depending on how closely tied your job is to something like “correctness” rather than (optimistic version) judgment or (realistic version) corporate inertia. Coding is the paradigmatic example in which checkable, correctible answers abound, which is why artificial intelligence is primed to change the daily reality of coding work. Insofar as any given industry utilizes code these days, artificial intelligence looms in all workplaces, albeit unevenly.
There are some people to whom correctness matters even more than it matters to coders, however: mathematicians. When a mathematician brushes up against “correctness,” they have good reason to believe they are doing so in a truly fundamental way. And today’s mathematicians seem to feel like they have recently come under existential threat.
Here’s a question you might not have considered before, but is probably a bit richer than it would seem at first glance: Why is math hard?
Mathematicians and theoretical computer scientists concern themselves with proofs: starting with a small, fixed set of basic axioms and armed with a smattering of Latin phrases (where’s my modus tollens crew at), they build up incontrovertible arguments that have implications far beyond the superficially modest content of the original axioms. But if all math is is proof, and if all a proof does is build upon indisputable axioms in a purely logical way, and if every proof is a question with only two answers (yes or no, true or false), then how can any question be ambiguous or difficult to understand? All you need to do is remember the correct axioms or proofs and apply them in the right way at the right time.
The cognitive and computer scientist Douglas Hofstadter, best known for his concept of “strange loops” as explored in his tome Gödel, Escher, Bach: An Eternal Golden Braid, gave one answer to this question in a 2012 essay, which went lightly viral over the past year. In response to a question from a reader of the journal Mathematics in School about the experience of being a “distinguished mathematician,” he first demurred, protesting his mathematical bona fides. And then he went further, writing of the “traumatic” experience of waking up to his own mathematical inadequacy and limitation. He wrote of “bumping [his] head against [his] abstraction ceiling.” He uses a few more metaphors to get the point across, but I immediately knew the feeling, because, as a pre-predoc, I’d bumped my head hard. At the time, the feeling of being unsure of the truth of some mathematical statement, which I knew other people could perceive and work with, felt akin to a type of personal failure. How did I forget proof A? How did I not realize that implication of proof B? If my ceiling had been higher, I would have seen further, into deeper commonalities with shared structure and more abstraction.
This question can be rephrased with less freighted, less personal language: Why is math not tautology? And what stops us from taking this to the extreme? Why are all mathematical facts not just lying on a frictionless ramp of logic leading from 1 + 1 = 2 (I know, I know: that’s not the first axiom) all the way to the Riemann hypothesis?
If you’re an aspiring mathematician who encounters these thoughts, you have a few options. Obviously, the first and easiest choice is simply to leave math. If you stay, you’re allowed to ignore these foundational issues, as most working mathematicians do. But, if you have a particular type of nerd in you, you’ll dig into the foundations. If you follow this path chronologically, you’ll probably start off by encountering Frege and Russell. You might get to L. E. J. Brouwer, intuitionism, constructivism, and Bourbaki. But at some point, you’ll probably hit Gödel and Turing, and then you’ll likely start thinking about computability.
Computability is the abstraction of computation. Its avatars include the P vs. NP problem, Gödel’s Incompleteness Theorems, Turing’s “Imitation Game,” and many descendants. As a field, computability leads to some deep, thought-provoking questions and to some that, once upon a time, I thought held no interest at all. In particular, I remember learning about computer programs called “proof assistants,” such as Coq (now Rocq). In 2005, Coq (famously!) helped settle the proof of the (notorious!) four-color theorem, after another attempt to use a computer to do so remained stuck in a, shall we say, intermediate epistemic status despite “more than 1,000 hours of computer time” and an announcement to great fanfare in 1976. It’s probably safe to say that the seismic shocks unleashed by that episode are finally reaching the surface of the field:
The math world lit ablaze with equal parts celebration and dismay. One of Appel and Haken’s colleagues, William Tutte of the University of Waterloo in Ontario, rejoiced that they “smote the kraken.” Others despised the thought of computers encroaching on human ingenuity. The affair also posed a philosophical problem in the math community. Does a proof that can’t be verified by humans count as a proof at all?
Still, the whole thing seemed, at the time, a little … dull. Foundations should be all deep philosophical pondering, not infinitesimal tweaks to computer programs!
And yet. Over time, computers have become more broadly capable, and computer-based pure math has been no exception. Its latest and most developed manifestation is a programming language called Lean. By eye, Lean doesn’t look a whole lot different from other programming languages. (You can mess around with it here.) There are types and conditional statements and variables; definitions can be made and reused. The main difference is that with a normal programming language, you write programs that give you outputs in order to automate some repetitive work; in Lean, all you can do is see if the program runs or not. If so, your proof is correct: QED. If not, your proof doesn’t work, try again. The promise—or threat—of Lean has seemed to me to be the realization of the frictionless ramp to the end of logic that would trivialize math. But what would give us the first push over the edge of the ramp?
The key step here was the innocuous “try again” in the last paragraph. The fact that every Lean program is a written artifact with a yes/no answer makes it ideally formatted for AI (and, trust me, I hate that I’m writing what I’m about to write) disruption. The Lean-ification of math may or may not make math any more interesting, and certainly not any more human. Rather, it renders it more efficiently doable by machines.
Since the end of last year, AI chatbots equipped with Lean have produced a stream of proofs of open problems in pure math. At first, when the hype was restricted solely to the predatory capitalist class, it was easy enough to ignore. But to my surprise, the “real” math world seemed ready to embrace the result: I looked at it differently when Terry Tao (the Patrick Mahomes plus LeBron James of modern math) posted about it. At the time, I still detected a bit of a raised eyebrow in most of what I read: “yes, I guess it’s cool”, they seemed to be saying, “but here’s why it’s still at arm’s length from what I’m actually doing inside my gourd all day.” The questions at hand seemed a bit obscure, and the results didn’t have big implications for any significant vein of literature.
The raised eyebrow is now knitted. An OpenAI paper and accompanying Lean proofs from early August, entitled “Ten Advances in Mathematics and Theoretical Computer Science,” followed closely by a new result from Anthropic, have kicked up a much bigger stir, all of which is sure to be dwarfed by the announcement that a Millenium Prize has been nabbed. Although these results have not been fully metabolized by the community, the reaction makes it clear to me that what is happening now hits much closer to what most mathematicians consider their core work. Wild extrapolations of the future of math have abounded as refuseniks preach rejectionism and other, more measured, approaches are suggested.
My favorite skeptical take is from Tobias Osborne, referencing the Bible by way of the title of the reclusive mathematician Alexander Grothendieck’s quasi-mystical memoir Reapings and Sowings. He points out that each of the final human-legible results fits within a single chat session’s context window. The conclusion is that these results are in some sense cherry-picked, and the implication is that what we are seeing now is AI models bumping up against their own current ceiling.
The question that would keep me up at night if I was a working mathematician: Is the raising of that artificial ceiling from last winter to now merely illusory? Or is it real and will it continue apace? And if it does, are there any other significant barriers between now and the end of math? Because regardless of whether or not the right prompts ever got entered to manifest Lean’s thumbs up or down of my pet theory, and whether or not that given logical sequence could become knowable in human terms, and whether or not it was all a stunt to drive pre-IPO hype for a clown car full of extractive capitalist ghouls, the fact that all it took was chatting with a bot to know the answer would kill my interest in turning coffee into theorems.
Among the most admirable things about mathematics as a field is that high-quality conjectures are valued nearly as much as high-quality proofs. In effect, throwing up your hands and saying “I think this is the answer to this question, but I’m really not sure” is understood to be a vital part of how the field moves forward. These are the “sowings” alluded to by Grothendieck and Osborne, and they perform roughly the function that real-world inputs play in other sciences, like “diseases” for medicine, “experiments” for biology or physics, “astronomy” for astrophysics, and so on. Conjectures give not merely questions to answer, but hints born of experience that act as directions for the field to orient around, goals to strive towards. Famous open-ended mathematical musings like Fermat’s Last Theorem (whose name I think is 2/3 as incorrect as Voltaire thought “Holy Roman Empire” was) or the Riemann Hypothesis have driven mathematical research for centuries. The 23 “Hilbert problems” more or less demarcated the boundaries of serious math research for the entire 20th century; the Clay Millenium prize problems were intended to do the same for the 21st. Say what you will about AI bots writing barely intelligible proofs: they aren’t writing conjectures at all.
So is this the end? Will AI math remove the oxygen from the seminar room and suffocate human ingenuity entirely? Or have rumors of math’s demise been greatly exaggerated? If one thing is clear, it’s that different fields are differently predisposed to getting AI-ed. The future is here, but because it’s so unevenly distributed, it’s not really the future.
The frictionless ramp which I feared as a prospective mathematician, and which the roller coaster cart of pure math now seems to be nearing the crest of, could also be described as a slippery slope. Slippery slope arguments are, always, incomplete: they substitute fear in the place of a critical explanatory step. It’s easy to be vaguely scared of what could happen without saying precisely how. So let me give one particular prognostication of a future for math in light of these recent developments.
The predecessor of what we might call the “conjecture era” we’re now in was the system of patronage, in which mathematics was but one of several baubles the powerful could hoard. I can imagine a re-closing of the workings of knowledge, where the locus of knowledge-making shifts from public, open, collectively (if imperfectly) funded grants to private, closed, quixotically personal discovery labs either inside the biggest tech firms or in small startups that get acquired or shadily co-owned. This will further devastate universities and continue to eat away at the “soft money” edifice they rely on. The resulting not-quite-academic findings will be leased back to us at profit, or held closely, developed in secret, and revealed as barely comprehensible jewels of arcana that, like Renaissance mathematicians at court, lend a bit of stature, a dash of rivalry, some injections of cash, and the imprimatur of legitimacy to the shadier primary activities of the companies. Anything that is old can be new again.
Similar to Hofstadter’s Gödel, Escher, Bach, Imre Lakatos uses a heavily footnoted form of dialogue in his Proofs and Refutations as a way to address heady concepts indirectly. In a footnote in the chapter on “Concept-Formation,” he remarks:
Quite a few mathematicians cannot distinguish the trivial from the non-trivial. This is especially awkward when a lack of feeling for relevance is coupled with the illusion that one can construct a perfectly complete formula that covers all conceivable cases.
There are no completely closed systems. All of what anyone does is human, and as such, humanistic. Even Lean is fallible: bugs can lead to ambiguities, and “trust” and “belief” are words that get tossed around when discussing it. The point is not that this is bad. The point is that this is not new, or really even all that different. Mathematicians, here are your accordions.
