American Progress, 1872 painting by John Gast; this image is available from the United States Library of Congress‘s Prints and Photographs division under the digital ID ppmsca.09855.

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.