Can mathematics be done by machine? I.
Can mathematics be done by machine? I.
Notes of a Columbia course with Gayatri Chakravorty Spivak and special guest Kevin Buzzard
This is a version of the notes I prepared and presented during the November 4, 2020 session, illustrated above, of Mathematics and the Humanities, the experimental semester-long course I taught with Gayatri Chakravorty Spivak. This session, entitled Can Mathematics Be Done by Machine? has already been mentioned on this newsletter as the occasion for my co-teacher's assertion that "the digital will never capture the contingent." Kevin Buzzard joined us from London by Zoom. I have slightly edited the notes to eliminate some repetition of text that was already published on this site, but assiduous readers will recognize sentences that have appeared here, in some cases more than once. The course was taught in hybrid form — half of the students were present in a Columbia classroom1, and the others were scattered across the globe. I have therefore preserved the original format, as far as possible; each heading was at the top of a slide.
That week I was the main teacher, Kevin Buzzard was the guest, and Spivak was the respondent to both of us. More of her contribution will be quoted in a future installment, along with some of the material Kevin brought to the session.
As always, discussion is welcome at the MWA blog.
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?
Questions to keep in mind
Most articles about controversies regarding the AI future of mathematics focus primarily on two questions — “Is it good or bad?” and “Will it work or not?” — while neglecting to reflect on the presuppositions that underlie these questions — what is the good of mathematics, and work to what end? — not to mention what should always be the first question to be addressed to any significant social development — cui bono, in whose interest?
The ethical evaluation of mechanized mathematics should remember that what pure mathematicians find valuable about what we do is precisely that it provides a kind of understanding whose value is not determined by the logic of the market. (But I suspect mechanical mathematicians will be programmed, or naturally inclined, to disregard that value!)
Mathematics and utility
…as more arts were invented, and some were directed to the necessities of life, others to its recreation, the inventors of the latter were naturally always regarded as wiser than the inventors of the former, because their branches of knowledge did not aim at utility. Hence when all such inventions were already established, the sciences which do not aim at giving pleasure or at the necessities of life were discovered, and first in the places where men first began to have leisure. This is why the mathematical arts were founded in Egypt; for there the priestly caste was allowed to be at leisure.
Aristotle, Metaphysics, 981b
Si les trois âges du concept sont l’encyclopédie, la pédagogie et la formation professionnelle commerciale, seul le second peut nous empêcher de tomber des sommets du premier dans le désastre absolu du troisième, désastre absolu pour la pensée, quels qu’en soient bien entendu les bénéfices sociaux du point de vue du capitalisme universel.
Gilles Deleuze et Félix Guattari, Qu’est-ce que la philosophie?2
A ten-year challenge, constantly renewed, indefinitely postponed.
Electronic digital computing was not yet 15 years old in 1958 when Alan Newell and Herbert Simon, in a widely-quoted article published in the journal Operations Research, predicted that within ten years, digital computers would reach four milestones, on the way to a "world in which [human] intellectual power and speed are outstripped by the intelligence of machines."
The goal of mechanizing aspects of what many took to be the essence of humanness meant that artificial intelligence was a controversial field from its earliest years on.
(Donald MacKenzie, Mechanizing Proof3
The reward
The Fredkin Foundation established three prizes in Automatic Theorem Proving (ATP). In the mid-1980s the Foundation asked the AMS to appoint a formal ATP prize committee and to take over the administration of the awards.
The Leibniz Prize was to be awarded "for the proof of a 'substantial' theorem in which the computer played a major role." The prize criterion:
The quality of the results should not only make the paper a natural candidate for publication in one of the better mathematical journals, but a candidate for one of the established American Mathematical Society (AMS) prizes … or even a Fields Medal. The proofs should not be less sophisticated than those of classical theorems when they first made their appearance…. Though obviously difficult to define precisely, the role of the computer program in the argument should not be mere auxiliary. Novel techniques, meaningful and original definitions, suggestions of interesting intermediate results, perspectives of wider application--any one of these contributions, and others that cannot be foreseen today, would meet the criteria.
Deep Blue
Since support for these prizes has been withdrawn, currently there are no plans to make future awards. (from the AMS website)
However:
Deep Blue Team Awarded $100,000 Fredkin Prize (NY TIMES, 7/30/97)
Grand Challenges in AI
The Unfinished Agenda for 21st Century
• Any Language to Any Language Translation among the top 100 languages with less than 5% error and
• Any Spoken Language to Any Spoken Language (Speech To Speech) Translation among the top 100 languages with less than 5% error
• Discovery of a Major Mathematical Result by AI
• Remote Repair in Space
• Self-Reproducing Robots
( from Raj Reddy, Talk at the Heidelberg Laureate Forum 9/27/194)
The “essence of humanness” (in red)
Six reasons not to trust humans with mathematics
1. They are sentimental.
Is a proof no more than the verification of the truth of a proposition, which can therefore be translated unambiguously?
Or does a human proof contain more than a logical deduction, just as the opening sentence of Jane Austen’s Pride and Prejudice contains more than its literal meaning?
2. They are mortal (and their minds are not open to inspection)
Kevin Buzzard worries that much mathematical knowledge is not only implicit (as many philosophers have recognized) but is often so localized, even within the mind of a single mortal mathematician, that it cannot be considered reproducible. Buzzard is a number theorist who thoroughly understands every step but one in the proof of Fermat's Last Theorem. The exception is the Langlands-Tunnell theorem, (after Robert P. Langlands, Jr. and Jerrold Tunnell). Wiles took this theorem on faith, as the starting point for his argument, because it had been checked by the experts.
3. Humans make mistakes
The unreliability of human perceptions is one of the oldest themes in philosophy (a 14000-word entry on the Stanford Encyclopedia). Special properties of deductive reasoning are supposed to confer immunity on mathematics from this unreliability, but since most actual proofs contain mistakes we see that this is insufficient. We have seen several alternative paradigms proposed to account for this discrepancy. Automated proof verification is an attempt to realize the formalist paradigm. (See the next installment.)
4. Humans are political
In a report posted online today, Peter Scholze of the University of Bonn and Jakob Stix of Goethe University Frankfurt describe what Stix calls a “serious, unfixable gap” within a seriesofpapers by S. Mochizuki.
Between 12 and 18 mathematicians who have studied the proof in depth believe it is correct, wrote Ivan Fesenko of the University of Nottingham in an email. But only mathematicians in “Mochizuki’s orbit” have vouched for the proof’s correctness, [Brian] Conrad commented in a blog discussion last December. “… nobody else … has been willing to say even off the record that they are confident the proof is complete.”
When [Mochizuki] told colleagues the nature of Scholze and Stix’s objections, he wrote, his descriptions “were met with a remarkably unanimous response of utter astonishment and even disbelief (at times accompanied by bouts of laughter!) that such manifestly erroneous misunderstandings could have occurred.”
(Erica Klarreich, Quanta, 9/20/2018)
In spite of the objections of of Scholze and Stix, which have not been withdrawn, Mochizuki's papers containing the purported proof was published in March 2021 in a special double issue of the Publications of the Research Institute for Mathematical Sciences.
5. Humans get bored
[Voevodsky’s new system] hastens the day when our mathematical literature has been verified mechanically and referees are relieved of the tedium of checking the proofs in articles submitted for publication. (Dan Grayson, 2017)
In other words, no human will ever again have to read a proof carefully.
6. Humans are imprecise
Kevin was trying to get his system to accept his formalized proof of the Hilbert basis theorem, a fundamental result in algebra.5 The theorem states that if a ring R is noetherian then the ring of polynomials R[X] is also noetherian. After puzzling over HAL 9000's reaction, Kevin realized that HAL was right: as soon has he added the condition that R is not the zero ring, HAL withdrew its (pronoun?) objection.
Human mathematicians: good riddance!
On pp. 326-327 (of Mechanizing Proof), Donald MacKenzie quotes a computer scientist who argued that mathematicians' failure to perform proofs formally, "by manipulating uninterpreted formulae accordingly [sic] to explicitly stated rules" proves that "mathematics today is still a discipline with a sizeable pre-scientific component, in which the spirit of the Middle Ages is allowed to linger on" [Dijkstra 1988], a philosopher (Peter Nidditch) who claimed that "in the whole literature of mathematics there is not a single valid proof in the logical sense," and another philosopher who doubts "that mathematics is an essentially human activity" [Teller 1980].
Part II will be posted in four weeks. The next entry, to be posted two weeks from now, will examine what may be meant by “human-level mathematical reasoning.”
Zoom was the means of participation of half of the class on average, but altogether about 3/4 of the students checked in physically at least once. Professor Spivak and I were teaching in room 312 of the Mathematics building at Columbia; a corner of the large blackboard in that room is visible at the back of the image on the left. I was told that this was the only mathematics course being taught in the presence of a live class that semester.
This quotation had already been introduced by Gayatri Spivak in an earlier class.
https://mitpress.mit.edu/books/mechanizing-proof
https://www.heidelberg-laureate-forum.org/fileadmin/user_upload/downloads/2019/HLF19_lecture_Reddy.pdf
Upon learning of this proof, which recovered in a few steps conclusions to which he had devoted much of his professional life, Paul Gordan is supposed to have exclaimed “This is not Mathematics — it is Theology!” The actual story is more nuanced.