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. 

Here, then, is what Silicon Reckoner will be about:

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. …