What it is that we do

This post is a follow-up on some somewhat off-hand comments that I made earlier regarding the notion of truth in a “proof-based” discipline such as pure mathematics or theoretical computer science. Since the former is easier to circumscribe and also has a larger literature available on it, for the purposes of the post I will discuss my emerging take on truth in mathematics; what I say applies to TCS as well. (I wasn’t able to find satisfactory writings on the practice of computer science, even more broadly interpreted than just “theory”; any pointers on this are very welcome.) I obviously don’t claim any originality here; I suspect that to some the points I make might be interesting while to others they could feel passé–in the latter case, please help me make progress in the comments!

A circle is a plane figure contained by one line such that all the straight lines falling upon it from one point among those lying within the figure equal one another. (Euclid, Elements, Book I, Definition 15.)

The question is more interesting than it may seem. First, let’s set aside the Platonician answer that mathematics is about proving statements that apply to abstract objects. None of this makes sense: there is no such thing as an abstract object (What is an “abstract circle?” Euclid’s definition of an abstract circle exists, but that definition has nothing abstract; it is plain English—or well, Greek, which is no better). Neither is there anything fundamentally “true” about the statements that mathematicians make about these objects. This last point is made clear in Voevodsky’s retelling of the story that brought him to start his research program on univalent foundations: see in particular the paragraph starting with “The primary challenge that needed to be addressed” here. While a subset of mathematicians has been carefully examining the logical foundations of mathematics and pursuing a program of formalizing these foundations with the goal of automating verification, two facts are historically evident: (1) this formalization has always come after the fact, i.e. first the theorem is proven, and second only is there some attempt at modifying the format of the “proof” so as to reach some abstract “higher standard”; (2) what the higher standard exactly is is a moving target. In other words, mathematicians do whatever it is that they do first, and only after that does some subset of them look back on what has been done and make an attempt to reformulate it in a way that seems more “rigorous” by the standards of the day. And even once this process has been completed (or rather, iterated over a few times), no absolute truth has been obtained; merely, one has gained higher confidence that some set of formal rules can be applied in a certain order to derive one statement for another. In summary, the logical answer “I define as true any statement that can be derived by said rules starting from said axioms” will not satisfy us. (My point is not to criticize this enterprise; only to point that this is not what mathematics is about. I don’t expect any mathematician would disagree.)

Once this point has been cleared we have opened up the possibility for a much richer interpretation of what mathematics is about, what it is that mathematicians do, and what is so special about the role played by the notion of truth in this enterprise.

The Greeks

Mathematicians have been around since Greek antiquity. I highly recommend the wonderful book The Shaping of Deduction in Greek Mathematics by Reviel Netz, a historian at Stanford. The book provides a fantastic historical introduction to the birth of modern mathematics, as practiced in the Western world. In this book Netz gives a detailed account of the practice of Greek mathematics that is based on a sometimes almost comical literal reading of the original texts. Netz is not a mathematician, and he takes the Greek writings at face value, without preconceptions as to any deeper meaning, mathematical or otherwise. To see how fantastic an enterprise this might be I highly recommend taking the time to read through a few paragraphs of Euclid’s elements, see e.g. here. (I wasn’t able to find an online version that has clear figures; Netz’ book contains many reproductions and he spends a great deal of time examining their significance as a companion to the text.) Wait, and they called this a proof?

Netz places a particular emphasis on the role of lettered diagrams such as this one in Greek mathematicians’ proofs. This one is taken from Apollonius, as reproduced in this book.

What I find most amazing about Netz’ work is that his book makes it absolutely clear that what Greek mathematics did is invent a very special world, with its own set of rules and specifications as to how things should be presented, what counts as valid and what does not, etc; most importantly this set of rules and specifications is absolutely arbitrary. There is nothing universally true about any of the statements made in Euclid’s book ; what there is however, and which is just as important, is a form of self-consistent, self-perpetuating consistency. This is the Greek mathematician’s most important discovery, and most enduring legacy: a system of thought, based on the use of formal rules, such that users of that system of thought can easily and unequivocally agree on the same statements. Netz contrasts this with the political discourse that the Greeks were so famously fond of; while in rhetoric endless arguments can be made in favor or against any given statement, in mathematics once an argument has been made there is no discussing it; either the argument is correct and accepted by all or it is flawed and all will agree on the presence of a flaw. By saying that mathematics does not establish universal truths we do not take away any of the strength of its evident success as a system of thought.

I insist that in the previous sentence by “mathematics” I mean “Greek mathematics.” There is nothing universal about the formal “proof system” used by the Greeks, and in fact that system is arguably quite different from the one used today (contrast a proof in Euclid’s Elements from one in e.g. Kerodon (see figure below); clearly either school would reject the other’s papers!). There is nothing absolutely perfect or even fool-proof about it either; when I write that “either the argument is correct or it is flawed” I do not dismiss the existence of a substantial grey zone in which there might be, and generally is, discussion. (Netz in his presentation makes it plainly obvious that Greek proofs had many “gaps” and that completely arbitrary choices are made as to what is valid and what is not.) The point is that this grey zone is by orders of magnitude smaller than in other disciplines, and this is what makes mathematics special.

A lettered diagram taken from the proof of Lemma 3.5.3.11 in Kerodon.

Greek mathematics has its limitations. In particular, it seems like they were not able to expand their explorations much beyond geometry; possibly because they did not have a formal way of re-using proofs. Indeed, only propositions from Euclid’s elements were part of the general corpus of “truths” that could be used without justification; any other proof could only appeal to either a statement from the Elements or a statement proved within the same text (as opposed to a statement made by another mathematician). The current system has a much higher level of re-usability, allowing it to much deeper. It is possible that current attempt at formalization will provide yet another layer to this by enabling re-using statements without the mathematician herself even being cognizant of the statement that is being re-used (e.g. the proof assistant would figure out that there is some theorem somewhere that could be useful).

The moderns

A lettered diagram taken from the proof of security of quantum key distribution in Renner’s Ph.D. thesis.

Once one has taken this somewhat distanced look at the practice of Greek mathematicians it becomes clear that there is no reason for contemporary practice to escape similar distanciation. As arbitrary as the rules that govern the former might seem now, just as arbitrary our own rules will seem later. The observation prompts us to re-evaluate the notion of proof and truth as follows: The goal of the mathematical proof is to convince the mathematician; a statement is true whenever the mathematician is convinced. I emphasize that the mathematician in this sentence is a human being, not a machine.

Propositions in Euclid’s elements are true because Euclid’s text convinced all other Greek mathematicians that they were true; the same hold of Voevodsky’s univalent foundations. To speak about my personal experience, the point was carried home vividly about a decade ago at the end of an entire afternoon spent sitting by the sea nearby Marseille in the South of France together with an illustrious French operator algebraist. For the whole afternoon I had been trying to explain, of all things, the Clause-Horne-Shimony-Holt inequality formulated as a nonlocal game—an elementary construction on which half of my research is based (see this post for example, although we certainly didn’t get that far). To no avail! Alice, Bob, games, the mathematician would have none of it. How could it be so hard? The message I was trying to carry across is bread and butter to quantum information theorists; moreover the language of functional analysis was not foreign to me either and so I believed I ought to have more than it should take to make the explanations clear; in my mind I had a clear theorem, together with an airtight proof, to communicate. Not so: I ended the afternoon defeated, and the point hammered in: as much as we may think that our language is formal, our reasoning rational, our goals clear, as soon as we step out of our self-referential cocoon we have to face the evidence: not so; there is nothing clear, formal, self-evident, in the mathematical truths we take as such. (If you’re not convinced yet, look at the pictures.)

After having read through the viewpoint of a historian on Greek mathematics, it is interesting to come back to the present and read up on the modern mathematician’s own account of their practice. Having delighted in Hardy’s A Mathematician’s Apology in my student years I was naturally attracted to Harris’ explicitly referential book Mathematics Without Apologies. The book aims to provide a personal answer to precisely the same question as Netz’ (“What do pure mathematicians do, and why do they do it?”—first line on back cover), with the essential difference that Harris’ book is written by a contemporary mathematician about the practice of modern mathematics. The perspective taken is thus very different: Harris does not waste a drop of ink to examine the material products of modern mathematics (e.g. printed articles), which naturally from his point of view do not have the least interest besides their mathematical significance; nor does he question the formal system that enables mathematics (he does discuss foundation issues, but these are themselves part of the formal system).

Harris delights in telling us stories about the practice of mathematics from the inside: the way one acquires prestige (he calls it “charisma”), how mathematicians perceive when a mathematical statement is interesting, what drives a mathematician to work on one problem or another, the influence of large research programs such as the Langlands program, etc. Just as Netz, Harris agrees that the proof itself, while an important product of the mathematician’s practice, is not a goal in itself. The goal is to introduce new objects, find relations between them, and build structures that support this exploration (Harris quotes extensively from Grothendieck, a builder of structures if there is any). Crucially the mathematician’s goal is not at all to find truth: her goal is to find beauty. Harris (un-apologetically!) defends the mathematician’s position as playing a privileged and essential role in our (Western) society: mathematics is the rare, if not unique, discipline where thought is valued for itself: not for its consequences or potential applications, nor even for some kind of universal validity or truth that it might reach — for itself, the sheer beauty of it. No apologies. While one might think that the arts are in a similar position, Harris points out that in contemporary discussions about art the notion of beauty has all but disappeared; instead, one talks of society, ecology, politics—all of this is good and important, but it is not about beauty. Mathematics is about exploring the beauty of human thought. This exploration is carried out within the very special, narrow and arbitrary corner that mathematical practice has delineated for itself since the Greeks got us started. And yet does not matter that it is narrow and arbitrary; what matters is that it is purely and uniquely human.

I don’t have a conclusion to give to this post. I suppose it is the kind of digression that one is naturally inclined to make while on sabbatical. (I was delighted to see Harris reference his time at the Institut Henri Poincaré in Paris extensively and spend multiple pages gossiping about Ed Frenkel, then a holder of the same FSMP chair I am now occupying.) Certainly it helps to gain a sense of what it is that one is doing. While these explorations destroyed a number of simple comforting myths about what it is that I do every day, in the end I find the void that lies beneath the surface much more appealing; I feel privileged and comforted in my desire to make use of that privilege.

Post-scriptum

In addition to the two books referenced in the post there are a couple articles that I found helpful. I am listing them here because I found such writings non-trivial to come by, and so they might be helpful to anyone interested in the topic. I welcome additional references.

• Barton, Ethnomathematics and Philosophy. This is Barton’s Ph.D. thesis, in which he studies the social emergence of mathematics not as inevitable, but as cultural, yet without negating what is so special about it. .
• Wallet and Neuwirth, Enquete sur les modes d’existence des etres mathematiques (unfortunately in French only it seems). The authors build on Netz’ work and others to examine the notion of mathematical proof within Latour’s framework of “modes of existence,” which Latour mostly applied to experimental sciences.