Intelligent Computer Mathematics vs. Intelligent Mathematics
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).2
Please submit comments here.
Christian Szegedy's name first came to my attention in an email message Kevin Buzzard sent me in May 2019, around the time we were planning our joint appearance at PhilMath Intersem 10.2019. Szegedy “is a researcher at Google working on machine learning, AI and computer vision via deep learning,” according to his Google Research page. Kevin had met him at “a serious conference about this stuff [automated theorem proving] in April” 2019 and paraphrased Szegedy's thoughts about computers and mathematics in the following words:
…computers are terrible at doing something, and then they're slightly less terrible, and then all of a sudden there are some new ideas which work and there is an extreme acceleration and then all of a sudden they're better than humans. Szegedy claims that computers will be better at proving theorems than humans within 10 years. I am extremely skeptical.… He actively wants to put us out of business.
The last part is just an expression, of course; Kevin would be the last person to think of mathematics as a “business.” He added: “I have seen no evidence yet that he will succeed.” Nevertheless, this comment, along with Patrick Massot's report in September 2020 that Szegedy's team at Google saw mechanization of mathematics as “a nice intermediate goal towards general AI,” put Szegedy on my radar. So I was glad that it didn't take me very long to find the article — “A Promising Path Towards Autoformalization and General Artificial Intelligence,” the lead article in the proceedings of the 2020 international conference on Intelligent Computer Mathematics — that confirms Massot's point. Szegedy's article, to which I turn now, expounds his and Google's view, as of 2020, that
in the coming years we will see automated systems to rival humans in general reasoning and the fastest path to achieve this is by creating automated mathematical reasoning systems via autoformalization.
The medium-term goal, as I already quoted on this newsletter, is to create "a human level mathematical reasoning engine in the next decade." The article outlines "a realistic path" to that goal through the short-term goal of creating an autoformalization system, which Szegedy defines as
an automated system that is capable of automatically formalizing significant portions of mathematics from a natural language input and verifying it automatically…
Here "formalizing" is the sort of thing we have already discussed in connection with the xena project and elsewhere. In other words, instead of undergraduates having "really good fun" under Kevin Buzzard's benevolent guidance, the process will be fully automated.
At some point during Covid confinement I saw that Szegedy and I had signed the same petition, though I don't remember which one. This convinced me that Szegedy, in contrast to his employer, is not a vampire, so if he sees this text I hope he will read it in the spirit of dialogue.
The article gets off to a bad start by defining mathematics:
Mathematics is the discipline of pure reasoning. Mathematical reasoning is not about mathematics per se, it is about reasoning in general.
What's wrong with this paragraph is not that the definition is incorrect; it's rather that it's a bad idea to attempt to define mathematics in the first place. When I started writing texts about (what I considered to be) bad ideas about mathematics, my first impulse was to begin by defining mathematics. It took me less than an hour of reflection to realize that the impulse would have to be kept in check.
There is a Wikipedia page entitled Definitions of Mathematics whose first paragraph is absolutely correct:
Mathematics has no generally accepted definition. Different schools of thought, particularly in philosophy, have put forth radically different definitions. All proposed definitions are controversial in their own ways.
The Wikipedia page goes on to illustrate its first paragraph with 18 different definitions, many of them by philosophers or mathematicians who became famous in spite of having loitered in this particular blind alley.3 The word "reasoning" doesn't appear on the page; the definition closest to Szegedy's is due to C.S. Peirce: Mathematics is the science that draws necessary conclusions. But "reasoning in general" is rarely constrained by the "necessary." Pierce himself is known for the famous move of adding abductive reasoning as a third alternative to inductive and deductive reasoning, only the last of which can lay claim to "necessity." In fact, several of the books I've read about AI — and that I intend to review at some point —complain explicitly that it will never "rival humans" as long as it neglects abduction.
Reuben Hersh's What is Mathematics, Really? doesn't answer the question in the title with a definition: he asserts
There's no need to look for a hidden meaning or definition of mathematics beyond its social-historic-cultural meaning.
and later that one can't really be more precise than
Mathematics is the mathematical study of mathematical patterns.
In the middle of his account of Lakatos's Proofs and Refutations — which he correctly identifies as "a blistering attack on formalism" and therefore a precocious dismissal of the revived formalization program4 — Hersh writes "We need to know what mathematics is about." But he fortunately doesn't try to satisfy this need, so I conclude the "We" is meant rhetorically. I read Szegedy's claim that mathematics is "about reasoning in general" while composing a warning about those for whom mathematics looks like "a dead mechanical dog" and I wrote in the margin: what is "being a dog" about? or a skunk?
It's unfair to take Szegedy to task for these two sentences, however, when no one, not excluding philosophers and mathematicians, can lay claim to the correct definition of mathematics. This may be the activity that he and his team at Google think they are emulating; what really matters is not what they think they are doing but what they are doing. I am reassured by the claim in his abstract that autoformalization, the technique to which his article is devoted,
could have far reaching implications not just for mathematical research, but also for software synthesis,
and he makes this more precise in the body of the text:
a solution to autoformalization could give rise to programming agents that turn natural language descriptions into programs.
This brings us back to the original motivation for mechanizing proof, as explained at great length in Donald MacKenzie's book of that title. For example:
From the 1960s on, NSA and some other military agencies began to be concerned about computer security… Much of the financial support in the United States for the development of automated theorem provers arose from the desire of ARPA and NSA for mechanical proofs of security…
Indeed, mathematical reasoning, according to Szegedy, is "just reasoning about anything specified formally," [my emphasis] and he chooses the examples of "verify[ing] the correctness or resource use of a computer program or … deriv[ing] the consequences of a physical model" to illustrate his point. I italicized the word "just" to illustrate how Google may wish to redefine mathematics, possibly along the lines promoted by Andreas Bogk on my blog:
You know, I’m just a random programmer, but I grew up believing that mathematicians are interested in a precise science, not the hand-waving kind. I’m shocked to find that this seems to be not the case, that you argue for glossing over essential differences in axiomatic theories…
But to return to autoformalization, I can't deny that some of the "immediate practical applications" Szegedy anticipates will appeal to mathematicians as well as programmers. The second part of this one, for example —
a strong autoformalization system could be used for verifying existing and new mathematical papers and would enable strong semantic search engines
— responds to a wish I've frequently seen expressed on blogs and in public discussions. Say you are a mathematician and you want to know whether a certain theorem has been proved, say for curves of genus 7. Good luck asking Siri or Alexa or OK Google! All of them are semantic search engines but they are not equipped to turn your question into a database search, both because your version of natural language has to be open-ended in order to be useful and because there's no reason to think the hypothetical paper containing the theorem for which you are yearning has used any of the words in your query to formulate the result. A "strong semantic search engine" would have to translate both your open-ended question and an appropriate fragment of the relevant mathematical corpus into recognizably equivalent formal formulas. In other words, as Szegedy writes, it would "demonstrate that sophisticated natural language understanding between humans and AI is feasible."
Since no such engine is currently available, you are stuck with human-level search engines as embodied in the participants on sites like MathOverflow. Or maybe you try your luck asking an expert. All that messy human interaction is inconclusive as well as time-consuming. But serendipity has its own charms. One year past my Ph.D. I asked a senior Brandeis colleague whether he knew anything about the decomposition of holomorphic discrete series representations upon restriction to subgroups. He suggested I ask Hans Plesner Jakobsen, whose office was around the corner from mine but with whom I had never spoken. It turned out that Jakobsen had written several papers on just that question. I have been citing those papers periodically ever since, and my first collaboration was with Jakobsen, which we completed after he returned to Denmark. It's almost certain that if he had not been my colleague I would never have found the answer to my question in time to convince Brandeis not to let me go after my first three-year appointment, and my life would in every respect have turned out differently.
Unless, of course, I had had a "strong semantic search engine" at my disposal.
Starting with a "seed corpus of translations" — a data set consisting of mathematical sentences in natural language alongside their formal equivalents — Szegedy's translation model is trained by generating approximate formalizations of new natural language sentences and then testing the approximation on the seed corpus. The process is reiterated using several deep learning models corresponding to "embed[ding] formal mathematical statements as low-dimensional vectors," "approximate embedding of the formal translation of the informal input statement (given as a picture [sic, see below])," and "an exploration guidance model" based on the existing formalized corpus, the three "trained in lock step."
Szegedy makes it clear that his project's ambition is to "go far beyond just transforming mathematics itself"; as Massot correctly reported, the project "could result in the creation of a general purpose reasoning module to be used in other AI systems." "Just transforming,"5 "disrupting," "moving fast and breaking things" — we have become inured to this sort of language and our reaction to such an ambition is probably a mixture of excited anticipation of our new and transformed professional lives (that, face it, have grown drab and stale) and resignation before the technological onslaught whose victory, it has been drummed into us, is inevitable, with each of us experiencing the mixture in different proportions.
The system also includes a "reasoning engine (theorem prover)" whose articulation with the translator is unclear to me. But automated theorem proving — the part that "actively wants to put us out of business," certainly a radical transformation of "mathematics itself" — is also on the agenda, as in this proposal:
artificial market mechanisms that allow arbitrary agents to bet on the status of mathematical conjectures while the agents are rewarded for correct predictions, proving theorems formally and for introducing interesting new conjectures.
I take it that "agents" and "reward" are terms of art in the deep learning community and that future algorithms will not actually be collecting our paychecks. I am deeply unqualified to comment on the technicalities that comprise the middle part of Szegedy's article. He takes the recent achievement of "human or near human performance" in computer vision as well as machine translation of natural language as precedents and anticipates that autoformalization will follow a similar trajectory. I can hardly deny that the rapid developments in both of the domains he mentions — thanks in large part to the recruitment of the entire online population as involuntary trainers — are extremely impressive and often useful, as well as thoroughly unsettling; to the extent that I understand how deep learning works in vision and machine translation I assume that the three models in Szegedy's system proceed by combining random nudging with a correction process based on comparison with the expanding formalized corpus. And I see no reason in principle — but as I say, I'm not qualified to see such reasons — why this can't succeed in generating a bigger corpus of formalized mathematics.
But the paper does shed some light on what the computing community may understand as "human-level." I have no stake in the formalization program and it makes no difference to me whether it’s carried out by fun-loving undergraduates or surly search engines. On the other hand, I am curious whether nudging of approximate translations according to the "exploration guidance model," and the analogous nudging of approximate proofs to generate new proofs of new conjectures, might lead to the creation of new competent "human-level" mathematical sentences. I am resisting the strong temptation to remind the reader that not all human mathematical sentences are equally consequential. The “surplus of meaning” that Grothendieck introduced transformed mathematics more radically than anything I can imagine algorithmic guided exploration might accomplish. But I am the first to acknowledge the limitations of my imagination.
Instead of replaying a moment of mathematical transformation that was undoubtedly human (and not superhuman), I will devote Part II, (hopefully) one week from now, to an outstanding performance of human mathematics that I was fortunate enough to witness a few months ago. The qualities I intend to highlight in my report on this talk have nothing recognizably in common with those emphasized in Szegedy’s article.
My free translation. The original text: L’écriture grothendieckienne est portée par une conception atypique des mathématiques, décrite et théorisée dans des textes [qui]… témoignent avec vigueur de la part incontournable de poétique qui anime le travail scientifique et de ce surplus de sens que l’écriture formalisée croit bon d’évacuer, alors même que là gît l’essence de la pensée mathématique. I discovered this quotation in Yves André's book Dix regards sur la mathématique contemporaine, which I will review in the future, from the perspective of this newsletter.
I thank Justin Clark-Doane for pointing me to the work of Kit Fine, which (roughly) sees essences in terms of definitions, and about which I may have more to say in the future.
Ian Hacking’s book Why Is There Philosophy of Mathematics at All? includes 2 1/2 pages of dictionary definitions from a dozen languages. For the first assignment in the course I taught last fall, I asked students to write down their own definitions of mathematics; of course no two were the same. My first lecture in that class proposed seven unconventional definitions, of which my favorite, based on a quotation from Cardano that I found in Barry Mazur’s book Imagining Numbers, is “the viewpoint that enables mental ease rather than mental torture.”
Formalizers not afraid of blisters should read the second page of Lakatos's Author's Introduction.
Szegedy deserves some sort of prize for his use of the word "just"…