It’s a gloomy, rainy, almost wintry day in Paris, which I don’t always love when it drizzles, and I’m starting to write the next entry in this newsletter, trying to figure out what, if anything, Christian Szegedy had in mind when he predicted, as I reported a few weeks ago, that “Autoformalization could enable the development of a human level mathematical reasoning engine in the next decade.” Is there exactly one “human level”? The expression is common among the knights of the artificial intelligence community, whose grail is something called “human level general AI.”

Notes of a Columbia course with Gayatri Chakravorty Spivak and special guest Kevin Buzzard

Summary

Proof, in the form of step by step deduction, following the rules of logical reasoning, is the ultimate test of validity in mathematics. Some proofs, however, are so long or complex, or both, that they cannot be checked for errors by human experts. In response, a small but growing community of mathematicians, collaborating with computer scientists, have designed systems that allow proofs to be verified by machine. The success in certifying proofs of some prestigious theorems has led some mathematicians to propose a complete rethinking of the profession, requiring future proofs to be written in computer readable code. A few mathematicians have gone so far as to predict that artificial intelligence will replace humans in mathematical research, as in so many other activities.

Mechanization of what mathematics?

One’s position on the possible future mechanization of proof is a function of one’s view of mathematics itself.

Is it a means to an end that can be achieved as well, or better, by a competent machine as by a human being? If so, what is that end, and why are machines seen as more reliable than humans?

Or is mathematics rather an end in itself, a human practice that is pursued for its intrinsic value? If so, what could that value be, and can it ever be shared with machines?

Part I: A review of Christian Szegedy’s “Promising Path”

“Grothendieck’s way of writing is based on an atypical conception of mathematics, described and theorized in texts [that] vigorously bear witness to the unavoidable poetic aspect that motivates scientific work and the surplus of meaning that formalization believes should be eliminated, although this surplus is precisely where the essence of mathematical thought lies.” (F. Patras, La pensée mathématique contemporaine, Introduction)1

This week and the next I compare two perspectives on the “the surplus of meaning” and “the essence of mathematical thought,” both implicit in texts about mathematics: the first by a prominent exponent and prophet of “intelligent computer mathematics,” the second by a prominent number theorist. It would be too easy to say that the first text takes the position that there is no surplus and that the “essence of mathematical thought” resides in formalization and nothing more, while the second text exemplifies the surplus of meaning as well as what one reviewer of Karen Olsson’s book The Weil Conjectures (to which we return in Part II) called “the poetry and precision of a theorem.” What, after all, is an “essence”? Philosophers have worried about this for millenia, with some interruption, asking for example in what sense the essence of Socrates resembles that of being an even prime number, and have failed to arrive at consensus on the essence of “essence.” The whole confusing history is recorded in the Stanford Encyclopedia of Philosophy’s entry on “Essential vs Accidental Properties” (which, troublingly, includes no references in French).…

The complete text has been published on my Silicon Reckoner Substack newsletter.

A presentation at the PhilMath Intersem in Paris in June 2019.

Mechanical proof assistants — for the purpose of proof verification as well as for proving theorems — have been around as long as computers. Mathematicians have only been paying serious attention over the last 20 years or so. Several highly respected mathematicians independently came to the conclusion that the form of peer review that was institutionalized over the last few generations has reached a kind of crisis, in which it can no longer be seen as a reliable warrant for the correctness of mathematical proofs. This is either because the proofs are too long or complex to be scanned by a human reader or because it fails to detect fatal mistakes. Kevin Buzzard has expressed different concerns — much mathematical knowledge is implicit (as many philosophers have recognized) but often so localized (even within the mind of a single mortal mathematician) that it cannot be considered reproducible. More positive reasons to welcome mechanical proof assistants have also been expressed — to help with the tedious parts of the referee process, or of the proofs themselves, or for heuristic interaction at various stages in seeking proofs (Gowers). Patrick Massot has written to me that “Having formalized definitions, statements and proofs is also very useful to learn, communicate, and teach mathematics”…

This is the first of a series of reviews of books I have been reading in order to provide at least a veneer of familiarity with the material on AI that I am subjecting to critical analysis. Marcus du Sautoy’s book should be the easiest to review, because du Sautoy is a mathematician and his book recounts a mathematician’s attempt to come to grips with the implications of recent developments in AI, some of them dramatic, for the future of his own profession, which is also mine. The title announces that du Sautoy wants to understand, and to help his readers understand, what AI may mean for the future of human creativity more generally, but it is clear that mathematics is very much on his mind, as it is on mine.…

At one point du Sautoy defines his existential crisis as concern “whether the job of being a mathematician would continue to be a human one.” This is where the ways he and I understand “existential” subtly diverge. I have written on this newsletter, and I will be writing again, that mathematics is “one of the innumerable ways that humans have found to infuse our lives with meaning.” That is not a job description. From beginning to end du Sautoy’s book makes it clear that he doesn’t really think of mathematics or any creative activity as a “job,” but when the word appears in sentences about machines replacing human mathematicians, as it does consistently, it’s a hint that someone is looking at the wrong existential crisis.…

What follows is the text of an article, adapted for this newsletter, that I submitted to four prestigious magazines, three of them directed at a general scientifically literate audience, the fourth more specialized but not specifically addressed to mathematicians…

Will computers ultimately be able to generate the kinds of proofs pure mathematicians value, and if so will that constitute progress? The modern history of the word “progress” has so many nasty associations — including colonialism, white supremacy, and genocide, as well as the obliteration of entire skilled professions and the ways of life that accompany them — that I find it difficult to invoke the notion as a positive value, even though in other contexts I’m happy to identify as a progressive. At the very least this troubled history should remind us that it makes no sense to speak of progress without immediately making clear: for whom? But then to ask whether an innovation, technological or not, represents progress for mathematics points to an intriguing question that is too frequently overlooked. What, namely, are the values of mathematics?

…In this connection, if and when future historians (if there are any) try to determine when the project to mechanize mathematics jumped the species barrier between brute force calculation and the core areas of pure mathematics, they may settle on the day in December 2020 when Peter Scholze proposed a challenge on Kevin Buzzard’s xena blog.…

A guest appearance of a pure mathematical icon like Scholze in a venue devoted to “automating mathematical reasoning” already qualifies as news, the more so when his challenge was met, to his great satisfaction, exactly half a year later. Quanta Magazine certainly thought so; on July 28 they published an article entitled “Proof Assistant Makes Jump to Big-League Math” on the challenge and its successful conclusion, incidentally confirming the appropriateness of the word “jump” that you read three paragraphs back. Scholze is impressed:

I now think it’s sensible in principle to formalize whatever you want in Lean. There’s no real obstruction.

But those curious about possible future cohabitation of mathematics with computation should look more closely at the contents of Scholze’s challenge.…

I have finally got around to creating a newsletter, tentatively entitled Silicon Reckoner, to be published on Substack. This will be a continuation of the recurring discussion on this blog of the implications of projects to mechanize mathematics, for example in this post or this post.

You can read more about the goals of the newsletter below, in excerpts from the first entry. There will be no additions to the MWA blog (the blog you are now reading) for the foreseeable future. However, at least at the outset I plan not to allow comments on Substack; instead, the comments section of this post will be reserved for discussion of the newsletter. As always, I will decide whether or not to approve comments. This is a form of censorship but the purpose is not to exclude (legitimate) points of view but to keep control of the amount of time I spend on this part of my agenda.

I don’t expect to set up paid subscriptions on Substack, but that may change at some point.

And the disclaimer, to appear in the first newsletter entry:

I will not claim familiarity with any of the formal systems used in the design of automated proof checkers, nor to understand any of the software that implements the actual automatic verification, much less to understand the details of current or future work on AI, whether or not it is applied to mathematics. Even when I have a pretty good idea of what is going on with some of these systems, I will fiercely deny any technical understanding whatsoever, because my understanding of the technicalities should never be an issue.

Is artificial intelligence on track to meet the expectations of its investors, who just in 2020 poured $50 billion into the industry? AI’s record of missed deadlines for predicted milestones is as old as its name. But literary production on the subject could hardly be more extensive. Reading all the non-technical books on my local bookstore’s AI shelf would be more than a full-time job, leaving less than no time for my real job, which AI has not yet eliminated. Even the sub- or parallel discipline of AI ethics now occupies 10 pages of footnotes on the English-language Wikipedia page and 1400 pages published in the last two years by Oxford University Press, on my own bookshelf; practically every day I discover another 100 pages or so. I have nevertheless forced myself to dip into a representative sample as preparation for an experiment that is beginning to take shape with this text.

Most of what I’ve read tries to address the question of just how “intelligent” the products of this industry have been up to now, or will be in the near future, or what it would take for actually existing AI to deserve to be called “intelligent,” or whether it would be a good thing, or whether it’s even possible. None of these is my problem. Or rather, they are my problem, but only as a citizen of my country, or of borderless civilization, concerned, like everyone else, by what the massive implementation of ostensibly intelligent artificial systems would entail for what matters to me — not least, whether it would make sense for these things to continue to matter to me, or perhaps more accurately whether what matters to me would still matter to anyone or anything else, if the ambitions of AI’s promoters even minimally come to fruition.…

My motivation in undertaking this experiment is to understand the consequences of this way of thinking for my own vocation of pure mathematics, which is marginal to the concerns of most of those at risk of the AI project’s collateral damage but which has been central to the project’s imagination and its aspirations from the very outset.

It is possible to view the growing interest in automated proof verification and artificial theorem proving, two aspects of a still largely hypothetical AI future of mathematics, as stemming from purely internal factors that govern the profession’s development as it evolves to meet its autonomously defined goals. The ideal of incontrovertible proof has been bound up with mechanization since it was first articulated, and the logic that ultimately made digital computers possible is a direct outgrowth of the attempt to perfect this ideal in the development of symbolic and philosophical logic in the late 19th and early 20th century, and can even be seen as a byproduct of the proof of the absolute impossibility of realizing this ideal. I don’t think this view is plausible, given the saturation of our culture with AI themes and memes, that goes well beyond bookstores’ overloaded AI shelves.…

This post is meant to be the first of a series of texts exploring the reasons for the absence of any sustained discussion of these issues on the part of mathematicians, in contrast to the very visible public debate about the perils and promises of AI. Much of my book Mathematics without Apologies was devoted to a critique of claims regarding the “usefulness” of mathematics when, as is nearly always the case, they are not accompanied by close examination of the perspectives in which an application of mathematics may or may not be seen as “useful.” Similarity with the intended critique of the uncritical use of words (like “progress”) that accompany the ideology surrounding mechanization — mechanical proof verification and automated theorem proving, in particular — will be apparent. The reason should be obvious: unless we can conceive an alternative to conventional measures of utility for which human mathematics is a positive good, the forces that make decisions about this sort of thing will declare my vocation obsolete. Most of my colleagues who are involved in advancing the mechanization program have conceded the rhetorical battle and some are already forecasting the demise of human mathematics. So the plan is to continue the discussion in this new format, and gradually to phase out the blog that I launched when Mathematics without Apologies was published, as I have already tried and failed to do once before.

Because I will be forced to draw on so many different disciplinary perspectives in the course of exploring the topic of mechanization, there is a real danger that these texts will lose any chance of forming a coherent whole. For my own sake, then, as much as for the sake of potential readers, I propose a slogan that is meant to hold everything together until I come up with a better slogan. Here it is:

Current trends in mechanization belong to the history of mathematics, both as events in a historical process and in the creation of common narratives about the meaning of the process. …

Several footnotes in MWA quote the philosopher Jacques Rancière’s Aisthesis:

Jacques Rancière writes that “Art exists as an autonomous sphere of production and experience since History exists as a concept of collective life” and dates this existence back to the mid-18th century…. Replacing Art by (small-m) mathematics in the above sentence, it says that the existence of mathematics as a self-conscious tradition-based practice is tied up with its projection in history, which is consistent with the themes of Chapter 2. The timing for mathematics may be different.

(note 70 to Chapter 3)

The questions of where (or whether) to draw the line between art and technique, or between the artist and the artisan, dominate many of the aesthetic debates of the 19th and 20th centuries, as reconstructed in (Rancière 2011).

(note 40 to Chapter 8)

For the educational benefits of the arts in France, see (Rancière 2011), Chapter 8, especially pp. 173-175. The aesthetic theorists Rancière treats in this chapter, which covers a period stretching from Ruskin through the Paris Exposition Universelle of 1900 to the Bauhaus, have in common a vision of art as “the power to order the forms of individual life and those in which the community expresses itself as community in a single spiritual unity” (p. 178). This ethic of art is much more familiar than the model on which Hardy draws and it is hard to imagine its application to mathematics in any way.

(note 18 to Chapter 10)

But Rancière’s influence on MWA is pervasive in the chapters that attempt to characterize what mathematics has in common with the arts, and goes well beyond what is contained in these few quotations. So I am pleased to share this portrait, created by the French artist who goes by the name Chaix et les étiquettes, at the request of a group of the philosopher’s admirers.

Chaix’s portraits are composed entirely of stickers that he collects surreptitiously, by the hundreds, during visits to the fruit departments of local supermarkets. The detail below reveals that the red background was liberated from a batch of pears, whereas the philosopher’s wavy white hair originally enlivened a stack of Royal Gala apples. The blue eyes are too blurry for me to read.

An updated and expanded version of this post has been published at Silicon Reckoner. Comments on the new version are welcome below.

Mechanization of mathematics, at least in certain aspects, has been welcomed as “progress,” notably in a comment on this blog. Most readers of this blog, I suspect, will embrace the “progressive” label, if the alternative is what is being promoted on the Killing Obama’s Radical Progressive Agenda Facebook page. Nevertheless, as the above image reminds us, the notion of “progress” in its current usage is so thoroughly entwined with technological determinism, European colonialism, genocide, and environmental devastation, that it is a struggle to find an interpretation of the word, applicable to mathematics, whose connotations are unequivocally positive.

The OED traces the first use of the word, in the (originally metaphorical) sense of

Advancement to a further or higher stage, or to further or higher stages successively; growth; development, usually to a better state or condition; improvement…

to 1457 in the Acts of Parliament of Scotland, in the sentence

Sen Gode..hes send oure souerane lorde sik progres and prosperite, that [etc.].

The word’s current use evolved from the mid-18th through 19th centuries, from the Enlightenment through the Industrial Revolution. The OED quotes Benjamin Franklin using the word in 1780. In 1794 the Marquis de Condorcet wrote his Sketch for a Historical Picture of the Progress of the Human Mind, “perhaps the most influential formulation of the idea of progress ever written” according to Wikipedia, while hiding on the“rue des Fossoyeurs” (the present-day rue Servandoni) in Paris from the warrant for his arrest issued by the Convention. (By dying in prison, Condorcet escaped the guillotine, “a symbol of the penal, technological and humanitarian progress inspired by the Enlightenment” according to the Open University website.) In the 19th century “progress” was a watchword for thinkers as diverse as Hegel, Comte, Marx and Engels (“entire sections of the ruling class are, by the advance of industry, precipitated into the proletariat [… and] also supply the proletariat with fresh elements of enlightenment and progress”), Darwin, and Herbert Spencer (“the civilized man departs more widely from the general type of the placental mammalia than do the lower human races“).

Gast’s painting is one illustration of the principle, that was generally accepted by European colonizers, including the American settlers, and given clear expression by the German Rudolf Cronau in 1896:

The current inequality of the races is an indubitable fact. Under equally favorable climatic and land conditions the higher race always displaces the lower, i.e., contact with the culture of the higher race is a fatal poison for the lower race and kills them…. [American Indians] naturally succumb in the struggle, its race vanishes and civilization strides across their corpses…. Therein lies once again the great doctrine, that the evolution of humanity and of the individual nations progresses, not through moral principles, but rather by dint of the right of the stronger.

Rudolf Cronau, in Friedrich Hellwald, Kulturgeschichte in ihrer natürlichen Entwickelung, 4th ed., 4 vols. (Leipzig: Friesenhahn, 1896 ), IV: 615-16

Other colonial powers used the notion of progress in similar ways. Gast’s painting is well-known but I only became aware of it last month, when I watched Raoul Peck’s indispensable four-part documentary Exterminate all the Brutes, whose title is a quotation from the character Kurtz in Conrad’s Heart of Darkness, characterized as “an emissary of pity and science and progress, and devil knows what else.” “By the simple exercise of our will we can exert a power for good practically unbounded,” Kurtz said, a few lines before arriving at the words that served as Peck’s title. This was the intellectual matrix in which Hitler formed his world view. The word “progress,” in expressions like “human progress” or “progress of mankind,” appears dozens of times in Mein Kampf. A typical example:

“Not through [the Jew] does any progress of mankind occur.”

Mein Kampf, Chapter XI.

Now that Godwin’s law has been reconfirmed, possibly for the first but certainly not for the last time, in connection with mechanization of mathematics, I can quickly come to the point of this post, which is to draw attention to the questions that are not being asked when the desirability or feasibility of mechanization of mathematics is under debate. Arundhati Roy asked one such question in her first non-fiction book, about the Narmada Dam project:

How can you measure progress if you don’t know what it costs and who has paid for it?

Arundhati Roy, The Cost of Living, Random House of Canada, 1999

Twenty years after the book’s publication, when the dam has submerged at least 178 villages in Madhya Pradesh, Tina Stevens and Stuart Newman defended the precautionary principle as protection from the “hidden agendas of BioTechnical science”:

Precaution does not derail progress; rather, it affords us the time we need to ensure we progress in socially, economically, and environmentally just ways.

Tina Stevens and Stuart Newman, Biotech Juggernaut, Routledge, 2019

Most of the mathematicians and philosophers who promote mechanization are perfectly candid about their agendas, and cannot be suspected of genocidal tendencies. But the potential implications of the widespread adoption of technological solutions to perceived mathematical problems — “what it [will] cost… and who [will pay] for it,” not to mention the question of who stands to benefit — are simply not being acknowledged.

This post is meant to be the first of a series of texts exploring these questions and the reasons for the absence of any sustained discussion of these issues on the part of mathematicians, in contrast to the very visible public debate about the promises and dangers of AI. Much of MWA was devoted to a critique of the notion of “usefulness” in mathematics when, as is nearly always the case, it is not accompanied by a close examination of the perspectives in which an application of mathematics may or may not be seen as “useful.” The similarities with the intended critique of the uncritical use of the word “progress” are evident, but now I want to keep focused on the ideology surrounding mechanization — mechanical proof verification and automated theorem proving, in particular. So the plan is to continue this discussion in a different venue, and gradually to phase out this blog, as I have already tried and failed to do once before.