Testing my beliefs

…preferably without giving offense

The moral: keep at least one hand free while sampling these desserts

This month's Joint Mathematics Meeting in Boston posed a series of unexpected challenges to some of my beliefs about mathematics.  Among these were beliefs not deeply held, or never really examined, so that it might be better to find a looser term than "belief" to describe them.  For example, ever since high school I have been loosely convinced that proof is the touchstone of mathematics, that the activity of proving theorems is what distinguishes mathematicians from the practitioners of other disciplines.  Of course what I meant by “proof” was the sort of argument that mathematicians actually share and discuss and eventually publish.  I didn't have formal proof in mind; that's the ideal of the Central Dogma, to which I do not adhere. 

The nature of my refusal to believe in the centrality of the kind of proof recommended by the Central Dogma will eventually reveal itself to be the theme of this week's installment, but for the moment I'm referring to the notion that proving theorems is what the members of the guild of mathematicians have in common.  This is hardly a notion peculiar to me; after all, the subtitle of Bettina Heintz's sociological study Die Innenwelt der Mathematik is  Zur Kultur und Praxis einer beweisenden Disziplin — “on the culture and practice of a proving discipline.”  But this is obviously nonsense.   One look at the stands in the Career Fair, or for that matter at the stands in the exhibition area, is enough to disabuse anyone of this notion.  Very few of the jobs on offer at the Career Fair have any use for proofs as the end product of an employee's activity.  Some sort of proof may be of value to show that a particular calculation does in fact show what the employee claims, or that the algorithm works as advertised, or that the encryption is secure or that the decryption is reliable.  But the end product is the calculation, or the algorithm, or the encryption, or the decryption.  Most mathematicians are applied mathematicians,¹ most applied mathematicians are not working in an academic setting, and the employers at the Career Fair are looking for candidates who can solve problems; proofs are usually optional.

---

                                                               Brief digression

(What was I doing at the Career Fair?²  The U.S. National Security Agency was there, billing itself as the "top employer of mathematicians in the nation."  Their business is encryption and decryption, and surveillance more generally.  I've had issues with the NSA for such a long time that I was protesting their activities, as one form of protest of militarism, even before I knew there was such an agency.  (You can read about the 1972 protest at Princeton, though not about my decidedly minor role, in Neal Koblitz's book Random Curves.)  Another loosely-held belief, that mathematicians are generally happy to accept funding from any source, however tainted, was put to rest when the Just Mathematics Collective (average age less than half mine) organized a visible (and occasionally audible) protest against the presence of the NSA table at the Career Fair.  Two veterans of the 1972 protest were on hand to lend support.³)

---

                                               At the heart of the profession

The real challenge to a deeply held belief, one that was thoroughly examined — or so I thought — in the pixels of the present Substack newsletter, came the following day, at the Dessert Reception for Fellows of the AMS, in Salon E of my hotel's Ballroom.⁴  With a glass of red wine in my left hand and a plate full of sticky desserts in my right, I was introduced to a personage of considerable influence in the world of mathematics.  He was aware of my book, but perhaps not of my beliefs about formalized mathematics, and certainly not of my role in organizing last October's Fields Medal Symposium that dealt with this very topic. Thus, when our conversation turned to the way developments in the mechanization of mathematics had been reported in the media, he was surprised that I disagreed that 2022 had been legitimately hailed as a year of great progress.  He expressed the opinion that at some point in the very near future (I think he mentioned a date before 2040) mathematicians would have access to convenient programs⁵ for formalizing proofs, and then verifying the formalization; that mathematicians would welcome this access; and that mathematics would be transformed as a result, for the better. 

My opinion, as I have written repeatedly here, is that formalization is beside the point for most mathematicians.  As I could have anticipated, however, what with the wine and the chocolate and whipped cream and my general inability to think in real time, I expressed my opinion badly.  I made the mistake of allowing the conversation to turn to a discussion of technical feasibility.  This is understandable, because the questions involved are reasonably concrete. But my disagreement is not with claims that technology will make it possible to reach a certain benchmark but rather with claims about what that benchmark really signifies. In order to have a meaningful conversation about such metaphysical or ethical points one first has to establish a common vocabulary, and for this it’s best to keep one’s hands free.

So be warned:  if you ever corner me at a reception and point to the apparent gaps in my thinking you will undoubtedly win the argument.  But it will be a hollow victory; the messenger's defects are not the fault of the message.  I'm unfortunately used to this and I wouldn't think it worth mentioning, except that one of my interlocutor's questions durably destabilized me.  With regard to formalization, he agreed that (as we have seen repeatedly here) mathematicians say what they are really after is understanding; but he insisted that, if there is a formal proof then the theorem is proved.  When I said that this was questionable on both historical and sociological grounds,⁶ and expressed my opinion that formalization is not an important goal for mathematicians, he retorted:  "So you think that Tom Hales wasted ten years of his life formalizing his proof of the Kepler Conjecture?" 

Though I did mumble something in reply, this left me at a loss.  On the one hand my admiration for Tom Hales, as a mathematician, as a citizen, and as a man of principle, is practically boundless. In any contest with the dark monopolistic forces besieging mathematics I would hope to have him on my side. So I would never wish to maintain that he was capable of wasting ten years of his life.  But on the other hand, it did seem that my position led inexorably to thinking just that impossible thought.

---

                                              Is Mathematician X obliged to care?

One thing I mumbled had to do with the legitimacy of formalization as a branch of mathematics, or perhaps at an artificial border zone between mathematics and computer science, one that had indeed flourished in recent years in ways that were undoubtedly of interest to specialists.  And I am not one to underestimate the importance of psychological factors in reinforcing one’s sense that one understands what one is talking about.  But I continued to deny that the practice had any metaphysical or epistemological significance for mathematics in general.  And I was not, and still am not, terribly satisfied with my defense of this denial, not least because it seems to be saying that Hales did waste those ten years if his quest was primarily philosophical.

Here I need to step back a bit to think about the Kepler Conjecture.  As a matter of pure geometry the question of finding the optimal packing of spheres in any dimension is undoubtedly one of the most appealing problems imaginable.  Beyond dimensions 1 and 2 the problem is also extremely difficult, and Hales's solution in the 3-dimensional case is a landmark of the highest historical importance.  It is of a different nature, however, than the only other known cases, in dimensions 8 and 24, which were solved by a synthesis of methods from different fields; no one was surprised when Maryna Viazovska was rewarded with the Fields Medal, in large part for her highly original solution of the 8-dimensional case.   In contrast, it's fair to say that Hales solved the original Kepler problem by pure geometry.  It is plausible that the geometric intuition necessary for our survival as 3-dimensional beings can guide us to the proof of the Conjecture, just as it guided Kepler to the statement of his Conjecture, and for that matter just as it purportedly guided generations of grocers to the practical realization of the Conjecture when they stack oranges or other approximately spherical fruits and vegetables.  Undoubtedly Hales was guided by his geometric intuition, and he was able to explain the "top-level structure of the proof" in just 9 pages in his 2005 Annals of Mathematics  paper.  But substantiating the intuition entailed verifying "nearly a thousand non-linear inequalities,"⁷ too much for even a team of humans to handle.

How does Mathematician X working in one specialty react to the news that a landmark theorem has been proved in a remote specialty, one for which X lacks the basic intuition?  The question answers itself:  unless there is reason to suspect that the methods of proof of the new theorem have a bearing on X's specialty, X will almost certainly not take the time to learn enough of the other specialty to be able to understand the proof in any meaningful way, but will rather defer to experts who assert that the proof is valid.  I don't see how this state of affairs is affected in any way by X's learning later that the proof has been translated into a formal language and verified by a machine.  X didn't understand the original proof and  certainly doesn't understand the machine's verification.  Unless X has an a priori ideological commitment to the superiority of machine-verified proofs over proofs verified by the interaction of human mathematicians, precisely nothing has been added to X's experience of the proof. 

There are unquestionably individuals, apparently including many computer scientists, who are ideologically committed to the superiority of computer-verified proofs over human proofs.  (For that matter, and I will return to this point in future essays, entire branches of the economy are built on the presumption that computers are superior to human beings in most or all respects.) Otherwise I can't explain why so many computer scientists are obsessed with the prospect of translating "the proof" of Fermat's Last Theorem into a verifiable logical sequence of formal propositions.  I happen to believe that this attitude is a symptom of a potentially genuinely dangerous preference for machines over humans as sources of truth, but this is a theme to be explored elsewhere.⁸ 

---

                                 Is mathematics subject to the laws of physics?

In favorable situations it is possible for the discoverer of a new proof to share the insight behind the proof with a broad audience of mathematicians in the space of a one-hour colloquium talk.  If we're looking for ideals that are valued by mathematical practice, certainly this one is more congenial than the unrealistic and not intrinsically appealing⁹ ideal of transforming proofs into a language that only machines can process.  Let's remember that those grocers didn't really choose the face-centered cubic packing, or the hexagonal-close packing, in order to save space on their shelves.  Just try stacking a few hundred oranges in vertical columns, and see what happens. 

Most of you will have too much sense, or too few identically spherical oranges, to take my suggestion literally; nevertheless you undoubtedly “saw” what would happen if you did.  In fact, what you “saw” can easily be turned into a “proof,” and probably even a proof, of the relevant

Theorem:  Let δ > 0 be a real number. Consider a collection of identical 3-dimensional spherical oranges, placed in k vertical columns, and subject to the force of gravity and non-zero oscillations of length δ.  Then there is an integer N, depending on δ, such that after N seconds all the oranges will be on the floor.

This doesn't even prove anything about Kepler's conjecture in the very special case of vertical packing, but it is relevant to grocers plying their trade on a vibrating earth in a non-trivial gravitational field.  Moreover, it is relevant to my argument, because your ability to see the consequences of such a naive attempt to generalize the known solution of the 1-dimensional sphere-packing problem to 3-dimensions illustrates the principle of what Ian Hacking called a cartesian proof.  It is a proof whose “top-level structure” can not only be communicated in a few lines, or by a simple diagram, but which conveys understanding of a sort impossible with any formal proof — provided the receiver is a being subject to gravity.

The formal verification of “nearly a thousand non-linear inequalities,” on the other hand, could serve as the model of Hacking's leibnizian proof, pure reasoning without any more understanding than what was already present at the top level, perfectly adapted to travel in interstellar space, or in no physical universe whatsoever. 

---

                                              Resistance is mainly passive

Perhaps my feelings about the Kepler conjecture are irrelevant; I’ll never develop a cartesian understanding of the concepts behind the proof. Turning to the kinds of mathematics I do understand, I’m already on record as stating that a formal proof would add nothing to my appreciation of Wiles’s proof of Fermat’s Last Theorem, the more so because I see the proof not as a specific text amenable to translation to a formal language but rather as “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.”

No one, myself least of all, would want to waste even ten minutes formalizing my own modest accomplishments.

There are also borderline cases, where my work has needed to quote a result whose statement I understand but whose proof is the object of some concern. The original version of my paper with Shepherd-Barron and Taylor, one step in the proof of the Sato-Tate Conjecture, quoted a theorem on discrete groups whose proof was based on the classification of finite simple groups. Philosophers and sociologists have pointed to this classification — more than forty years after the result was announced, the proof, which runs tens of thousands of pages, is still not considered definitive — as a problem for those for whom certainty is the hallmark of mathematics. It has therefore been a prime target for formalizers. An noteworthy triumph for the formalization program was the completion of a proof in the COQ formal language, by a team led by Georges Gonthier, of the Feit-Thompson theorem that finite groups of odd order are solvable, a crucial component of any proof of the general classification theorem. If the entire classification theorem had been formalized, would it have made me feel less uneasy about the Sato-Tate Conjecture?

It’s true that some mathematicians prefer to keep the classification theorem at arms’ length, because of its complexity. We were pleased to include an independent proof, due to Nick Katz, of the result we needed for our application, so in the end any remaining misgivings about the status of the classification theorem are irrelevant to the Sato-Tate Conjecture, or to any subsequent applications of the method. But even had that not been the case, formalizing the proof of the theorem on discrete groups would have provided no solace. Katz’s version was as close to a cartesian proof as we could have wished, very much in the spirit of the rest of our paper, while the classification theorem appeared at best as an uninvited guest, whose relevance to the Sato-Tate problem could not have been more tenuous.

My conclusion is that, beyond the community of mathematicians — that counts Tom Hales as a particularly distinguished member — who are directly involved in developing the dynamic but still limited and highly specialized field of formal mathematics, formalization of mathematics is a manufactured demand, sustained by a series of overlapping viral narratives very similar to those discussed in Robert J. Shiller’s Narrative Economics.¹⁰

---

                                         Passive resistance may not matter

None of what I wrote above should be taken to mean that formalization in one of the available languages, or in some language not yet invented, won’t become a requirement for publication in respectable journals. Among my colleagues are those who argue for the necessity or inevitability or benefit of compulsory formalization with the sort of passion usually reserved for matters of religion or money. Here I’ll set aside the religious motive and just observe that when you consort with people who place money at the fulcrum of their scale of values, some of their obsession is likely to rub off on you. And in this as in most matters, it is such people who make the decisions that determine the course of our professional lives. Not the least of these decisions is how much of that money that is so important to them will be diverted to supporting the research without which the debate on formalism is empty.

Although its early stages are well covered in Donald MacKenzie’s Mechanizing Mathematics (up to about the year 2000), the history of formalized mathematics has yet to be written. Some of the talks at October’s Fields Medal Symposium touched on some major milestones, and the topic has been treated in numerous prominent articles by and for mathematicians. In contrast to MacKenzie’s insightful book, these articles (at least those I have read) treat the history as an entirely internal matter, driven exclusively by intellectual and ethical considerations within the field of mathematics; they make no reference to the material incentives and penalties, not to mention material resources, that will be needed to put the formalization program into practice on the scale anticipated by my interlocutor at the Dessert Reception. It will take the skills of an investigative journalist to sort these out, to understand the motives of the industrialists who are investing so much in projects to mechanize mathematics as well as the venture capitalists who are backing them up, and the means by which media, funding agencies, and institutions of the profession are convinced to promote certain narratives, including those that contribute to manufacturing demand for formalized mathematics. Most crucially, perhaps, journalists and social scientists will be needed to document my diffuse but persistent impression that most mathematicians really don’t see the interest in formalization.

I am neither a journalist nor a social scientist and all I have are anecdotes about the growing numbers of mathematics Ph.D’s who have despaired of academia and are taking jobs in Silicon Valley and its satellites; or who are supplementing their income with part-time tech jobs that require them to sign non-disclosure agreements; or about the distinguished applied mathematicians who are pressured by funding agencies to include machine learning projects in their grant proposals. In future posts I will share as much of this information as I can; but I have far exceeded my 3000-word target, so this will have to wait.

1. Or teachers, and while the teacher may teach how to produce proofs, the "product" of the teaching profession, if one must speak that way, is the educated student, and not the proofs created along the way.

2. What was I doing in the exhibition area?   Looking for coffee, most of the time.  That room had the only coffee tables accessible without a trek across the cavernous and labyrinthine Hynes Convention Center to the Dunkin Donuts at the mall entrance. It was a scandal when the tables inexcusably ran out of coffee well before the Special Session I was attending had ended.

3. And if you would rather not collaborate with NSA funding of mathematics you can say so by signing the pledge at
https://www.justmathematicscollective.net/nsa_statement.html#bookmark=id.qqo1e7umtkit.

4. The name is symptomatic of the faintly ridiculous character of these annual meetings that punctuate the academic calendar.  Does anyone know whether there are really balls in these ballrooms, like the famous balls of the Viennese season, with black tie and ballroom gowns and dancing to a string orchestra?   And if so, do colleagues in other fields take part?

5. Although he didn't say this, I assumed he had in mind programs as easy to use as LaTeX for typesetting or Maple — the sole Diamond sponsor of the JMM, one rung above the NSA, the sole Gold sponsor — for symbolic manipulation.

6. Here I missed the opportunity to cite the references quoted in this earlier post (see the section “The intellectual bias of our time”) or Karine Chemla's introduction to The History of Mathematical Proof in Ancient Traditions, a book that “opens the way to providing the first comprehensive, textually based history of proof,” to quote Jeremy Gray. I could also have mentioned the visible disconnect between the ideological insistence that proof is the goal of mathematicians and the jobs on offer at the Career Fair.

7. Hales, A proof of the Kepler conjecture, Annals of Mathematics, 162 (2005), 1065–1185; Hales et al., A formal proof of the Kepler conjecture, Forum of Mathematics, Pi, (2017), Vol. 5, e2, 29 pages doi:10.1017/fmp.2017.1.

8. As far as I know machines don't intentionally lie, but the recent large language models have revealed the novel possibility of machine "hallucination."  I don't know whether or not this will chasten the philosophers and computer scientists who are counting on future machines to satisfy their need for a kind of confirmation that Wiles really did prove Fermat's Last Theorem that the community of mathematicians is unable to supply.

9. Except, of course, to specialists in formal proof verification, for whom this is understandably a legitimate professional challenge, and "fun," as Kevin Buzzard put it.

10. The theme of formalization as manufactured demand will be addressed at length in future newsletters, beginning with the next installment on a notorious example of manufactured demand in the AI industry that is not directly related to mathematics.