New entry on Substack newsletter on Scholze’s liquid tensor experiment

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.

3 thoughts on “New entry on Substack newsletter on Scholze’s liquid tensor experiment

  1. Will Sawin

    The idea that machine learning would consign applied mathematicians to the recycle bin is a bit of a strange one to me. One only has to look at some recent machine learning papers to see significant amounts of applied mathematics! A neural network is quite a rich and complicated mathematical structure and there is lots, potentially, to do to study them.

    Of course one might hope that the neural networks will eventually figure out to design themselves, but the same can be said for almost any other field of human endeavor.

    Liked by 1 person

    1. mathematicswithoutapologies Post author

      I agree with you completely, but there is a habit of thought that views any form of paid activity as a “job” and then presumes that because some “jobs” can be automated then so can all the rest of them.

      Software verification has been automated to a certain extent for some time. I can imagine an epidemiological system that would collect all data from all sources and generate a comprehensive plan, even going so far as to lock people in their homes automatically after a suspected contact. I don’t imagine I would enjoy the company of the “one” who might hope for that sort of thing, nor for the other kind of “one” who hopes that neural networks will design one another.


  2. Thomas

    “Was it fun ?” probably is a good rule of thumb, but not sure Cantor would have answered yes. Yet his work is of stunning beauty and importance and i for one would have wanted him for colleague.



Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s