Alexander Gamburd circulated the first version of his essay “The Siren Call of Silicon Leviathan” in mid-September, acknowledging with implicit regret that it was “probably way too long to be posted (e.g. on your substack).” An even longer version — 26 pages, plus an additional 40 pages of endnotes! — has now been posted on arXiv. Everyone who has an opinion about the the subject of this newsletter should read it. It is not light reading, especially if you decide (as I recommend) not to skip the endnotes, but to my mind it is one of the two most thoughtful essays anyone has written to draw out the implications of AI for mathematics, the other one being “The fall of the theorem economy” by David Bessis.
Gamburd argues, with ingenious metaphors and drawing on an astounding range of references,1 that “Mathematics was central to the enlightenment” because it created “knowledge that compels assent without appeal to authority, that is the same for the peasant and the prince, that any human being with patience may verify.” This argument is developed in the excerpt copied below. The flip side is that the application of AI to mathematics undoes the work of the enlightenment:
Mathematics once more contains truths that exceed all the ability of human reason and are held on authority; the authority is the Lean proof checker and the corporation that owns the prover; the clergy are those who can put questions to the prover and interpret what it returns, the corporation’s mathematicians first; the language the laity cannot read is not Latin but Lean.
(To avoid misattribution, I have chosen to reproduce passages from Gamburd’s text in blue, here and below.) Gamburd distinguishes demonstration from certificate: the corporations, possessed of “subhuman superintelligence,” provide the latter but only a humanly comprehensible proof counts as a demonstation.
A certificate is a document: it informs us, reliably, that a monument exists, and that is all. The Lean proof of 8 September is a document 616,000 lines long about a monument no one has visited. We may believe the document. But a civilization whose knowledge consists of documents about monuments it does not visit has ceased, on Panofsky’s definition and on Hobbes’s, to be a humanist civilization, whatever the state of its certainties.
But press releases about mathematics are now central to the prestige of the frontier labs, and Gamburd concludes that this gives mathematics a surprising power in the last instance:
The [mathematical] community’s sword is the one this essay has already drawn, acceptance withheld; it is a bloodless sword, and it is the only one the Leviathans2 cannot forge for themselves, since it is the thing they compete for.
The history of ideas began a long time ago
When the panelists at the Heidelberg Laureate Forum were asked “What general career advice would you give to a beginning Ph.D. student, in view of AI?,” my answer included the following two items:
study philosophy to avoid being swayed by spurious arguments and sensationalist predictions, all of which misrepresent the nature and aims of mathematics as a social practice;
study social science and the humanities so you can recognize how language is used to discourage resistance; note in particular the similarities between the rhetoric about the inevitability of an AI takeover of mathematics and the 19th century rhetoric of progress that accompanied colonialism.
I should have added that issues very much like those raised by the arrival of AI in mathematics have been addressed repeatedly in the long history of reflection upon the human condition. Whether or not you agree with Gamburd’s text, its great merit is to demonstrate how the the debate can be clarified — enlightened — by restoring it to its proper place as a chapter in the history of ideas.
For example, Po-Shen Loh’s essay “Why Do We Need Human Mathematicians Anymore?” published on the author’s blog and as a guest post on Terence Tao’s (widely-read) blog, is an admirable attempt to answer the question in the title. But it makes the mistake, all too common when mathematicians grapple with ethical or epistemological or aesthetic questions, of forgetting that similar questions have occupied human minds, in every literate culture, for thousands of years.
And whether or not Daniel Litt is correct when he claims that
As we think about how to reshape our profession, it’s important to understand that, whether one likes it or not, it’s impossible to stop people, amateur or professional, from pushing a button to produce mathematics. The idea that we will persuade people not to play around with math, or that we will be able to “reserve” problems for graduate students, is just not realistic.
he owes it to his readers to remember that the question — whether or not human beings are so incorrigible that it is impossible to stop some of them from defying community norms — has been the subject of energetic and extensive reflection, notably reflection on how to create a stable form of government that respects accepted principles of justice. One need look no further than the Federalist Papers 6, in which Alexander Hamilton asked
Has it not… invariably been found that momentary passions, and immediate interest, have a more active and imperious control over human conduct than general or remote considerations of policy, utility or justice?
or the Federalist Papers 51, with James Madison’s famous line:
If angels were to govern men, neither external nor internal controls on government would be necessary.
Gamburd’s erudition is exceptional, but everyone who wants to share their sensible ideas should first remind themselves that it is almost certain that generations of thinkers have come up repeatedly with the same ideas, and others have refuted them, and that contributing to a debate on pressing issues means acknowledging what these past generations have contributed and debating them as well.3
Section I of Gamburd’s essay: Mathematics and the Enlightenment
Mathematics was central to the Enlightenment, which took off as a fledgling startup with the Principia, the demonstration that a handful of propositions governed the apple and the moon alike: Fontenelle drew the moral that l’esprit géométrique was not so attached to geometry that it could not be carried into other kinds of knowledge. D’Alembert made the mathematical sciences the only ones “marked with the seal of evidence” and graded every other discipline by its distance from them; Kant held that a doctrine of nature contained exactly as much science as it contained mathematics; and Condorcet proposed a mathématique sociale.
But the deepest of mathematics’ services to the Enlightenment unicorn—the one that yielded spectacular returns indeed—was neither doctrinal nor methodological. Mathematics was the proof of concept, the demonstration that what the Enlightenment wanted was possible at all: knowledge that compels assent without appeal to authority, that is the same for the peasant and the prince, that any human being with patience may verify. It did not have to be invented by the founders; it already existed, for a geometrical demonstration is a truth that owes nothing to whoever asserts it. Locke recommended mathematics “not so much to make them mathe- maticians as to make them reasonable creatures,” and the phrase tells us what a reasonable creature was: someone who would not take the forty-seventh proposition on Euclid’s word, but would follow it back until the impossible became necessary. There were no mysteries in Euclid beyond the reach of human reason; that was the point the Enlightenment made of Euclid. Mathematics was, strictly speaking, not the Enlightenment’s proof of concept but its existence proof: it did not show that autonomous reason might work; it exhibited an instance. That is why one might say that the Enlightenment—in effect—bound itself to the mast of its firstborn, and why the ship of mathematics entering thoroughly turbulent waters threatens the Enlightenment project, potentially in its totality.
The converse is less familiar but no less pertinent: it was the Enlightenment that made math- ematics as we now know it. Until the Enlightenment the subject was, at its frontier, a private and often a courtly art. Tartaglia surrendered the solution of the cubic to Cardano only un- der oath; Newton sent the method of fluxions to Leibniz as an anagram; the Bernoullis issued challenge problems as one issues a challenge to a duel; a result was property, and property was defended by concealment. The Enlightenment turned that private possession into pub- lic reason. The academies and the journals made publication rather than possession the act by which a result came into existence; priority went to whoever printed first; credit attached to a name anyone could cite; the demonstration was addressed to an anonymous reader presumed competent. André Weil, opening the Euler chapter of his history of number theory, marks the change. Until the latter part of the seventeenth century mathematics “had sometimes bestowed high reputation upon its adepts but had seldom provided them with the means to social ad- vancement and honorable employment,” and its results traveled through “a private network of informants”; then, “by the time of Euler’s birth in 1707, a radical change had taken place,” and “scientific life, by the turn of the century, had acquired a structure not too different from what we witness to-day.” Euler wrote eight hundred papers to be read, and the Letters to a German Princess—no less than Descartes’s letters to Elisabeth of Bohemia a century before— to be followed by a princess. The same century made mathematics an instrument of social advancement—the École Polytechnique admitted by examination, and Fourier the tailor’s son, d’Alembert the foundling and Monge the pedlar’s son had shown what the subject could do for those without high birth, though not yet for those without the right sex, for Sophie Germain followed Lagrange’s course there from its lecture notes under a man’s name—and it fixed the modern standard of rigor. Cauchy’s Cours d’analyse of 1821 was a Polytechnique course, and Grabiner has argued that its rigor was in part a consequence of teaching: a working analyst could rely on a trained sense of when a series converged or a limit existed, but that sense cannot be lectured to a hall of students, and what can be lectured is a definition that decides every case and a proof that uses nothing else. Rigor is tact made teachable, and the École had to teach. Lagrange, lecturing at the same school a generation earlier, had founded the calculus on power series in the Théorie des fonctions analytiques; Cauchy’s limits replaced them.
The norms of the mathematics we practice—preprints accessible to all, credit by citation, publication necessitating refereeing by peers, and thereby (and only thus) establishing priority (a practice given its definitive modern form by Lamb’s teacher Stokes, during thirty-one years as Secretary of the Royal Society and editor of its Transactions), understanding as the end and proof as the means—are not artifacts of lex naturalis but Enlightenment institutions. Publication used to discharge three functions at once—announcing a result, identifying its contributors, and demonstrating understanding—which had never needed to be distinguished, because for three centuries the capability of producing a deep theorem was vested in a human mind that had understood it. The mathematical community is a tiny, open, unarmed and (by and large) honorable republic—a province of what d’Alembert called the Republic of Letters—that publishes everything in advance, without promise of remuneration; not from naïveté, but because its whole constitution—as well as its raison d’être—was the abolition of walls.
This two-edged contention—that mathematics was the Enlightenment’s existence proof of concept, and that the Enlightenment was the maker of mathematics as we now know it—goes a long way towards explaining why the decisive engagement between the frontier models and the learned world took place in mathematics rather than in ________, where the money is. A theorem in Lean either passes the proof checker or does not, so mathematics is the one irre- placeably consequential domain of human knowledge in which a machine can be told, at scale and without a human judge, whether it has succeeded: in the trainers’ own jargon, the do- main of verifiable rewards, the verdict that elsewhere must be bought from human graders being here supplied by the proof checker at no cost; and mathematics is transacted entirely in text, so its whole frontier is reachable through nothing but tokens (the esprit géométrique thereby submerged). But the deepest reason is the Enlightenment’s own doing: it had agreed to regard mathematics as reason’s home, and a machine that computes proves its claim to reason most convincingly there. From Turing’s chess to Go to the IMO, the proxies for machine intelligence have been formal games, and mathematics is perceived as the oldest of them, the one Hobbes meant by “Reckoning.” When the machines began to solve olympiad problems, Jacob Tsimerman put a question to his Doktorvater, Peter Sarnak, who had observed that this told more about the competitions than about the machines: “What level does the AI need to perform at before you take it seriously? What would it need to do? When would you change your mind?” This essay attempts to unravel the answer that 8 September appears to have given. The Millennium million is small change, and so is whatever was spent to claim it; what really was at stake was the relative standing of the two powers that contend for the title of this essay, and the episode was less about advancing mathematics than about being seen to have done so. To be seen to do mathematics is to be seen to think. One may view the open literature of this section as a commons, and the frontier models as its enclosure. The first consequence is already visible: that mathematicians may come to guard their work in order to keep it from being taken. That is the road back to Tartaglia, and a Middle Ages in reverse—Panofsky’s phrase from my epigraph, whose meaning section IV takes up—is likely to affect the sociology of the subject before reaching its epistemology. Simone Weil held that the three monsters of contemporary civilization are “Money, mechanisation, algebra,” and the Silicon Leviathan is the point at which the three become one body. The Leviathan of Job lived in one of the four classical elements. The Silicon Leviathan lives in a fifth, and Weil put it first on her list.
Bloodless swords
Gamburd’s suggestion that the mathematical community could withhold its acceptance of the results issued by the AI labs — meaning refusing to acknowledge them as valid contributions to the mathematical literature, was anticipated by Terence Tao’s introduction of the notion of canonicalization in his public lecture at the International Congress of Mathematicians in Philadelphia. Tao may or may not have borrowed the word from computer science but he gives it a precise meaning in the text based on his lecture:
Key results should ultimately become part of the definitive textbooks and reference material of their subject, in the form in which they are taught to the next generation of students. This process of canonicalization — in which a result is restated in its natural generality, given its right proof rather than its first proof, connected to its neighbors, and absorbed into the standard toolkit — is the slowest stage of all. It requires broad, deliberative consensus, and it is the stage least amenable to optimization by AI tools. It is also, in my view, the most valuable part of the entire process.
More recently, Stepan Nesterov, a graduate student at Stanford, proposed a definition of proof on the site Proofs and Prompts that, suitably interpreted,4 looks like the only one compatible with canonicalization, and that corresponds to what working mathematicians have meant in practice by proof, until formalization became fashionable:
Definition. A mathematical proof is a text in natural language which explains to a person sufficiently well-trained in mathematics why a certain statement is correct. A statement is mathematically proven, if there is a mathematical proof which is accepted to be correct by sufficiently many well-respected members of the mathematical community.
More officially, the Advisory Group on Mathematics and Artificial Intelligence (AGMAI), which “came together after OpenAI approached some of its members about establishing an external advisory board” but chose instead to remain strictly independent of the industry, issued its first guidelines yesterday for “responsible release of AI-generated mathematics.” The nine members of AGMAI begin by making clear that
we do not endorse [what the industry is doing], and we ask [AI labs] to stop testing advanced mathematical problems on proprietary models.
But since they know the industry will continue doing so anyway, they state conditions under which AI-generated mathematics might be considered compatible with community norms. Moreover, they ask the labs “to make an appropriate [financial] contribution to fulfilling their responsibility towards the development of human understanding of their AI output,” although they stipulate that “acceptance of such support by the mathematical community would not be conferring legitimacy on the practices of the AI labs.” This group of mathematicians, at least, is unwilling to forge the sword for which the Leviathans compete.