Can mathematics be both meaningful and rational? Disagreement persists.
Can mathematics be both meaningful and rational? Disagreement persists.
The upcoming Fields Medal Symposium, Part 2
The need of reason is not inspired by the quest for truth but by the quest for meaning. And truth and meaning are not the same. The basic fallacy, taking precedence over all specific metaphysical fallacies, is to interpret meaning on the model of truth.1
According to [18th century Scots philosopher Thomas] Reid machines, like paintings, birds, or human beings, were capable of exhibiting signs of intellectual “excellence” and hence of eliciting love. He called this sense of beauty “rational” rather than instinctive, for its correspondence with “some latent perfection of which that beauty in the object is a sign.” Sensing it required training, like that of an expert mechanic. Confronted with an apparatus suited in every detail to the purpose for which it was designed, the mechanic “pronounces it to be a beautiful machine.”2
This is the second part of an essay written in preparation for the upcoming Fields Medal Symposium. It begins with a long digression about the purely philosophical implications in the formalizers’ approach to mathematical rationality. Those who are only interested in automation of mathematics as a new toolbox may wish to skip this digression. First, however, here are a few quotations from the first essay on Silicon Reckoner, in a (probably futile) attempt to dispel lingering misconceptions about its aims.
First, very much aligned with Venkatesh’s stated purpose:
I will not say things like "this [fill in the blank] is not mathematics." Instead, I will share my thoughts on what it means to say and on who is entitled to say "this is" or "this is not mathematics," and I will attempt to track how the consensus regarding the boundaries of what qualifies as mathematics has shifted over time.
Next:
I will not predict that mathematicians will never decide en masse to submit to the discipline of automated proof checkers
nor will I predict that automated theorem proving will or will not work, not will I say that it’s a good thing or a bad thing, nor will this newsletter ever lend itself willingly to reductionist readings of this sort.
Finally, my objective has never been to stake out a coherent position in defense of or in opposition to a position that has already been formulated in defense of or in opposition to the mechanization of mathematics. If I give voice in this newsletter to skepticism about the more grandiose claims of the mechanizers, it’s primarily because it’s precisely such claims that receive the preponderance of attention in the media, for reasons that deserve to be explored.3
What does it mean to say that mathematics is rational?
One measure of value, the “construction” of which is the focus of Venkatesh’s essay, is the extent to which mathematics is rational. Mainstream philosophy of mathematics tends to conflate mathematical rationality with what I have persisted in calling the Central Dogma. The charitable explanation of the easily observed failure of most mathematics to conform to this Dogma is that formalization is too much trouble; but I guess philosophers realize that most mathematicians couldn’t care less about formalism.4 They view us, therefore, as having inadvertently discovered a rich metaphysical treasure whose true significance is lost on us, like the Australopithecus who picks up a piece of gold without realizing that it is money.
There is more than one way to talk about rationality in mathematics. The first version of David Corfield’s chapter in Circles Disturbed was entitled “How Mathematicians May Fail To Be Fully Rational”, replaced in its final version by “Narrative and the Rationality of Mathematical Practice.” Corfield was seeking a version of mathematical rationality consistent with Alasdair MacIntyre’s conception of a “tradition-constituted enquiry.”5 He quotes MacIntyre approvingly, notably in this excerpt from his earlier draft:
The participant in a craft is rational qua participant insofar as he or she conforms to the best standards of reason discovered so far, and the rationality in which he or she thus shares is always, therefore, unlike the rationality of the encyclopaedic mode, understood as a historically situated rationality, even if one which aims at a timeless formulation of its own standards which would be their final and perfected form through a series of successive reformulations, past and yet to come.6
This is not incompatible with the view of mathematical rationality shared by “much of the Anglo-American philosophy of mathematics” — the Central Dogma, in other words — for which
the mathematician’s work is taken to be solely of interest insofar as in consists in deducing the consequences of various axioms and definitions… [a] view of the discipline, with its strong focus on aspects of mathematics that do not feature largely elsewhere – its use of deductive proof, its supposed capacity to be captured by some or other formal calculus, the abstractness of the objects it studies.
Corfield’s article, however, takes issue with this view, and takes inspiration from MacIntyre to formulate an alternative version of rationality that escapes the limits of formalism, and highlights the craft-like aspects7 of mathematical practice. Although Corfield wisely avoid using the word “meaning,” which is too coarse to be of use for his philosophical purpose, for the sake of this essay I will presume that his aim is to reconcile rationality in mathematical practice with the way mathematicians talk about our work as if it possessed some meaning that cannot be captured in a string of symbols in a formal language.
Logical confusion
…convention coerces a real self into behaving inauthentically… According to [Maurice] Bloch, it is precisely through formalization that coercion is exercised: “formalised language, the language of traditional authority,” he writes, “is an impoverished language; a language where many of the options at all levels are abandoned so that choice of form, of style, of words and of syntax, is less than in ordinary language.”
(Talal Asad, Secular Translations, p. 102)
In talking about rationality in this way, Corfield is contending with the antinomy that is the curse of philosophy, namely that life is change and the rationality of that which is changeable cannot be expressed rationally, if one requires rationality to meet the standard of timelessness (that last point is a tautology),8 to be "encyclopaedic" in MacIntyre's expression. Whether or not the rationality of mathematics actually "aims at a timeless formulation of its own standards" — even it is "historically situated" — is a matter no one can decide in a timeless fashion, since the rationality doesn't speak for itself and therefore where it is aiming can only be inferred, in various ways, from what it does. The stories one most often encounters are those told by philosophers who take it upon themselves to speak on behalf of mathematicians, whose job doesn't require them to deduce from their practice what makes that practice rational. And since most English-language philosophers learn about mathematics from the same book, or so I have been told, it’s hardly surprising that the Central Dogma figures centrally9 in most versions of the story.
For the philosophers who adhere to the Central Dogma, the “timeless formulation of …standards” at which the rationality of mathematics aims is precisely its aspiration to be expressed in a language that admits formal verification. This perspective leads to logical confusion on the part of the Central Dogma’s promoters among mathematicians.
I had written in an earlier post that
I’m not denying … that a procedure can be devised to transform human text systematically into Lean. But I do emphatically deny that this in any way resolves the epistemological conundrums that ostensibly motivate some of the most vocal of the formalizers, those who are most clearly attached to the Central Dogma. It literally makes no sense to claim that Bloom’s original proof and its formalization in Lean are the same thing, because it is impossible to define a procedure for verifying that a sequence of formulas is a formalization of a human proof. Even attempting to prove the validity of such a procedure would lead to paradox. Formalization would be superfluous if that weren't the case. (Emphasis added.)
Choosing to read a formalization as the same thing as the human proof, therefore, required an “act of faith”:
Formalization can only eliminate the epistemological antinomies if humans are excluded from the process entirely, and the machines are left to sort it out among themselves.
In the middle of an exchange about condensed mathematics on the Zulip Chat Archive, Jireh Loreaux accused me of missing the “key distinction” between the “act of faith” required to accept the definitions in a formalization and the “act of faith” implicit in accepting an unformalized human proof.
It can only be because they have been taught by the Central Dogma that a mathematical proof is always already implicitly formalized that mathematicians like Loreaux can fail to grasp my elementary logical point about translation — that if a human proof can be proved to be logically equivalent to a formal proof then the human proof was already formalized.
Or, more formally: let F be a formula in language H, let T be a transformation (formal translation) from language H to language L, and let P be a proof of the formula T(F). Then P(T) is a proof of F. Maybe going by way of L provides more confidence that F is correct, but it doesn’t change its epistemological status.
I asked the philosopher Colin McLarty, who will be on hand at the Fields Medal Symposium, how anyone trained in logic can miss this point. McLarty replied that
I have long experience trying to get people to see a certain tension in the idea of "already implicitly formalized," but it is deeply felt as a triumph of 20th century logic and so people do not want to give it up.
Earlier in the same Zulip thread, Peter Scholze had already put his finger on the antinomy:
I guess I'm just currently feeling that mathematics remains a human activity, because if I were to truly check that the computer did the right thing, I would have to unravel the whole proof in my head and convince myself that it all adds up.
What he means by “truly check” corresponds to rationality in Corfield’s sense, and not to a formal translation T. A proof in a living human head is meaningful; it is exactly what is not “already implicitly formalized,” and there is no procedure T that makes it so. But a philosopher who attempts to make a rational case for this kind of meaning will be bitten by the very same antinomy. This is why I predict that not much attention will be given to “meaning” in Toronto, although I can think of no better way to talk about value in mathematics.
Benefits?
But there is a third consequence to this method of dealing with a proposition. That proposition is a proposition. It is a proposition that is a proposition. It is a proposition that is a proposition. If, on the other hand, a proposition is a proposition, we could prove and prove that a proposition is a proposition by reason. But, because a proposition satisfies these two conditions under respect to a given proposition, we thus satisfy the following conditions: (1) if there is a proposition, and it is a given proposition, we can prove from that proposition the existence of a given proposition. (2) if there is a proposition, and it is a given proposition, we can prove the existence of a given proposition. (3) if a proposition satisfies a condition 1, 2, 3, 4, 5, 6 and every other condition of a given proposition. Hence, all propositions except the one of P. are considered by reason as propositions as being given by reason. If the proposition of P is taken to be a proposition, we accept it as being a proposition. There would, obviously, be a second proposition. For instance, if the proposition of S was a proposition that is a propositional proposition, we can prove the existence of S from that proposition by the formula (1) (N.B.*S).10
In the article I reviewed a year ago, Christian Szegedy suggested creating translations of human proofs automatically by machine learning. This is how AI has got so effective at object recognition and automatic translation between human languages: by instantaneously generating a zillion possible translations (or objects), giving each of them a score by some probabilistic method, and then offering the translation with the highest score.
Szegedy doesn’t mention Bayesian probability, but if that’s the method used then the procedure is not unlike the way mathematicians reach consensus on the value of a research direction, on the model Venkatesh sketches. The process includes a step of revising the prior probabilities after comparison of the output with the target, presumably by checking whether T of a proof in H is a valid proof in L. This is all well and good, but the epistemological antinomy is intact. Statistical verification has bypassed formal rationality and the output is not provably a translation of the human proof but only very probably so; only by an act of faith can the validity of the original human proof be deduced from the formal validity of the formal proof.
With this in mind, I look forward to Johann Commelin’s talk in Toronto next week, in which he will explain his contention “that formalization of mathematics is delivering benefits right now.” I hope I’ve made it clear that I doubt that the benefits include clearing up the epistemological misgivings that motivate at least some of the adherents of the formalization program. I’ve also explained in the past that I don’t see how formalization will have any effect whatsoever either on my practice of mathematics or my participation in what Venkatesh called the “construction of value.”11 But I’m willing to be convinced otherwise.
I am once again deeply impressed by Jim's versatility. In the past few years Jim has begun to take on the leadership role that corresponds to his place in the field.
He has a great impact on the world of dance and holds a firm place as one of the world's most powerful leaders for dance.He is one of the most creative and open-minded number theorists of his generation, and I recommend him enthusiastically.
In his own nomination, Leon Sperling states, "I am honored to nominate Jim.”
(Crossed-out text inserted by the InferKit demo into the concluding paragraph of an old letter of recommendation — the name of the candidate has been changed to Jim. Is automation of writing reference letters for jobs on the near-term agenda? How about reading the letters?)
Challenges for humans
the achievement of ritualized practice is itself essential to what the self becomes, helping to form or to deform it. (Asad, p. 103)
While we indulge in dreaming of a future in which human mathematics has been altered beyond recognition but not killed, we should not lose sight of the present. I have already listed several goals for this Substack newsletter in the five numbered items in the first year’s final entry. Each of these is worth bearing in mind, I think, while reading Venkatesh’s essay or attending the talks in Toronto, and I’ll try to work them in during the Symposium’s closing panel. Here I want to close by raising a few very different issues suggested by Venkatesh’s essay.
Question: The merit of analyzing developments in mathematics in terms of “construction of value” is that it forces us to confront the actual history of our practice, including current history, rather than an idealized history devised to satisfy external observers (philosophers, computer scientists, legislators, or the occasional Ultra-High Net Worth Individual donor). The risk is that seeing value as “constructed” leaves us bereft of a consistent answer to the question: “What are you doing it for?”
The other day a dancer asked me just that question, in just those words. I parried the dancer’s (by no means hostile) question with the obvious rejoinder: “And what are you dancing for?” I was not asking the dancer to conclude that the two of us are part of the same struggle to extract from the morass of everyday life some ineffable but marketable quality of beauty or enlightenment or grace — not that I disagree with such a conclusion. It was rather to express my sense that the question is one that addresses itself unceasingly to each of us and that it’s not up to outsiders to impose on us a prefabricated answer. A crypto billionaire, for example, may hold that proof is for the verification that some chunk of cryptocurrency really does belong to the entity that claims ownership, and would then see improved automation of proof as a way to make the system work more profitably. The “us” to whom Venkatesh’s essay is addressed will want to keep these motives in mind but should by no means feel bound by them.
To my mind the most valuable outcome of the Fields Medal Symposium would be to make the mathematical community more conscious of these stakes.
Question: Although the Fields Institute gave next week’s event the title “The Changing Face of Mathematical Research,” Venkatesh’s title included the word “Automation,” and since that was the sole focus of his essay the organizers decided that this would also be the primary focus of the Symposium. Thus the implications of Venkatesh’s original title — “Approaching Obsolescence” — will remain as a constant subliminal menace.
Other developments in technology, however, that promise to postpone the expiration date of human mathematics indefinitely, will not be treated in the Symposium, although they mesh with the Fields Institute’s title. Facebook has changed its name in line with its contention that its survival is tied up with virtual reality. Though there have been a few efforts12 to develop VR as a teaching resource, it has generated nothing like the interest in formalization or automated theorem proving. Yet in principle VR ties human practitioners ever more tightly to the future of mathematical research. The future may look more like geometers going with the Ricci flow and proving the Poincaré conjecture by hands-on manipulation of the geometry — with real virtual hands! — than like a vestigial mathematical priesthood awaiting an oracular mainframe's disclosure of yet another proof that no human will understand.
I make no bets on the outcome of the titanic clash looming between Meta and Alphabet.13 For those inclined to bet, however, let this serve as a reminder that binding your imagination to the Central Dogma may not only be philosophically unwarranted; it may also blind you to opportunities to make real (and not only virtual) money!
Since two essays were published this week, the next essay will appear approximately four weeks from now.
Hannah Arendt, The Life of the Mind, I.
Reinhold Martin, Knowledge Worlds: Media, Materiality, and the Making of the Modern University, Columbia University Press (2021), p. 45.
Which means, in particular, “follow the money.” Of course that’s not the whole story, but it’s a larger part of the story than some readers might think.
See note 11, below.
Angus MacIntyre, Three Rival Versions of Moral Enquiry, Duckworth.
This text generation website autocompleted this paragraph as follows:
My impression is that Corfield was coming from a distinct tradition: His preferred philosophical perspective, I think, is hedonistic. Mathematicians should think about their purposes and decide to do mathematics for the sake of pleasure. Corfield’s hedonism seems to me to be a more relaxed version of an adherence to Aristotle, Plato, and the early Scholastics who viewed mathematics as being rightly or wrongly deduced from the requirements of the philosopher.
My own view is that the hedonist approach is generally to be preferred: Mathematics is not necessarily a rational endeavour, but rather an inquiry into the nature of mathematical inquiry. And if there is anything hedonistic about mathematics, I believe it is the openness of the question: Mathematics is a kind of construction, and it is open to a number of possible meanings that are open to some reinterpretation, but I don’t think these reinterpretations will radically change the nature of the question or its outcome. As a question, the question of rationality is still pretty tough: That’s one of the reasons I favour a hedonistic approach over a Platonic one. But as a way of understanding, mathematics should be open.
See the discussion of craft in this earlier essay.
This is not the place to talk about dialectical logic.
As the position with which must be addressed, whether or not one agrees with it.
Text created by DeepAI, based on the GPT-2 model by OpenAI, in response to the prompt “automated theorem proving.” By posting this I am arguably not adhering to my commitment to “presenting positions with which I disagree, especially those with which I disagree most vigorously, in their strongest form.” But in this case I’m not sure how to state a position with which I disagree.
The response of Peter Woit’s colleagues at the end of this post on Not Even Wrong suggests that my perspective is widely shared — of course this doesn’t mean it’s right!
Familiarly known as Facebook and Google.