The Central Dogma of Mathematical Formalism
The Central Dogma of Mathematical Formalism
and its first $20,000,000 Center
It is very difficult for us to understand truth.
Eric Schmidt, Executive Chairman of Alphabet (Google), November 2017
I’ve always thought it very regrettable and, in a sense, also foolish, that the philosophers decided somewhere in the nineteenth century that metaphysics wasn’t a respectable discipline and had to be thrown overboard, and reduced themselves to becoming logicians and statisticians. It seemed a very poor diet, somehow, to me.
W. G. Sebald, from The Emergence of Memory: Conversations with W. G. Sebald
Today’s title was inspired by a lecture by Giuseppe Longo at last January’s online conference on philosophy and mathematics organized by John Cruz Morales and Silvia de Toffoli. Longo described formalism in mathematics as a precursor of the Central Dogma of Molecular Biology, which was formulated in 1958 — with the name Central Dogma — by Francis Crick.
It must be terrible for a mathematician to have a point of view. If I had a point of view, I would feel compelled to defend it, and following the habits acquired during my professional socialization that would mean attempting to construct something like a rigorous proof that my point of view is correct.
Values are a different matter. Even a nihilist has values, if only the value of rejecting all values, and usually that’s OK. Each of us brings our values acquired through arduous reflection to the society of tolerance of which the liberal university aspires to be a microcosm,1 and in the spirit of tolerance we learn about each other’s values and keep our value judgments to ourselves. By articulating them in essays like the one you are now reading I continue to learn about my own values as a mathematician. You may decide that you do not have the slightest sympathy for my values, but by reading about them you learn that mathematics is sufficiently broad-minded to allow people with my values, or at least one such person, to participate in its society. You may conclude that my values are completely irrelevant to whatever I may have achieved in my practice as a mathematician, and that I am deluded to think otherwise, and that’s OK too. Please keep this in mind when you read my thoughts about what I will be calling the Central Dogma of Mathematical Formalism, and about the mathematicians who adhere, or claim to adhere, to that Dogma.
Readers who have never spent an hour convincing an audience of professional skeptics that they have correctly proved a difficult theorem will have missed the thrill of universal acknowledgment that they were right, at least this one time, and cannot imagine how intensely validating this experience can be. But it can also be addictive, and one does get the impression that some people go into mathematics because they crave acknowledgment that they are always right. This can lead them to mistake their values for points of view and therefore conclude that everyone who is serious about … [whatever the issue happens to be] … must necessarily share their values.
Mathematical formalism, as encapsulated by its Central Dogma, to be discussed below, is a legitimate value. So are the ethics based on religion. The problem arises when formalism, or religious ethics, rather than being offered as a (personal) value, is mobilized to support the point of view that it is of universal validity.
The Central Dogma of Mathematical FormalismFor 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 unsubstantiated2 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.” This is an absolute judgment, a gesture toward a rigorous proof — that of course we will never see — of the point of view expressed by the Central Dogma. That ambiguous word “tantamount” in the next line is more like a confession that Avigad is wavering in his adherence to the point of view, like Jasmin Blanchette, Principal Investigator of the project Lean Forward, funded by the Dutch Research Council, when he writes
Too many proofs look more like LSD trips than coherent mathematical arguments.
One likes to imagine that Blanchette has enough personal experience of LSD trips and coherent mathematical arguments to be able to tell the difference. But is the difference as clear-cut as Blanchette thinks? Phil Lesh, the late3 bassist of the Grateful Dead, once offered this characterization of music, or of life, or of both, in terms that could apply just as well to mathematics:
In life, as in art, there are recurring themes, transpositions, repetitions, unexpected developments, all converging to define a form that’s not necessarily apparent until its ending has come and gone.
In the course of a Twitter thread whose thrust is to question the “only if” of the Central Dogma,4 Gowers nevertheless allows that formalization is sufficient for “getting” a proof :
If you have formalized your proof in a language such as Coq or Lean, then you've definitely got a proof. (@twgowers, 20.08.2021)
This hardly seems controversial, but I have a problem with the image. In the first place, it’s very much bound up with the present historical moment: Euclid obviously wouldn’t have known what to do with a formal proof in Coq or Lean, but we also shouldn’t assume that 20 years from now a proof in one of today’s formal languages will be more legible than a betamax videocassette.
I also find the choice of verb odd: “getting” sounds rather less active or even participatory than what usually counts as mathematical practice. My main objection to the sentence, though, is that it depicts the proof as an artifact, whereas I prefer to conceive of a proof as a social process. And lest that last sentence be dismissed as mere verbiage, I take the liberty of quoting myself to explain what I mean:
a proof like the one Wiles published [of Fermat’s Last Theorem, ed.] is not meant to be treated as a self-contained artifact. On the contrary, Wiles’ proof is the point of departure for an open-ended dialogue that is too elusive and alive to be limited by foundational constraints that are alien to the subject matter.
The Central Dogma set (literally) in stone
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. Charles Hoskinson’s speech at the opening of his eponymous Center at Carnegie-Mellon University5 is simultaneously a pure expression of the messianic vision that characterizes the tech industry and an outline of the project to use the economic power of that industry to “transform” the future values not only of mathematics but even of “wannabe mathematics”:
It’ll keep growing the endowment until it’s an Institute, and then eventually it’ll become a very large distributed community, it’ll leave the safe harbor of CMU and go to Africa and go to Europe, go to South America, go to Asia, all around, hundreds and eventually thousands of mathematicians or wannabe mathematicians will grow up with the tools built here, will grow up with the knowledge derived here, and a completely new language of mathematics will evolve, one that is a bit more complete, a bit more special, and a bit more descriptive.… Now we get to do it [i.e., relive the early 20th century foundations crisis, MH]… maybe another Bourbaki-style moment, where we can cover the entire pedagogy of all the fields of math and have open-source textbooks with this paradigm, and then… more and more will publish with this paradigm, more and more journals will begin following this paradigm, it will transform all kinds of things, even the notion of peer review itself… and eventually the entire domain, tens of thousands of man-years of effort, will be invested towards the things that are established here.
I can’t begin to tell you how glad I was to find this talk, because it saved me the trouble of writing a whole paragraph’s worth of imputed intentions,6 while highlighting a point I’ve been trying to make ever since 2011, when I first heard Vladimir Voevodsky predict that within five years — by 2016, in other words — no serious journal would accept a mathematical article that was not accompanied by a formal verification of the kind required according to the Central Dogma. My point, then as now, is that it’s not enough to assert a Dogma, as Voevodsky did then and as Avigad did more recently, in order to impose it as a “paradigm,” to borrow Hoskinson’s vocabulary. The Dogma has to conform to, or embody, the existing values — “virtues,” in Alasdair MacIntyre’s language — of the practice.
Nevertheless, in order to “persevere in its being,” as Spinoza puts it, the practice of mathematics requires what MacIntyre calls external goods as well as internal goods. A sudden massive infusion of external goods, in the form of money, or a Center (or as Hoskinson seems to prefer, an Institute), can forcefully nudge the practice of mathematics in the direction of a new paradigm. (You may call this a “distortion” of the values of the practice — but for me to do that would be to express a point of view, an encumbrance of which I am blissfully innocent, as I have already explained.)
What some people like to call the progress of mathematics has always consisted in the subversion of paradigms. Pierre Deligne made this point in a lecture on Voevodsky’s univalent foundations: he said it reminds him of Orwell’s Newspeak, where the ideal was to have a language where it is impossible to express heretical thoughts. The paradigm the Hoskinson Center promises to bring into being may well be nailed in place by “eventually thousands of mathematicians or wannabe mathematicians.” I am nevertheless confident that human creativity, and the Spinozian conatus of mathematical practice, will undermine it sooner rather than later.
But even if it doesn’t permanently “transform” mathematics with a “completely new language,” it will protect Hoskinson’s High Value Assets:
The ideas generated here can be commercialized in that we can create a marketplace for deduction.… the correctness of software turns out to be the exact same type of problem, isomorphic in a certain respect, to the correctness of a mathematical proof. It’s just that you have to look at it a little bit differently.
There is a sense in which this is absolutely correct, and I’ve referred repeatedly7 to Donald MacKenzie’s Mechanizing Proof for an account of the history of how the pursuit of this objective influenced the project of mechanization of mathematics. There’s a deeper sense in which this “isomorphism,” like the Central Dogma itself, is totally misguided. That sense is what I have been pursuing in this newsletter, but unfortunately the argument doesn’t fit in a few sentences, and a concise expression will have to wait.8
Panic
A few weeks ago I was “thumbing” through a new digital “preprint” when the following line left me numb with panic:
This contradicts Harris’s Theorem 2.5.6 in (etc.)
My first thought was: I have made more than my share of mistakes, many of them in print, but surely that paper was safe! (Denial is the first stage of grief.) Looking over that paper again, more than 30 years after its publication, was the last thing I wanted to do that morning, but I knew I would not be able to evade my responsibility. So in a state of considerable irritation (Anger is the second stage) I downloaded my old paper and “turned” to the offending page. What I saw was a jumble of symbols whose meaning was long-forgotten. It would take me weeks, I realized, to reconstruct whatever I had been thinking long ago, back in the days of Reagan and Thatcher, and there was no guarantee of success. With irritation giving way to a second wave of panic, I returned to the new preprint, straining to find a flaw in the reasoning that led to their contradiction of my theorem. My task seemed hopeless, because the line that caused me such distress came at the end of nearly 100 pages of dense and difficult arguments that in turn relied on more than 100 publications, most of which I had not read.
One claim didn’t look right, though. Turning it over in my mind, and making my best guess as to the meaning of the authors’ notation, I convinced myself, in a way I will outline below, that the claim could not possibly stand in the intended generality. I started writing to one of the authors to point this out (I had reached Bargaining stage), putting together the sequence of steps as in their text, when it suddenly dawned on me: the sentence that had ruined my morning was in fact the conclusion of a reductio ad absurdum, or proof by contradiction! The strategy of the preprint was to posit the opposite of what they wanted to prove and to show that it led to a patently absurd conclusion, namely one whose absurdity consisted precisely in presuming to contradict my long-settled Theorem 2.5.6. Far from questioning the veracity of my Theorem, the authors were using it as their ace in the hole, playing their last card on the very last page of their paper.
My immediate reaction was profound relief, but it could just as well have been elation. Theorem 2.5.6 was a red line, a sentinel that brooks no contradiction, and I had placed it on the border that separates truth from confusion, now and forever. The point I want to make here, though, is that at no time did my panic have anything to do with the Central Dogma of Formalism. This is not because a small but persistent mathematical subculture rejects the law of the excluded middle, and thus the principle of proof by contradiction. The reasoning that put me back on track was entirely heuristic, in keeping with a position I once suggested as an alternative to the Central Dogma:
Unlike those of my colleagues who predict that computers will soon replace human mathematicians by virtue of their superior skill and reliability in proving theorems, I am inclined to respond that the goal of mathematics is to convert rigorous proofs to heuristics. The latter are in turn used to produce new rigorous proofs, a necessary input (but not the only one) for new heuristics.
(Note that this is presented as an inclination and NOT a point of view.) Here is the heuristic used to complete the proof by contradiction. The authors needed to show that a unitary representation of a certain group could not have an undesirable property. The (very ingenious) argument deduces from the undesirable property that one of the parameters classifying their unitary representation can be taken to be unbounded. But it is a basic principle that one of the parameters classifying the unitary representations of that group belong to a bounded set. My Theorem 2.5.6 is a precise version of this heuristic in the case at hand, and a convenient reference, but when I saw that the authors could just as well have cited the basic principle, and there was no need to go to the trouble of citing my specific theorem, I realized that I had misread their intentions.
As this episode illustrates, I am hardly a model of systematic, coherent, and focused thought. But maybe that’s a point worth noting.9 It may be possible to train an AI to read the full proof in order to realize that the authors’ contradiction of my Theorem 2.5.6 is not to be taken as a conclusion but rather to be bracketed within the framework of a reductio ad absurdum. It’s more difficult to imagine an AI finding its way to the correct interpretation by means of the heuristic based on its common sense, analogous to the enhanced version of the Turing test known as the Winograd Schema Challenge and exemplified by these two tests of language comprehension found on the website commonsensereasoning.org:
The trophy would not fit in the brown suitcase because it was too big.
Q. What was too big?
The trophy would not fit in the brown suitcase because it was too small.
Q. What was too small?
Central dogmas and literary intellectuals
Ever since high school I’ve been a big fan of molecular biology, and I was close to the front of the line a year ago when the first messenger RNA vaccines were made available at the stunning Fort Washington Armory in New York. I wonder, though, whether Crick anticipated a backlash on the part of literary intellectuals when he chose10 “dogma” as the name for his postulate:
…once “information” has passed into protein it cannot get out again. In more detail, the transfer of information from nucleic acid to nucleic acid, or from nucleic acid to protein may be possible, but transfer from protein to protein, or from protein to nucleic acid is impossible. Information means here the precise determination of sequence, either of bases in the nucleic acid or of amino acid residues in the protein.
Crick’s formulation attempts to constrain the use of the word “information” with a precise definition, but once the dogma entered the public domain, “information” recovered its plasticity as metaphor for everything — “the fundamental core of things,” as James Gleick put it. Opposition to dogmas of all kinds is a value cherished by intellectuals, especially those nourished on critical theory. Crick’s Central Dogma of Molecular Biology, which grounds its own billion dollar industry, is no exception; — because it is often taken as a license for genetic determinism,11 but also because it forces research along directions consistent with the metaphor while foreclosing others, as Nadia Abu al-Haj points out:
By the turn of the millennium, the Human Genome Project had produced a sequence of the human genome. But in the aftermath of its success, geneticists have become increasingly convinced that knowing the sequence does not get us very far. Scientists began inquiring into how genes are actually expressed. What are the processes by which the “genetic code” generates proteins? Rather than focus on the genome and its genetic code, scientists are increasingly turning to analyze the cell apparatus as a whole. In the paradigm shift from mapping and sequencing the genome (genomics) to the study of development, function, and expression (post-genomics), the gene as “the central dogma,” as the informational code from which biological expression and function proceed, has been challenged. Knowing the code cannot give an adequate account of life. It cannot give an adequate account of the development, growth, health and illness, and death of a living being.12
Change a few words in Abu al-Haj’s critique of the extension of the information metaphor, especially the last two sentences, and it becomes an effective retort to the Central Dogma of Mathematical Formalism, provided one is willing to accept the metaphor of mathematics as a living community rather than the version of the formalist metaphor that sees it as an inert body of intrinsically meaningless texts.
Literary intellectuals have picked up on “the emancipatory potential of epigenetics” in the hope of undermining Crick’s Central Dogma. The expression in quotation marks is taken from a book by Clare Hanson entitled Genetics and the Literary Imagination. Here is the complete quotation:
…the emancipatory potential of epigenetics has been emphasized by philosophers of biology, especially those who have resisted what they see as the limitations and distortions of neoDarwinism. Evelyn Fox Keller, for example, sees discoveries in epigenetics as changing the very meaning of the genome, transforming it 'from an executive suite of directorial instructions to an exquisitely sensitive and reactive system that enables cells to regulate gene expression in response to their immediate environment'. For John Dupré, epigenetics has been crucial in breaking the hold of the so-called Central Dogma and in demonstrating the diversity of forms of inheritance at the molecular level. However, the most ambitious philosophical approach to epigenetics is that of [Catherine] Malabou, who aims to harness the insights of contemporary biology in order to transform philosophy itself. … for her the importance of epigenetics lies in the fact that it demonstrates the porous boundary between the organism and the environment and shows that the living being does not simply perform a programme, rather, 'the structure of the living being is an intersection between a given and a construction'.13
While readers wait for the Central Dogma of Mathematical Formalism to come to the attention of colleagues in Comparative Literature departments, I invite them, in the spirit of the Winograd Schema Challenge, to guess where the word “mathematics” can be substituted in that last Malabou quotation.
Comments welcome at Mathematics without Apologies.
I naively expected to find an expression of this attitude on my own university’s website, but this is what showed up instead:
Columbia’s actual mission statement is too prosaic and matter of fact to reproduce here, but it does express the value of “advanc[ing] knowledge and learning at the highest level and convey[ing] the products of its efforts to the world.”
I no longer believe that the word “militant” is justified in this sentence. I do defend the use of “unsubstantiated” if the quotation is meant as an actual description of the “state of affairs” in mathematics, as opposed to a philosopher’s rational reconstruction. This is explained in detail in the entry entitled “Best to equivocate on professional norms.” I apologize to Jeremy Avigad for misrepresenting his intentions.
This observation was added on October 26, 2024, the day after Lesh died. The quotation is from a 2005 article by Lesh in the Denver Post.
…while simultaneously arguing that the “leap from the fact that we have a formal notion of proof to the romantic idea that mathematics is perfectly democratic: it doesn't matter who you are, because if you've proved something you've proved it” betrays a misunderstanding of the social nature of the discipline. This is a welcome argument, especially because Gowers concludes that “It is perfectly possible for a discipline as a whole to be unwelcoming/problematic for certain groups even if most practitioners of that discipline feel no hostility towards those groups.” But it is not directly related to the points I’m trying to make in this week’s essay.
He’s honest. “I found out I liked money a little bit more than math” (at 1'09'').
Teen Vogue has already spared me the trouble of explaining how billionaires’ accumulated wealth can be transformed to a public good.
In the middle of this newsletter, for example. That article also predicted that Peter Scholze’s liquid tensor challenge on Kevin Buzzard’s Xena blog would be seen in retrospect as a turning point, so I was not at all surprised to hear Hoskinson cite both Buzzard and Scholze in explaining why he chose to endow a Center based on Lean at Carnegie-Mellon.
As will my reaction to Hoskinson’s plan to solve the problem of “diversity” with “better tools.” Someone else will have to unpackage his claim (at about 11'15'') that “the soul of the company is in Africa.”
Indeed, the subtitle of How Mathematicians Think, an enlightening book by William Byers, is Using Ambiguity, Contradiction, and Paradox to Create Mathematics.
“Legend has it that the term dogma was originally meant as a joke,” according to the semiotician Jesper Hoffmeyer. Richard Lewontin takes the expression semi-seriously when he writes that “Molecular biology is now a religion, and molecular biologists are its prophets.” He adds, commenting on the habit in the early 90s to refer to the human genome project as “the biological grail,” that “It is a sure sign of their alienation from revealed religion that a scientific community with a high concentration of Eastern European Jews and atheists has chosen for its central metaphor the most mystery-laden object of medieval Christianity.”
For example, H. A. Burbano writes that the “doctrine” of “[g]enetic determinism at the molecular level… emerges from Crick’s central dogma and its underlying instructiveness.” The pernicious effects of the information metaphor show up in recurrent attempts to ascribe the underrepresentation in mathematical research of certain groups — especially women — to evolutionary dynamics, or simply to genetic predispositions.
Nadia Abu Al-Haj, The Genealogical Science, p. 10.
Clare Hanson, Genetics and the Literary Imagination, p. 174.