…beyond my interest in how current trends in mechanization of mathematics force me to sharpen my own understanding of what makes mathematics valuable as a human practice (as in this close reading of a magnificent lecture by Dick Gross), I am deeply interested in mechanization of mathematics, of which formalization is a small part, as a social phenomenon: how it establishes a shared vocabulary, an ideology, a system of values, a community; how it overlaps with and is influenced by broader economic and industrial trends; what it does or does not share with contemporary political movements; and much more. In this respect the leanprover-community Zulip Chat Archive is a veritable socio-historical goldmine. And with that in mind I encourage you to direct your comments to this page.
And what does this have to do with mechanization?
…nothing evokes as much hostility among intellectuals as the suggestion that social forces influence or even dictate either the scientific method or the facts and theories of science.(Richard Levins and Richard Lewontin, The Dialectical Biologist)
Last October 24 I unexpectedly received the following message from an extremely eminent colleague who had been invited to join the brand new Association for Mathematical Research, an organization of whose existence I had been unaware until then:
the thing that puzzles me is why do we need a new Society devoted to research? Especially since its mission statement is just: ‘research.’ I’m already a member of a number of them. Is there a subtext I’m not getting here?
Continued at Silicon Reckoner. Comments welcome here, as always.
Any change in technology leads almost inevitably to an improvement in the welfare of some and a deterioration in that of others. To be sure, it is possible to think of changes in production technology that are Pareto superior, but in practice such occurrences are extremely rare. Unless all individuals accept the “verdict” of the market outcome, the decision whether to adopt an innovation is likely to be resisted by losers through non-market mechanism and political activism.
(Joel Mokyr, The Political Economy of Technological Change: Resistance and Innovation in Economic History.)
…Two weeks ago I quoted Jasmin Blanchette, a Dutch computer scientist who complained about “proofs [that] look more like LSD trips than coherent mathematical arguments.” I thank Alex Best for informing me that the expression goes back to the very interesting Teaching Statement that Scott Aaronson posted in 2007. Blanchette sees formalization as a remedy, but it occurs to me that the comparison cuts both ways. Most people who write about that sort of thing claim that enlightenment is what is sought by those who take steps to achieve altered states — through wine, poetry, virtue, meditation, or a drug like LSD. Enlightenment is also what I am seeking in a mathematical proof, and I’m sure most of my colleagues feel the same way. Nick Katz likens a routine sort of mathematical enlightenment to Molière’s M. Jourdain, realizing that he is speaking prose. Most precious are the rare proofs that induce a sense of transcendent bliss, bringing tears to one’s eyes. No such weeping with joy, either by programmer or by machine, has yet been recorded in the annals of formalization.
In connection with today’s entry, however, I am thinking of a different form of enlightenment. Imagine that in your condition of heightened consciousness you find yourself speaking a throwaway word mechanically — like “luddite.” Suddenly you tell yourself that what you hear is not only nor even primarily your own voice, but the entire history of semi-conscious associations that planted that word in your manifest vocabulary. While this is obvious in retrospect, it is only your altered state that impresses upon you the realization, the intimate feeling, that it is the word, with its accretion of dead slogans and long unexamined thoughts, that is speaking through you, and not the other way around. In this situation — here I have to tread carefully, to protect my professional reputation — enlightenment can be experienced as a form of liberation.
The essay continues at siliconreckoner.substack.com.
For mathematical formalists, a proof is a sequence of valid formulas in a symbolic language, each obtained from the previous one (more likely the conjunction of several) by a legal transformation (rule of deduction), or the statement of an axiom.
A theorem is then any valid formula that appears as the final statement in a sequence.
Here is a recent
militant but unsubstantiated attempt to ventriloquize mathematics in support of this Central Dogma:
an informal mathematical statement is a theorem if and only if its formal counterpart has a formal derivation. Whether or not a mathematician reading a proof would characterize the state of affairs in these terms, a judgement as to correctness is tantamount to a judgment as to the existence of a formal derivation, and whatever psychological processes the mathematician brings to bear, they are reliable insofar as they track the correspondence. (Jeremy Avigad, 2020)
Avigad, as you see, actually writes “if and only if.” …
The distinction between “if” and “only if” is in any case lost on the public when the Dogmatic position is supported, as Avigad’s is, by a new $20,000,000 institute as well as the backing of a 33-year-old cryptocurrency billionaire who is rumored to be willing to donate ten times as much over the coming years.…
The complete essay can be read on the Silicon Reckoner Substack newsletter. Comments welcome here.
Mathematics is unpredictable. That’s what makes it exciting. New things happen. William Thurston, May 14, 2007
It’s a gloomy, rainy, almost wintry day in Paris, which I don’t always love when it drizzles, and I’m starting to write the next entry in this newsletter, trying to figure out what, if anything, Christian Szegedy had in mind when he predicted, as I reported a few weeks ago, that “Autoformalization could enable the development of a human level mathematical reasoning engine in the next decade.” Is there exactly one “human level”? The expression is common among the knights of the artificial intelligence community, whose grail is something called “human level general AI.”
Part 1 of the text continues.
Notes of a Columbia course with Gayatri Chakravorty Spivak and special guest Kevin Buzzard
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.
Part I: A review of Christian Szegedy’s “Promising Path”
“Grothendieck’s way of writing is based on an atypical conception of mathematics, described and theorized in texts [that] vigorously bear witness to the unavoidable poetic aspect that motivates scientific work and the surplus of meaning that formalization believes should be eliminated, although this surplus is precisely where the essence of mathematical thought lies.” (F. Patras, La pensée mathématique contemporaine, Introduction)1
This week and the next I compare two perspectives on the “the surplus of meaning” and “the essence of mathematical thought,” both implicit in texts about mathematics: the first by a prominent exponent and prophet of “intelligent computer mathematics,” the second by a prominent number theorist. It would be too easy to say that the first text takes the position that there is no surplus and that the “essence of mathematical thought” resides in formalization and nothing more, while the second text exemplifies the surplus of meaning as well as what one reviewer of Karen Olsson’s book The Weil Conjectures (to which we return in Part II) called “the poetry and precision of a theorem.” What, after all, is an “essence”? Philosophers have worried about this for millenia, with some interruption, asking for example in what sense the essence of Socrates resembles that of being an even prime number, and have failed to arrive at consensus on the essence of “essence.” The whole confusing history is recorded in the Stanford Encyclopedia of Philosophy’s entry on “Essential vs Accidental Properties” (which, troublingly, includes no references in French).…
The complete text has been published on my Silicon Reckoner Substack newsletter.
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.
- 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.…
2. Human Compatible, by Stuart Russell
Comment here on this week’s entry on the Substack newsletter.