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).…
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.
To quote the petition that you are all invited to sign:
In February of 2019, the Moscow State University mathematics PhD student Azat Miftakhov was arrested and detained for manufacturing explosives. Later these charges were dropped. As soon as he was released, he was arrested and detained for another unrelated crime: breaking a window in the office of United Russia, the ruling political party in the Russian Federation. We, along with the international civil rights society Memorial, consider Azat to be a political prisoner, unfairly framed due to his anarchist views. The court extended his pre-trial period multiple times — a year and a half in total — without reason. Law enforcement officials have tortured him, restricted his access to scientific literature, and threatened his relatives’ personal safety.
The Société Mathématique de France published an update on December 21, and called for its membership to sign the petition:
Le procès d’Azat Miftakhov approche de sa conclusion. Les débats sont prévus le 23 décembre. Le verdict devrait tomber peu de temps après.
Le 14 novembre 2020, la SMF a exprimé sa profonde préoccupation face à la détention prolongée du jeune probabiliste et activiste politique russe qui fut incarcéré début février 2019. Il est resté emprisonné depuis et a été torturé. Azat Miftakhov est accusé d’avoir cassé une vitre dans un bureau de la “Russie unie”, le parti politique au pouvoir. Il plaide non coupable.
I’ve been saying for some time that most articles about controversies regarding the AI future of mathematics focus primarily on two questions — “Is it good or bad?” and “Will it work or not?” — while neglecting to reflect on the presuppositions that underlie these questions — what is the good of mathematics, and work to what end? — not to mention what should always be the first question to be addressed to any significant social development — cui bono, in whose interest? Within the limitations imposed by this conventional frame of reference, last week’s article in Quanta by Stephen Ornes was a good one. It provided a clear introduction to the subject matter for the well-informed amateurs as well as professionals who read Quanta, recalled the history of attempts to automate proofs — with a helpful reminder that these attempts were originally motivated by the need for computer scientists to verify the reliability of their programs, a theme treated in depth by Donald MacKenzie in his classic Mechanizing Proof — and surveyed some of the most ambitious contemporary projects and their applications within mathematics.
When I agreed to be interviewed for the article it was in the hope of nudging the discussion in the direction of the questions that are typically neglected. In responding to Ornes’s first message I made only one request:
If you decide you do want to use one or more quotations from me, I would want at least one of them to address this point: that what pure mathematicians find valuable about what we do is precisely that it provides a kind of understanding whose value is not determined by the logic of the market.
Note my abusive and rather underhanded implicit definition of the pure mathematician as one whose values conform to an impossibly unrealistic ideal. The impulse to cash in must surely be alive in my professional community as it is in every other corner of neoliberal civilization. And yet, if the products of our imagination cannot provide an escape from the market, what can?
The sentence quoted above was in the last draft of the article that Quanta showed me, but it did not make the final cut. (And the editors also disregarded my invitation to use the photo reproduced above, which better conveys my mixed feelings about the whole business than the photo they did use.) The article’s only hint of the cui bono question was a brief allusion to Christian Szegedy’s group at Google Research. I don’t know what was in the back of Google’s mind when they decided to sponsor research into automating mathematical proof. Their business is computing: maybe they are simply looking to improve software verification, like the original proof automaters. Or maybe they really are interested in mathematics as such; but I would not count on them to care about “a kind of understanding whose value is not determined by the logic of the market.” To a very great extent, Google and its Silicon Valley companions are the market. If Google’s aim is to reproduce what drives us to invent things like homotopy theory and pseudodifferential operators, it can only be because they think they can bottle it and sell it back to us, just as they have done with our search histories and the keywords they extracted from our gmail.
Whether or not you find that “evil” depends on your frame of reference. Just yesterday I received a notification of an NSF Program Solicitation entitled “National Artificial Intelligence (AI) Research Institutes”:
Artificial Intelligence (AI) has advanced tremendously and today promises personalized healthcare; enhanced national security; improved transportation; and more effective education, to name just a few benefits. Increased computing power, the availability of large datasets and streaming data, and algorithmic advances in machine learning (ML) have made it possible for AI research and development to create new sectors of the economy and revitalize industries. Continued advancement, enabled by sustained federal investment and channeled toward issues of national importance, holds the potential for further economic impact and quality-of-life improvements.
The 2019 update to the National Artificial Intelligence Research and Development Strategic Plan , informed by visioning activities in the scientific community as well as interaction with the public, identifies as its first strategic objective the need to make long-term investments in AI research in areas with the potential for long-term payoffs in AI. The President’s Council of Advisors for Science and Technology has published Recommendations for Strengthening American Leadership in Industries of the Future , including AI, and calls for new and sustained research in AI to drive science and technology progress. The National AI Research Institutes program enables longer-term research and U.S. leadership in AI through the creation of AI Research Institutes.
This program is a joint government effort between the National Science Foundation (NSF), U.S. Department of Agriculture (USDA) National Institute of Food and Agriculture (NIFA), U.S. Department of Homeland Security (DHS) Science & Technology Directorate (S&T), and the U.S. Department of Transportation (DOT) Federal Highway Administration (FHWA). New to the program this year are contributions from partners in U.S. industry who share in the government’s goal to advance national competitiveness through National AI Research Institutes. This year’s industry partners are Accenture, Amazon, Google, and Intel Corporation.
This program solicitation invites proposals for full institutes that have a principal focus in one or more of the following themes, detailed in the Program Description:
• Theme 1: Human-AI Interaction and Collaboration
• Theme 2: AI Institute for Advances in Optimization
• Theme 3: AI and Advanced Cyberinfrastructure
• Theme 4: Advances in AI and Computer and Network Systems
• Theme 5: AI Institute in Dynamic Systems
• Theme 6: AI-Augmented Learning
• Theme 7: AI to Advance Biology
• Theme 8: AI-Driven Innovation in Agriculture and the Food System
(Emphasis added.) I’d guess Automated Theorem Proving fits best with Theme 1. So the researchers quoted are unwittingly (or maybe wittingly) contributing to a logic of national competition. This sort of language always strikes me as ironic, given the international nature of projects like proof automation, and given my own failure to muster much enthusiasm for French national competitiveness during my years teaching in Paris, in spite of frequent exhortations from the authorities using identical language (but in French, of course).
I shouldn’t complain that Quanta did me the honor of giving me the last word but when I read it in the draft —
Even if computers understand, they don’t understand in a human way.
— I couldn’t believe that I had actually written anything so imprecise. And I’m still pretty sure I never did; but unfortunately I did speak those words at this roundtable. The thought is hardly original to me; mathematicians have been saying this in various ways for years, at least since the Appel-Haken solution of the Four-Color Problem. I tried to add some content by revising the sentence to restore the context in which it was spoken:
Even if we do want to attribute understanding to computers, it won’t be the kind of understanding we attribute to human beings.
This amendment, too, was included in the last draft I saw, but the sentence reverted to the shorter version. I should not have been surprised: the published sentence is meaningless but is admittedly more journalistically effective. On this blog I’m not constrained by a word limit, so let me revise the sentence one more time:
Even if we do want to attribute understanding to computers, it won’t be the kind of understanding we currently attribute to human beings.
The word “currently” reflects my expectation that the industrial version of proof automation, which is where I suppose this is all heading, will lead not only to a reconsideration of the purpose and nature of mathematical proof — hardly for the first time — but also to a new adaptation of human understanding to the needs of machines. This is in line with the industrial imperative Shoshanna Zuboff sees in what she calls surveillance capitalism:
With this reorientation from knowledge to power, it is no longer enough to automate information flows about us; the goal now is to automate us.