Replies to my fan mail
Why speculate when you can just ask?
What a joy it was to discover, finally, that people have been sending me messages through this indirect channel1, and how sad that it took me so long! But the discovery comes just at the right moment, while I am staring at another self-imposed deadline to write a review of a serious and challenging book — Stuart Russell’s Human Compatible. Russell’s book has very little to say about mathematics but offers insight into how the inevitability and desirability of technological change is viewed by those in a position to do something about it. Reviewing it is obligatory for the project of this newsletter. But now I can put off grappling with its challenges for another two weeks while I do something much easier, and especially much more fun, which is to try to clear up some of the Lean community’s misunderstandings of my intentions, my concerns, my reading of the cultural moment.
And boy are there a lot of misunderstandings! And not the ones I anticipated. I’ll answer some of your individual questions, Zulip Chatterers, and address some of your recurring misconceptions, but a first point to bear in mind before attempting to guess my intentions: Silicon Reckoner is not about you! Not about formalizers, certainly not about the Lean community, nor any other particular branch of the centuries-old project to mechanize mathematics. It’s not especially directed at mathematicians, nor even at computer scientists — though I have to say I have seen things written and heard things said by computer scientists,2 including a close friend, that display a dogmatic vision of mathematics that is very different from mine, and that I would hope to alter.
No: my second main motivation in scattering about 3000 words into the ether every two weeks is to continue my efforts, that began during the Science Wars of the 1990s, to combat a caricature of mathematics that remains distressingly prevalent among humanities scholars. You can find it, for example, in William Blake’s
May God us keep/From Single Vision and Newton's sleep
or in Poe’s Purloined Letter
I never yet encountered the mere mathematician … who did not clandestinely hold it as a point of his faith that x squared + px was absolutely and unconditionally equal to q
or more perniciously in the Adorno and Horkheimer quote in this earlier installment. I see this caricature codified in what I called the Central Dogma3 and reinforced by the pronouncements of some4 of the promoters of the mechanization of mathematics, and even more in the journalistic vision of the new mechanization projects; and since that’s not the vision I want my colleagues across campus to remember I owe it to myself, and to them, to make them aware of an alternative that I see as more representative of the practice of mathematics.
This leads me to my third main motivation, but before I get there I should help Patrick Massot deal with his Selective Reading Syndrome (SRS) by pointing out that I responded to the August 5, 2021 comment quoted above (inadvertently, since I had not yet discovered Lean’s Zulip Chat Archive) just 26 days later, writing:
Someone named Gershom B. objected [six years ago] that “programming and computer science are _extremely_ playful disciplines.” I am sure he was right about that; moreover, I have reliable reports that formalizing mathematics is “really good fun” and that this accounts for much of its appeal to a growing community. As usual, the point I am making is addressed to the rhetoric surrounding the mechanization of mathematics rather than to the experience of practitioners; nevertheless, we can speculate whether the machines themselves will ever experience proof verification as “extremely playful.”
I want to stress that “as usual,” since that and the point about rhetoric should suffice to make it clear that my purpose in this newsletter is not to attack anyone — except for war criminals, racists, tech billionaires, and the like — and certainly not to express fear of anything — though I am indeed concerned by the accumulation of power by the very forces that just happen to be investing the most in promoting AI and incidentally the mechanization of mathematics. Nor am I upset, nor do I have “opponents,” nor …
Come to think of it, I’m not sure that Massot read even the August 4 post to the end. Far from expressing opposition to funless human mechanizers, its final paragraph only objects to hiring actual machines as colleagues if they don’t positively enjoy their work. (Marc Huisinga made the same mistake.) Pretty much all the questions raised on Lean’s Zulip Chat Archive were already answered on Silicon Reckoner, mostly in the very first post which serves as a kind of statement of purpose. So I could just quit here and invite my Zulip readers to look for clues and hints that are not at all concealed in the undergrowth of the prose of my previous posts — no more than the one that Massot failed to spot at the end of the August 4 post.
But it’s so much more fun to interact with my fans directly! So let’s start with an admission of guilt. Filippo A. E. Nuccio was absolutely right on August 6, 2021 to point out that I had no right to claim to speak for all mathematicians when I wrote
What pure mathematicians find valuable about what we do is precisely that it provides a kind of understanding whose value is not determined by the logic of the market.
I fully sympathize with Nuccio. I can’t stand it when other mathematicians write such things, and not only because the concept of speaking for mathematicians as such is nonsensical. If Nuccio had taken the time to follow the link conveniently attached to the above sentence he would have seen that I had already conceded his point, 11 months before he made it, condemning my own sentence as an
abusive and rather underhanded implicit definition of the pure mathematician as one whose values conform to an impossibly unrealistic ideal.
That’s from the article on the Mathematics without Apologies blog5 that I wrote to explain the back story for that “abusive and underhanded” sentence: Briefly, Stephen Ornes had called me while writing his Quanta article entitled How Close Are Computers to Automating Mathematical Reasoning? Wary of being cast as the token skeptic in yet another article celebrating the inexorable progress of technology, I agreed to be quoted, but on one condition — that the quotation include a sentence — imprecise, perhaps “abusive and underhanded,” but nevertheless containing more than a kernel of truth — like the one to which Nuccio objects. Ornes agreed and the sentence was in the last draft Quanta showed me. But it was cut before publication. To add insult to injury, the article substituted a vacuous sentence
Even if computers understand, they don’t understand in a human way
taken out of context from a roundtable discussion in which I had participated.
I gave Quanta the chance to atone for breaking their promise by submitting a first version of an article, specifically built around the sentence on the logic of the market, for the series of “Quantized Columns,” to which Quanta had invited me to make regular contributions. The article’s starting point was Scholze’s guest appearance on the Xena blog and the aim was to propose an interpretation of its significance different from the one that I anticipated (correctly) would be reported if and when his challenge was met successfully. But my column was rejected on spurious and easily falsifiable grounds, and after reading Quanta’s subsequent articles on mechanization I strongly suspect that it’s because mine didn’t conform to their chosen narrative, a synthesis of the understandable journalistic attraction to novelty with an at best mildly critical orientation to the pretensions of Big Tech.
The essay with that boldface sentence about the logic of the market was revised several times for different audiences and pitched to a few more publications. Although a French version — preceded by a long section on the benefits [sic!] of computing in mathematics — may finally appear this year, I decided to start a Substack newsletter sooner than planned because I was impatient to provide an outlet for one draft of the essay. Bear in mind that it’s not the final draft; nor is anything else in Silicon Reckoner. Every sentence can be improved, and the one that Nuccio found abusive (as did I) can be placed in context. Still, I come up with a blank when I try to imagine how his “position towards ‘the logic of the market’” differs from mine, as he claims, with regard to the value of his understanding of Iwasawa invariants.
A user named only Mac, who identifies as a computer scientist, is “slightly concern[ed]” about my apparent confusion/conflation of logic and rhetoric
the hope (as I see it) is that rest of mathematics follows objectively/logically from these principles and is not merely a matter of rhetorical consensus.
It’s an ancient and commendable hope, but it’s also an old story in philosophy, perhaps the oldest there is, that no coherent account can be given of that “separation between logical and rhetorical argument” that Mac finds so essential. Western philosophers, at least, have been aspiring to make that distinction forever, and it’s one of the noblest aspirations imaginable. But every attempt is fatally flawed because it bumps up against the fundamental humanness that makes humans function so much less transparently than programmable machines. Fortunately, if you look at what actually matters to human mathematicians6 you will rarely find this “separation” high on the list. I don’t know how the Leaners who took up Scholze’s challenge feel about his comment.7
What I care most about are definitions … [after thinking for “a long time” about a particular concept] it took another two or three years to finally write down the correct definition…
What I want to stress here is that writing down definitions is neither a logical nor a rhetorical act: it is a creative act. Acceptance of a definition is a social process. And Scholze’s definitions have been transformative.
There’s no reason a computer scientist like Mac should care about any of this; but by the same token, the relevance to mathematicians of the “slight concerns” of computer scientists or philosophers regarding what mathematicians should be doing has yet to be demonstrated.8 After all, G. H. Hardy not only didn’t distinguish between logic and rhetoric; he actually referred to proofs as “rhetorical flourishes” in the famous sentence in which he adds that he and Littlewood call them “gas” — does anyone know why they called proofs “gas”?
To the complaints about my “flowery prose,”9 similar to those I already encountered in connection with Mathematics without Apologies, I can only say that this is how I like to write. Writing convoluted sentences in a variety of tones and registers, and stopping in the middle of a paragraph for a digression whose relevance may initially be unclear to the reader, is one of my ways of having fun. Some other people like it as well, and I’m happy to be writing for them. Is it a coincidence that this neat division between those who dislike my style and those who enjoy it neatly tracks the division between those who are enthusiastic about formalization and mechanization and those who would rather give it a pass? The first group likes straightforward binary oppositions — black/white, yes/no, for/against, good/bad, 0/1, and/or, etc. — while the latter doesn’t mind some ambiguity and may even find it thrilling. If I were as nasty and mean-spirited as some of the people on Lean’s Zulip board I might even be tempted to speculate that it’s precisely the discomfort with the complexities of natural language that leads people in the former category to seek refuge in the secure but empty certainties of symbolic logic, where theorems go to die.10 But I’m not nasty; and more to the point, such prose skills as I possess decay if not maintained. This is why my primary motivation in starting Silicon Reckoner was to force myself to keep writing, at a pace of 3000 words every two weeks, so that I will remain capable of stringing together a few decent sentences if the need arises.
But can’t the two communities coexist peacefully, even as I explain to my friends in comparative literature that (at least for now) there are more of us than there are of them? Maybe, but while publications like Quanta shoehorn my side into the role of token skeptic, the other side gets promoted by the PR agencies of tech billionaires and is courted with $20 million institutes… Which reminds me that I need to acknowledge Jeremy Avigad’s comments. Avigad is a philosopher, among other things, and unlike most Zulip Chatterers doesn’t chop his thoughts into tweet-sized bits. For those reasons, among others, I owe him a more considered response than what I can offer here, and I promise to do that in an extended review of the Synthèse article that I quoted, along with his article that just appeared in the January 2022 issue of the AMS Bulletin and that more directly addresses the concerns of Silicon Reckoner. For now I can only say I’m sincerely sorry if he was offended by my characterization of the quote as “militant” and “unsubstantiated.” Each of those words has a precise meaning for me but using them in public commits me to explaining what they mean and justifying their use, and I intend to do this ahead of my initial schedule, in four weeks if possible.
On the other hand, I don’t intend to apologize for insinuating in the essay on the Central Dogma that Charles Hoskinson, with his new “paradigm” and his “Bourbaki-style moment,” is aiming at a hostile takeover of at least part of mathematics (not to mention the ominous-sounding “wannabe mathematics”). In the first place, I have no sympathy to spare for billionaires, tech or otherwise, so if I were to apologize it would be to those members of the community who will be accepting his largesse. Now before you try to remind me that institutions like Columbia or Carnegie-Mellon have always depended on the kindness of strangers to the academic enterprise, I retort that this is something of which I am only too aware. While freedom of expression at private and public universities is never a sure thing, mathematicians have for the most part been protected. Still, accepting a job anywhere entails accepting limits on your freedom. For example, to preserve departmental comity you can’t always say out loud what you think of some of your colleagues.
But there are very good reasons to believe that the mentality of the tech industry is not congenial to the kind of intellectual freedom to which we are accustomed. When I read the Nature article about the DeepMind collaboration with mathematicians, my first thought was that I would be perfectly happy to complete one project (on explicit properties of the decomposition of the restriction of a discrete series representation to a Lie subalgebra) in collaboration with a deep learning apparatus. But then I learned indirectly that a colleague — who may be reading this paragraph at this moment — agreed with what I wrote about the DeepMind collaboration but is unable to say so because “had to sign a confidentiality and non-disclosure agreement” when he got involved with a prominent Silicon Valley company “and cannot express his reservations publicly.”11 That sort of thing rules out any interaction on my part with Google or its neighbors. Avigad, no doubt, will do what he can to maintain academic standards, but I have a hard time believing that Hoskinson will welcome the free expression of reservations about what I called his “messianic vision” in the Center that bears his name.
This leads me to Anne Baanen’s partial defense of the “Central Dogma” text:
The central thesis I distilled is that this currently trendy branch of mathematical formalism, that a proof is a proof iff it can be transformed into a formal arrangement of symbols checked for syntactic correctness by an automated process, is merely an ideology that can/should/will be subverted by another. … Formalism certainly is not a universally accepted standpoint, even though it would be in the interest of the ITP community to agree with it unanimously.
That’s absolutely right, and it’s why I think it’s appropriate (as well as catchy) to call it a dogma. Baanen later points out, correctly, the distinction between formalization and formalism. Referring to the reigning ideology as the Central dogma of mathematical formalism collapses this distinction, perhaps abusively, but I couldn’t think of a snappy title that avoids this potential ambiguity. Baanen’s next paragraph helps to clarify what is and is not at stake.
What I really miss in the post is engaging with previous iterations of debates on mathematical formalism — getting rid of the details about computers and cryptocurrency I can imagine Brouwer writing such an essay against Hilbert.… Are there differences in kind or degree to that of the early 20th century?
It helps to make a further distinction, in the terminology of my essay, between the ideology as point of view and ideology as value. As value it affirms that formalizing (in Lean or otherwise) can be interesting, enlightening (like an LSD trip), intellectually stimulating, or fun. I have no quarrel with that; it may not be any of those things for me (and it’s not) but your pleasures are none of my business. As point of view it insists that mathematicians are simply wrong not to accept the new paradigm and indeed that at some point they will be compelled to do so. No one in the chat is actually advocating that, though Nuccio “actually find[s] it very nice” to imagine some nameless authority enforcing compliance.
To return to Baanen’s question about the difference between now and 100 years ago: Brouwer and Hilbert were responding to a perceived crisis that mobilized central figures in the (at the time much smaller) international mathematical community. Although I suspect that most working mathematicians at the time were much less worked up about the so-called crisis than one would conclude from reading the historical accounts, the debate did have a lasting effect on training of future mathematicians. In contrast, and in spite of the presence of formalization on the ICM stage and the breathless coverage in publications like Nature and Quanta, formalization is today a marginal concern among mathematicians. It seems to be less so among computer scientists, and I can certainly dig up quotations by computer scientists that cross the line from value to point of view, decry the failure of mathematicians to get on board, and in many cases look for technical explanations for this failure. The essays here on the roots of technological determinism explore the origins of this peculiar mindset; my spontaneous response is to say that, as long as mathematicians are not committing the sorts of acts that would land us in the docks at The Hague12 the computer scientists can just butt out.
Let me repeat that formalization is a marginal priority for mathematicians, because this is a point the Lean crowd needs to understand. I suspect that much of the vitriol expressed by the Lean Zulip Chat’s more intemperate and borderline sociopathic participants13 is directed not at me but rather at their own frustration with this marginality. Even if at some point in the future mathematicians are forced to comply with a formalization diktat in order to publish, this will be as irrelevant to the content of mathematics as the obligation to submit manuscripts in LaTeX, and considerably more disruptive to the train of thought.14
Most of the essays on Silicon Reckoner, the ones not being discussed in the Zulip chat, explore why formalization and the promised AI future are of marginal interest among mathematicians and why they are likely to remain so. This is necessarily difficult to pin down because, as Gayatri Spivak declared to Kevin Buzzard in November 2020, “the digital will never capture the contingent.” As a human activity mathematics is irreducibly contingent; that’s why most philosophers steer clear of what actually drives mathematics and latch on to what can be easily formalized.
The injection of enormous resources from the tech industry may alter the mathematical population, however, and then all bets are off. In the meantime, speaking for myself, and to make things clear one more time: the word that best describes my reaction to formalization is not fear, nor upset, nor any impulse to attack, but rather boredom. I certainly admire the ingenuity that goes into successful programming, and I did learn to program a (very) long time ago. If I needed to do so again to solve a specific problem, as I hinted in the paragraph about the Silicon Valley NDAs, I’m sure that finishing the job would bring me momentary satisfaction, on the order of weeding my garden (but without the benefit of fresh air) or changing a light bulb (but without any additional enlightenment). But programming is so low on my list of appealing activities that I haven’t touched it in any form since before I left Brandeis in 1994 (and I didn’t much care for it then either).
On the other hand, and beyond my interest in how current mathematical trends of any kind force me to sharpen my own understanding15 of what makes mathematics valuable as a human practice, I am deeply interested in mechanization of mathematics, of which formalization is a small part, as a social phenomenon: how it establishes a shared vocabulary, an ideology, a system of values, a community; how it overlaps with and is influenced by broader economic and industrial trends; how it acquires resources to expand; what it does or does not share with contemporary political movements; and much more. In this respect the leanprover-community Zulip Chat Archive is a veritable socio-historical goldmine. And with that in mind I encourage you to direct your future comments, questions, and speculations regarding my intentions to this page.
Thanks to Kevin Buzzard and Peter Scholze for defending me, especially from the diagnosis of dementia. I hope they’re right!
Really, nothing posted on a public internet forum is a secret; I have to assume that anyone who wrote about me expected me to see it, sooner rather than later.
NOT ALL computer scientists, it should go without saying. But then I read things like “Marc Huisinga (Jan 28 2022 at 11:52):
…I don't think that these are positions held in general by the ITP community…”
I wonder: who said they were?
A few posts on the chat acknowledge that many computer scientists do adhere to the Central Dogma about mathematics. They’re in good company; I’ve elsewhere traced the attitude back to Plato’s Republic. Only their psychoanalysts know why such people feel compelled to interfere with someone else’s fun…
…to which I will return very soon…
NOT ALL! See note 2.
If my fans really want to know how I think about mechanization it’s all in there; none of it corresponds to what they have been writing on Zulip. The third main motivation I promised above is to develop these thoughts and to place them in some sort of socio-historical context.
As opposed, perhaps, to computer scientists or philosophers.
Jeremy Avigad seems to agree with Scholze: see pp. 105-107 of the recent article I expect to review in a month’s time.
I can think of much ruder ways of saying this, but I save them for private conversation.
I understand this to mean the use of subordinate clauses and more than one adjective per sentence.
That’s not … quite … what I really think. But writing that sentence was just too much fun!
This mindset reminds me of my experience when, in the wake of Edward Snowden’s revelations, Allyn Jackson and I tried to organize a debate in the pages of the AMS Notices about the relations between mathematicians and the NSA. We were hoping to hear from all sides but found to our surprise that essentially no independent voices were raised in support of the NSA. It was explained to us that the mathematicians who had worked with the NSA were forbidden from writing anything about it that the Agency had not previously vetted. Those mathematicians who might have been sympathetic to the NSA were not willing to go through the process.
My image of the legendary Dutch verdraagzaamheid (first on the list here) has taken a hit; for some reason many of the most militant and intolerant versions of this ideology have been written by Dutch computer scientists. See also note 8.
By the way, I thought Anne Baanen’s thoughtful comments confirmed (by contrast) my impression that the agressivity of many mechanizers is testosterone-fueled. Instead it confirms my ignorance of Dutch first names. The Lean community does appear to be overwhelmingly male.
I take heart in reading in the Lean Community Guidelines that “Behavior that is offensive, discriminatory, or aggressive will not be tolerated in any form.”
Do I underestimate the plasticity of the human brain? If ancient Egyptians could reason in hieroglyphics and I can reason in simplified LaTeX and programmers can reason in code, why can’t mathematicians be trained to reason directly in Lean? Maybe warming up by teaching their children Lean as a first language? Would a Lean future, by selecting traits adapted to its use, inexorably favor the mathematical population’s evolution toward greater freedom of thought, or conversely toward greater conformity? Time will tell.
Spare a thought, though, for the technical typist, a skilled profession that most of you have never known, laid low by LaTeX.
…as in this close reading of a magnificent lecture by Dick Gross…