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

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