The judge placed his hands on the ground. He looked at his inquisitor. This is my claim, he said. And yet everywhere upon it are pockets of autonomous life. Autonomous. In order for it to be mine nothing must be permitted to occur upon it save by my dispensation.…
(Cormac McCarthy, Blood Meridian)
Translation
One difference between mathematics and poetry, I have already argued, is that the former passes efficiently and apparently without ambiguity between languages, whereas translation of poetry is notoriously difficult and imprecise. This observation strongly supports the thesis that the content of a mathematical statement is independent of the natural language in which it is expressed, which in turn makes the formalization program more plausible.
Contemporary formal languages for mathematics (Coq, Lean, Isabelle, etc.) are high-level in the sense that their vocabulary includes comprehensible words from natural language. This represents a marked improvement on impoverished and purely symbolic systems, like the one Russell and Whitehead popularized [sic] in Principia Mathematica. However, existing formal languages for mathematics have the drawback that they reinforce the English language’s arbitrary and increasingly unjustified world domination. As a compromise between phonetic, pictographic, and symbolic languages, I propose that henceforward mathematical text be written in emojis. The string of emojis at the top of this page is a translation of a familiar theorem into the Google Noto Color Emoji set. (I hesitated between the Google and Apple emoji languages, and even toyed with Microsoft Word icons, but since Google has taken a special interest in the mechanization of mathematics they seem to be the safest choice.)
Logical deduction would proceed by applying appropriate smiley substitution rules, to be developed in consultation with Google’s engineers.
Do you recognize the theorem? Of course it is Hilbert’s Basis Theorem, stated in its contemporary form:
If R is a noetherian ring, then the polynomial ring R[X] is a noetherian ring.
The “If” at the beginning is superfluous and has been dropped, but there’s a thumbs up sign at the end to signify that the statement is complete.
We’ll see below that this was not an innocent choice of theorem to launch my modest proposal to rewrite all of mathematics in a universally familiar visual medium that is politically and culturally neutral as well as fun. Even if the mathematical community rejects my initiative, I hope readers will spend a few minutes imagining their immersion in a virtual world in which mathematical statements are apprehended instantaneously without mediation by language. They will then have a better idea of how it feels to be a robot, and they will be in a better mood to read the remainder of this week’s anniversary entry.
Anniversary blues
This installment marks the first anniversary of this newsletter, and it’s time to take stock of what it has accomplished in its first year. It’s an understatement to say that it has failed to live up to most of the ambitions I announced for it in its pilot episode. It’s true, I can take some satisfaction in having produced a regular stream of 3000+ word texts roughly on schedule. But I have failed — and this is what disappoints me most — to devote any serious attention to
exploring the reasons for the absence of any sustained discussion of these issues1 on the part of mathematicians, in contrast to the very visible public debate about the perils and promises of AI.
At least I was not deluded enough to think that my newsletter would make history by stimulating the beginning of such a discussion. A more realistic ambition would have been to shake the hold on the imaginations of a few mathematicians, as well as many philosophers and computer scientists, of the Central Dogma of Mathematical Formalism, which, in the version one can read in M. Ganesalingam’s 2009 thesis, asserts that
…when mathematicians are writing modern mathematics in a formal register, they intend to formulate meaningful statements in some underlying logic. If it was pointed out that a particular sentence had no translation into such a logic, a mathematician would genuinely feel that they had been insufficiently precise. (The actual translation into logic is never performed, because it is exceptionally laborious; but the possibility of the translation is held to be crucial.2) Thus mathematics has a normative notion of what its content should look like…
It occurs to me now that my chances of affecting attitudes would be greater (though still slim) if I were to offer an alternative reading. Here it is, the first of five numbered attempts to articulate what (I think) I actually believe:
1. The Central Dogma is a rational reconstruction, on the part of philosophers, of the norms of mathematical practice.
Here “rational reconstruction” means roughly what it did in Lakatos’s ironic sentence—
…actual history is frequently a caricature of its rational reconstructions…
—with the caveat that Lakatos was referring to the methodology of historians of science whereas I have in mind the philosophers’ drive to read whatever they observe as if it were rational.
This can almost be taken as a definition of rationality — whatever can fit as a fragment of philosophical discourse — provided you remember that all meaningful philosophical assertions are destined to be proved wrong. My alternative reading, in this light, is just an empirical observation: it’s philosophers who have been peddling the Central Dogma as a philosophical thesis, and not merely a methodological norm as in Hilbert’s Program or the Bourbaki project.
Critical thinking
Since a meaningless observation like my point 1 cannot be proved wrong, my alternative reading is not a philosophical assertion. But it can still serve as the point of departure for critical thinking. This does not consist merely in thinking critically within the frame defined by a question. Critical thinking, in the sense of Kant’s three Critiques, means questioning the question’s presuppositions.3
To engage critically with the project to mechanize mathematics, for example, it is not enough to toss one more idle opinion into the pot. Rather than asserting a thesis or a dogma, critical thinking asks questions like: how would one go about determining whether or not this rational reconstruction is accurate? or: are the philosophers right to attempt any rational reconstruction of mathematics?
Simply denying the prevailing opinion doesn’t count as critical thinking either. Airy claims that I’ve heard from some of my colleagues, for example, to the effect that the AI industry can never eliminate human mathematics, are silly as well as historically naive. I recently finished a book called Le yiddishland révolutionnaire, part of the history of the last chapter in the story of a culturally and linguistically unified community that came into being over many centuries and occupied a substantial portion of Central and Eastern Europe but was effectively wiped out in the space of barely ten years. We are currently witnessing the demonstration that it is technically possible to eliminate a political unit the size of Ukraine from the map, along with its population.
Sophisticated thinkers are already contemplating the elimination of entire populations of scholars, far more fragile than countries and poorly fortified. Witness this elegiac, or perhaps lugubrious, poem by Scott Aaronson:
…if the “insights” on which you pride yourself are impersonal, generalizable,
Then fear obsolescence as would a nineteenth-century coachman or seamstress.
From earliest childhood, those of us born good at math and such told ourselves a lie:
That while the tall, the beautiful, the strong, the socially adept might beat us in the external world of appearances,
Nevertheless, we beat them in the inner sanctum of truth, where it counts.
Turns out that anyplace you can beat or be beaten wasn’t the inner sanctum at all, but just another antechamber,
And the rising tide of the learning machines will flood them all,…
So should we fear obsolescence? Will AI flood our cozy antechamber? These are legitimate questions, but posing them only rises to the level of critical thinking when it begins to address the means by which such an apocalypse may come about. That means realizing that the future of mathematics is a political question and that it will be determined by relations of power.
Power
Even mentioning that the continued material existence of mathematical research is conditioned by power relations usually brings on accusations of paranoia, although it’s generally understood that the funding model of universities and research institutes in most countries is highly unstable and that in all countries choosing how to apportion funds is and always has been one of the primary prerogatives of power. The same colleagues who promote formalization to safeguard the rationality of mathematics must implicitly assume that, if and when our professional priorities diverge from those of our corporate benefactors, government funding agencies and private philanthropy will side with us rather than with the
accountancy-driven compression of human potential within a global interlock of power, money, mechanization, and mass media.4
I fall into a fit of cognitive dissonance when I try to reconcile the irrationality of this assumption with the rationalism that ostensibly motivates the mechanization project. Here is Farhad Manjoo’s recent mea culpa for his early “failure to seriously consider the implications of an invention” — in his case Facebook — “as it becomes entrenched in society”:
It does not seem in any way good for society — for the economy, for politics, for a basic sense of equality — that a handful of hundred-billion-dollar or even trillion-dollar companies should control such large swathes of the internet.
This problem, the tech behemoths’ power, was fostered in the Obama administration. It’s a direct result of the vibe I describe — the feeling that tech people knew what they were doing, that they were the good guys, that their inventions were going to save the day.
(Farhad Manjoo, “I was wrong about Facebook”)
Now I want to stress that I am quoting Manjoo not because I claim that mathematicians participating in the mechanization projects have been duped by the Silicon Valley ideology, or are trojan horses for a tech industry takeover of our beloved vocation, much less that “formalizers need to sacrifice children to AI beings during their satanic masses.” Rather
2. Given the intense interest “tech behemoths” like Google as well as crypto billionaires are directing at mechanization of mathematics, colleagues should at least acknowledge that the power-wielders’ plans for mathematics and ours are probably not perfectly aligned, and that the possibility that in many respects these plans may be diametrically opposed deserves to be taken seriously.
I suspect that many colleagues dismiss concern with the material conditions of our vocation because they prefer to see mathematics as subject to a Nietzschean will to power:
…the man who sets himself the task of singling out the thread of order from the tapestry will by the decision alone have taken charge of the world and it is only by such taking charge that he will … dictate the terms of his own fate. (McCarthy, Blood Meridian)
For the judge, speaking these words in McCarthy’s book, “taking charge” is incompatible with freedom:
The freedom of birds is an insult to me. I’d have them all in zoos.
This attitude is perfectly suited to the Silicon Valley ethos, not to mention their business model; it is an avatar of thanatos, and is the impulse I spy behind the Central Dogma.
History is a nightmare from which some colleagues think they have awakened
I don’t claim any expertise in the history of mathematics, but I do get impatient when, after colleagues express their opinions about mechanization, often vehemently, they show no interest when I remind them that the opinions that they thought were so original have not only been formulated but have been debated and contrasted with other opinions and are part of a historical process of evolution, etc. etc. The lack of interest in history is characteristic of mathematics’s irrepressible optimism, the conviction that future mathematics will inevitably be better than what we know now, so why dwell on the past? This attitude is undeniably productive in its original setting5 but is unhelpful in clarifying how change actually takes place.
This is why the formalizers’ rhetoric is largely based on a simplistic notion of progress, sustained by a low-level (and largely rhetorical) adherence to the Central Dogma. There’s no doubt that interest in mechanization is growing, especially among younger mathematicians, and that this is due largely to the perception that the various research programs associated with mechanization have been successful. But perception of success, and the effectiveness of rhetoric, are also effects of power! What Silicon Reckoner has not (yet?) explored adequately is precisely
3. How are these effects of power produced in practice; what is the role of institutions, the media, and funding decisions in promoting these perceptions and this rhetoric?
It has not been treated adequately here precisely because I am not a historian and therefore am not qualified to carry out the research. Anecdotes that have been shared with me suggest, for example, that the NSF has been actively nudging even prominent specialists in the direction of mechanization. But even if I had the time to follow up on these leads I would lack the professional qualifications to make historical sense of them.
Conventional history of mathematics largely traces the boundaries of legitimate exercise of power, but mainly obscures the role of power relations. Instead it relates how good ideas are displaced by better ideas. Several colleagues who should know better dismiss young historians of mathematics as “idiots” because they remind us that the history of mathematics, like any other branch of history, is driven by power relations. These colleagues make the natural6 mistake of confusing power with abuse of power, or with brute force. Hiring decisions, editorial decisions, prize committees, prestigious invitations, and so on rarely involve violence. They don’t have to be abusive, nor do they have to rely on old-boy networks, in order to be exercises of power. If they are effective they are exercises of power by definition.
Translation and Progress
Hilbert’s Basis Theorem, transcribed at the top of this post into culturally neutral (?) emojis, is doubly relevant to the themes of this anniversary edition. Kevin Buzzard reported his surprise when Lean rejected his first attempt to formalize the usual proof because he7 failed to specify that R is not the zero ring.8 More momentously, just this Theorem “became the paradigm of modern axiomatic mathematics,” according to Colin McLarty,9
an origin myth, a titanomachy where new gods defeat the old
The “narrative at its barest bones,” which climaxes with Paul Gordan’s exclamation upon learning that Hilbert’s proof had made his life’s work obsolete —
This is Theology, not Mathematics!
— points to where translation, in this case from Gordan’s problem of constructing polynomial invariants to the emerging formalism of abstract algebra, is emblematic of progress.
I prefer to eschew reference to “progress” as long as the word remains imprisoned in a Silicon Valley gilded cage, and one of the aims of Silicon Reckoner has been
4. To convince colleagues to avoid using words like “progress” unreflectively, especially when discussing mechanization.
But clearly something happened to mathematics when abstract algebra became the default formalism for questions like those about invariants. Abstract algebra, as developed by Noether and van der Waerden, and then Bourbaki, was the native language in which I learned algebraic geometry and algebraic number theory, and returning to pre-Hilbert ways of thinking requires a real effort. We can rejoice in the mathematical landscape that these developments opened up without, however, using the language of progress. McLarty is not averse to the word but he does not characterize Hilbert as “progress” over Gordan.
McLarty’s deep and thoughtful study of the creation of a paradigm brilliantly illustrates the kind of critical thinking that is precisely what has been absent from current debates over the “approaching obsolescence” threatened by “the coming mechanization of mathematics.” I know of one notable exception: an essay by Akshay Venkatesh whose original title included the two expressions quoted in the previous sentence. Venkatesh compares the approaching role of machines in mathematics to the period highlighted by McLarty and deduces that the coming paradigm shift will be much more radical:
Post-mechanization mathematics may look to us as modern mathematics might impress those working a century ago, but I think this does not go far enough. The impact of [Venkatesh’s hypothetical mechanical assistant] on mathematical cognition may be much greater than the passage of a hundred years. To find a suitable parallel for this effect on our thought process, we might consider, for example, the introduction of algebraic notation in mathematics.10
A future post will be devoted to Venkatesh’s insights and to the debate they will be inspiring at the October Fields Medal symposium planned in Venkatesh’s honor. I want to leave readers with a thought about one more example of translation. For some reason Wiles’s proof of Fermat’s Last Theorem has been the formalizers’ white whale, practically since it was announced. I wrote above that nothing happens when Hilbert’s Basis Theorem is translated from German to English or to emojis; and I submit that, whatever is happening when a human proof is translated into a Lean proof, it is generally not the sort of thing11 that would be qualified as “progress” from the purely mathematical standpoint. For reasons I have explained elsewhere, I can’t imagine anything interesting happening when and if someone translates the proof in Wiles’s version (or any of the subsequent versions) into Lean. But I equally can’t imagine that anyone who is informed about the subject would deny that something interesting happened when Frey, Serre, and Ribet translated Fermat’s Last Theorem into a question about modular forms. So here is a question to be explored:
5. What is the difference between the two kinds of translation?
The iniquity of oblivion
If so many of my colleagues are ready to contemplate the obsolescence of our profession, amid “the rising tide of the learning machines,” I suspect it’s because they are acutely conscious of their own rapidly approaching expiry dates. Like Gordan’s calculations of invariants after Hilbert proved his theorem, their life’s work is destined to be declared éculé et pisseux, to use Bourbaki’s expression,12 by the very generation whose induction into the profession they oversaw, and who now snicker at their obsolescence behind their backs or even to their faces.
I myself know only too well how translation and retranslation ceaselessly wipes forebears’ slates clean. For the last 10 years I have strained to climb out of Peter Scholze’s wastebasket, switching fields frantically, but inevitably cast down like Sisyphus to the bottom, as Scholze tosses over the rim yet another translation of a notion I thought I knew well — in some cases having even contributing to its invention — now restated in a language I can only understand, if at all, at the end of a lengthy struggle. And what reward do I reap for my struggle, if not an invitation to an unsteady berth on a cruise ship, unwelcome in any harbor, reserved for the éculé et pisseux?
…you should be careful, hundreds of young people perfectly understand the math that is in your article and they clearly see that you don't know the subject (the referee included). If I were you I would concentrate on cool projects that I like and, quietly, without putting pressure on myself, I would take the opportunity to please myself rather than trying to have who knows how many projects at the same time. Since you’re reached a certain age and a certain level in the mathematical community, you might as well take advantage of it :)
This message (Google-translated from the original language, to conceal its author’s nationality) was just such an invitation. But I choose to read it not as a victory for thanatos, whatever its implications for my own mortality, but rather as a manifestation of eros, of the irrepressible vitality of human mathematics, its organic striving for constant renewal as a medium of self-expression and self-fulfillment.
What robot would send such a message to its trainer?13
Serendipity
Silicon Reckoner can be read as an extended paean to serendipity, a poem in blank verse demonstrating that Gayatri Spivak’s maxim — that “the digital will never capture the contingent” — is as true of mathematics as of literature. At least I can be satisfied that the newsletter’s first year has not been short of illustrations of this principle. Here I was about to conclude this week’s episode with a true story of serendipity, of which I learned just last week, that radically transformed my own field. But Substack has just warned me that I am “Near email length limit,” so I will save the anecdote for a future essay, and this anniversary edition will end on a note of serendipitous fragmentation.
And after just over one year, having published 3 news flashes as well as 26 essays, Silicon Reckoner will be taking off the month of August. Since my initial plan to invite readers to submit comments to the Mathematics without Apologies blog met with little interest, I will be gradually activating comments on Silicon Reckoner posts, starting with this one. If comments have been activated on a post, the speech bubble icon at the top will link to a page where you can write what you think. Eventually they will all be activated — individually, , since I haven’t figured out how to activate them all at once. The advantage of the Wordpress blog was that I can filter them before publication, rather than afterwards, as is the case here. We’ll see how that works out.
That is, those connected with the “still largely hypothetical AI future of mathematics.”
Emphasis added to indicate where evidence is sorely lacking.
Elif Batuman provides a startling illustration of critical thinking about “politics” in her reaction to the U.S. Supreme Court’s overturning of Roe v. Wade. “I now know that there is nothing more political than the depoliticisation of the lives of women and children.”
Julian Bell, An Impulse Heard Round the World, NY Review of Books, May 26, 2022.
Though the road to future mathematics often begins with a return to sources, for example when Griffiths “ha[d] a look at a paper of Poincaré.”
Natural because they are not in the habit of critical thinking.
Kevin, that is, not Lean, who has not indicated a choice of pronouns.
See this presentation, pp. 40-43.
Here is the link to the published version of McLarty’s essay.
Venkatesh’s essay is concerned with “mathematical cognition” rather than our material circumstances. Although the words “university” and “laboratory” do not appear in the text, they are implicitly included among the “mechanisms that influence the construction of value” and he writes
We shall assume these mechanisms will evolve slowly in relationship to the
transition we want to study, and so we will not discuss them. This is clearly not
entirely realistic…
I am aware that some serious mathematicians have claimed that the practice of formalization has led to new insight into their field, and I even promised in an early installment to take up the question of when this might happen to me. One more promise that has yet to be kept.
So, at least I have been told. The only documentary evidence I’ve found online is in this chapter by Grothendieck from SGA 7, and the citation gives no sense of the cruel work of history, of the “iniquity of oblivion,” in the words of Thomas Browne.
The letter contains the key to what makes mathematics a vocation, and not a job, unlike that of Aaronson’s “coachman or seamstress” or of today’s long-distance trucker. "Seamstress” is actually a poor choice for Aaronson. We had a friend and neighbor in Paris who had a faitful clientèle as a seamstress. If she hadn’t reached retirement age she could have gone on indefinitely, or at least as long as there are humans to wear clothes. But we’ll have to return to this later.
Thank you for your comment and for the link to your essay. I'm not sure where our agreement is "violent"; I am much less keen than you on Frege, but that remains to be developed. Thank you for quoting me. I have some serious complaints about the way I was quoted in that Quanta article, outlined at https://mathematicswithoutapologies.wordpress.com/2020/09/01/the-inevitable-questions-about-automated-theorem-proving/; my continuing frustration with Quanta was one of the factors that led me to start Silicon Reckoner.
It's generous of you to say that I've triggered a discussion, but I haven't seen much evidence that this is the case. I hope more people who disagree with the hype, or propaganda, will speak up. I particularly appreciate section 6 of your essay, but when you write about "meaning" and that "There is no audience besides the audience of mathematicians," you have to bear in mind that much of the ethos of the mechanization project is already post-human and its most energetic protagonists are probably past being convinced.
I stumbled on your blog and then followed to this substack. Thank you for your very thoughtful article. I must admit that (like many fellow mathematicians) that I don't have much patience for philosophy and history of mathematics, but I do share your reservation about formalization of mathematics, on a narrower ground.
In my view, there is a long history of computer scientists and tech evangelists to oversell the value of automation. Inevitably, some comparison to basic tools like printing press or steam engine is made. However, computer automation has only changed the way we work, often not for the better. Even in the programmers' own domain, a new programming language is invented every month promising to raise programmers' productivity drastically. Needless to say none achieves that goal since new ones keep appearing. I think it's possible that the formalizers end up in a similar conundrum as the programmers, that a large amount of time is spent on satisfying the compiler instead of thinking about mathematics. If referring to someone else's theorem works similarly to importing a library in programming, I don't really envy a mathematician who is required to do that for their proof to be accepted.
In my view, the recent advances in machine learning has not changed the situation significantly. The "AI" succeeds in very narrow domain (like Go and chess), but only produces something that appears correct in the domain of language and arts. The AI optimists are counting on the mysterious singularity to validate their hypes. Now, it's entirely possible that the singularity will come in the near future, but I do doubt the current technology is a net benefit.