Category Archives: Silicon Reckoner

Can mathematics be done by machine? I.

Notes of a Columbia course with Gayatri Chakravorty Spivak and special guest Kevin Buzzard

Summary

Proof, in the form of step by step deduction, following the rules of logical reasoning, is the ultimate test of validity in mathematics. Some proofs, however, are so long or complex, or both, that they cannot be checked for errors by human experts.  In response, a small but growing community of mathematicians, collaborating with computer scientists, have designed systems that allow proofs to be verified by machine. The success in certifying proofs of some prestigious theorems has led some mathematicians to propose a complete rethinking of the profession, requiring future proofs to be written in computer readable code. A few mathematicians have gone so far as to predict that artificial intelligence will replace humans in mathematical research, as in so many other activities.


Mechanization of what mathematics?

One’s position on the possible future mechanization of proof is a function of one’s view of mathematics itself.

Is it a means to an end that can be achieved as well, or better, by a competent machine as by a human being? If so, what is that end, and why are machines seen as more reliable than humans?

Or is mathematics rather an end in itself, a human practice that is pursued for its intrinsic value? If so, what could that value be, and can it ever be shared with machines?

The remainder of the article is at Silicon Reckoner.

Mechanization of Rigor

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

Comment here on this week’s entry on the Substack newsletter.

Book review: The Creativity Code, by Marcus du Sautoy

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

Comment here on this week’s entry on the Substack newsletter.

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.