Gonna have fun fun fun!
Wouldn’t it be nice if Lean spoke our language?
I very distinctly remember thinking during LT2021 that I never attended a traditional math conference with so many talks mentioning fun and enjoyment. (Patrick Massot, Zulip Chat Archive)
…he might be arguing more about either the way this is presented in articles or a fear that math will be less fun in the future when formalization has taken over. I certainly have heard this argument before (and much more succinctly!) (Jason Rute, Zulip Chat Archive)
I understand that Harris fears that math would become less fun with proof assistants. But he simply has no evidence to support that claim, only his fantasies. (Patrick Massot, Zulip Chat Archive)
Right now interactive formal proving is fun because it is new, it is ambitious, it is optional, and it is decoupled from discovering the proofs. But imagine a world where it becomes required for publication… (Jason Rute, Zulip Chat Archive)
(My emphasis)
I couldn’t wait for June to watch the talk Patrick Massot gave last February 15 at the Institute for Pure and Applied Mathematics (IPAM) in UCLA, after I learned that Massot and collaborators had developed a system to translate Lean proofs into human-compatible informal proofs. It was a mild (62.6° F) day in Westwood, with clear sunny skies, ideal weather for surfing or for tooling down Wilshire Boulevard in Daddy’s T-Bird. Nevertheless, Massot was able to attract this many people —
out of the sunshine and into a sterile institutional space to watch his demonstration of the system’s output of a version of a theorem about continuity from Bourbaki’s General Topology. The slide reproducing Bourbaki’s proof was followed by a slide showing his own formalization in Lean, followed by the latter’s informalization produced by Massot’s system. It’s hardly surprising that what Lean produced looked very much like the original Bourbaki argument. It came with a bonus, however, in the form of nested hyperlinks, which expanded when clicked into increasingly fine-grained justifications of intermediate steps. This operation could be repeated until the skeptical reader finally arrived at statements in the Lean library that had previously been formally verified. Think of it as a massive extension of the principle of the Stacks Project to every proof, but where the proof unspools on the page in front of you instead of tangling in a mess of hyperlinks spread over countless separate pages.1 It’s hard to imagine that even the most determined human being wouldn’t be satisfied at this point, but an AI with trillions of nanoseconds on its (their?) hands might want to go all the way back to the axioms, and who would be so cruel as to deny it the right to its own artificial sort of fun?
Readers and authors: the alignment problem
I get around: I’ve attended conferences, eccentric as well as traditional, all around this great big world, yet I don’t think I’ve even once heard a speaker mention “fun and enjoyment.” Nevertheless I can confidently assert that mathematicians usually expect our work to bring us fun fun fun, a quality of experience you won’t find in most job descriptions, not even in the fine print. “What makes you think you should have a job that you actually like?” Anne Merchant used to tell her daughter Natalie, the future singer-songwriter. “Life is about waking up every morning to do something you hate with people you don’t like.”
You can tell by the frequent bursts of uproarious laughter — for example, when Massot revealed the slide reproduced above — that the audience in California is happy they woke up that morning. I captured several screenshots like the one above; I wish they all could be accompanied by their soundtracks in this newsletter, so my readers could pick up the vibrations in the room.
Part of the fun, I’m pretty sure, comes from the sense of being on a mission. I’ve suggested in the past that the formalists’ mission is related to realizing the promise of the Central Dogma — to create a proof’s formal Doppelgänger, thus confirming its validity according to a purely mechanical version of the validation process — but that wasn’t prominent in Massot’s talk. His primary motivation (apart from having fun), at least as presented in his IPAM talk, seems less to be to guarantee correctness than to improve mathematical communication, as suggested in the above image, offering an interactive experience that the reader can fine-tune. Massot is a technophile and is disarmingly straightforward about his epistemology: the situation in 1993 was already a “big improvement” over earlier methods, but “the content is the same” [1’20”-1’32”] — the loss of the thrill of a face to face meeting with Pythagoras notwithstanding.
But Massot also presents the technique as a way to attenuate the hierarchical distance between author and reader. He is “not enthusiastic about unreadable proofs” and warns [39’30”] against
…always thinking in the old way of having the author decide on the level of detail of the proof and you shouldn’t do that.
That “shouldn’t” is an ethical injunction, rather than a claim that he has verified that adding the option to click repeatedly on hyperlinks really represents an improvement on “the old way” of mathematical communication, and it’s a reminder that Massot’s talk, and much of the IPAM conference as a whole, is ideologically based rather than empirically grounded.
Time will tell whether or not Massot’s hopes for the technique are borne out. In the meantime, I want to explore the ideology behind the impulse to renegotiate the terms by which the reader is subordinated to the author.
Inside, outside, or somewhere in between?
When I suggested to Will Cavendish that the Lean community, and formalizers more generally, see themselves as an embattled minority, he replied that not only was my impression correct but that it is an accurate description of the community. I admit I find it hard to reconcile this vision with the project’s welcome of the clammy embrace of industry heavyweights, in the form of speakers from Microsoft, IBM, Amazon, and Google (total assets well over $1,000,000,000,000) at the IPAM meeting. Also the full run of the IPAM building for the five days of the conference; and a six-week programme at the Newton Institute in Cambridge in 2017, a full trimester at the Institut Henri Poincaré in Paris in 2014, yet another trimester coming up at the Hausdorff Institute in Bonn, not to mention a dedicated institute at Carnegie-Mellon University at $20,000,000 and counting.
But it’s also hard not to sympathize with the distrust of a system visibly designed to serve the interests of a self-selected and self-reproducing caste of designated experts, a system that is moreover reliant upon these same gatekeepers for validation of the results upon which one’s own work depends, for validation of one’s own work, and ultimately for validation of one’s determination to pursue this lonely career. Absent such validation one is liable to end up literally on the outside of the formal institutions of mathematics, barred by paywalls from access to the digital archives, one’s future foreclosed.
This very newsletter can be (and, I'm told, has been) interpreted as an uncompromising defense of the unwarranted privileges of the dominant caste. Those who have been marinating in the binary logic of the digital age may2 believe that an unwillingness to join the party must stem either from the perception that the new technology is just too complicated — hence the emphasis on making formalization less unwieldy3 — or from outright hostility.
I’ve already explained that my own attitude toward formalization is one of indifference rather than hostility, and I believe that it is shared by most of my colleagues. I am hostile, however, to the arrival in our midst of an industry whose business model is a contemporary extension of the tendency Marx identified in The Poverty of Philosophy:
Finally, there came a time when everything that men had considered as inalienable became an object of exchange, of traffic and could be alienated. This is the time when the very things which till then had been communicated, but never exchanged; given, but never sold; acquired, but never bought – virtue, love, conviction, knowledge, conscience, etc. – when everything, in short, passed into commerce. It is the time of general corruption, of universal venality, or, to speak in terms of political economy, the time when everything, moral or physical, having become a marketable value, is brought to the market to be assessed at its truest value.4
Any activity that provides a refuge from this "general corruption" deserves to be protected. Mathematicians happen to be fortunate enough to find ourselves in such a refuge; it is therefore our responsibility to warn against its corruption.5
We have been in this room so long that we no longer see it
I have reported elsewhere that the Bulletin of the American Mathematical Society is currently preparing a special issue on the implications of automation and AI for the future of mathematics. A number of contributors to the special issue were on hand at the IPAM meeting; others have watched the video; and at least two saw Massot’s talk as a milestone, a sign that formalization is now making genuinely interactive proofs possible. I have to confess that I too, was initially impressed by the readable output. But after thinking it over I realized Massot never explained how human text is generated from Lean programs. Or else it went by so quickly that I missed it.
So I sent the following message to someone I spotted in the audience.6
I can imagine exactly three ways it could have worked. The first is reinforcement learning: the system is given an enormous database of Lean programs paired with human text, and it gradually learns to associate the latter with the former using statistical analysis and correction by human trainers. Such a project would in principle require many millions of dollars, so I don't think that's what he did.7
The second is dictionary based: the terms in Lean are assigned translations into English. Then the system uses the dictionary to transform a a sequence of terms in Lean to a sequence of expressions in English. At this point something has to be done to mold the sequence into syntactically correct English sentences, for example running it through a large language model. Maybe he said what is done there but I missed it.
The third would be to fake it in some way. He presented a single example. Maybe the system was overdetermined so that the output could only consist in sentences of a certain form, and only a small amount of variation (filling in blanks) is permitted. It's hard for me to imagine that such a procedure could apply in great generality.
The correct answer was essentially the second option, possibly constrained by a short list of admissible sentences as in the third. I heard someone in Massot’s audience mention large language models, but apparently they were not involved in creating the output.
Just because something is hard for me to imagine hardly means it’s impossible. But try snapping sentences together out of English-language fragments from a predetermined dictionary, like Lego blocks, following rigid rules of translation from analogous blocks of another (natural or artificial) language, and decide for yourself whether the result is satisfactory. Start with the opening sentence of a famous French novel and you get
A long time I myself have been gone to bed at good hour.
The meaning is recognizable but only because the sentence is short. A more characteristically digressive sentence by the same author turns into this.
This was not any more longer the room quite powerful still on my sensitivity not certainly to me make suffer but for me give of the fun the tank of beautiful days similar to a pool at half-height of which they made shimmer a azure wet with light that covered a moment intangible and white like a emanation of the heat a veil reflected and fleeting nor the room purely aesthetic of evenings pictorial it was the room where I had been since so many of days that I not it saw anymore.8
The sentence was chosen at random among sentences that include the word joie, which I translated as fun but otherwise left ChatGPT’s choices untouched. The LLM itself offered, unbidden, a slight improvement on the Lego assemblage:
This was no longer the room, still powerful on my sensitivity, certainly not enough to make me suffer, but to give me joy, the tank of beautiful days, similar to a pool at half-height of which they made a wet light shimmering azure, that an impalpable and white veil, reflected and fleeting, covered for a moment, like an emanation of the heat; nor the purely aesthetic room of pictorial evenings; it was the room where I had been for so many days that I no longer saw it.
Note that the adjectives have been placed before the nouns, where they belong in English. An LLM applies such a rule (or so I imagine) on the basis of statistical analysis of French texts paired with English translations; it’s simple enough to be built in as an a priori rule in a system like Massot’s. The result is syntactically correct and almost comprehensible, but still much less fluent than the sample Massot used to illustrate the system.9
You may object that the author whose character have been gone to bed at good hour is an irrelevant distraction in an essay on formal proofs. One of the Zulip chatterers quoted above complained, as it happens, that yours truly’s posts “…are long, and full of flowery prose and side remarks.” Surely an attention to prose style is even more unwelcome in a mathematical proof.
Not for us rose-fingers, the riches of the Homeric language. Mathematical formulae are the children of poverty.10
But the implication of Massot’s talk, that the next “big improvement” in mathematical communication will take the form of a further impoverishment of the prose in which this communication takes place, is at the very least open to question.
Neither technophile ideology nor the laughter in that auditorium can drown out a substantial philosophical point. Why does it make sense to claim, with Massot, that “the content is the same” when a proof undergoes an automatic translation from one medium to another? Remember that Christian Szegedy’s autoformalization program promises translations in the opposite direction. Whatever the method, the idea that mathematical “content” is nothing more than an instruction set for modular assembly was fashionable a century ago. If Massot and the Lean community really believe that nothing is lost in translation, then they ought to consider heeding Brendan Larvor’s advice, in the article he mentioned in a comment here a few days ago:11
Rather than choosing a metaphor to describe translation between informal proofs and formal derivations with the aim of preserving the Standard View, it might be less question-begging to work up a general account of intra-mathematical translation on a broad evidence-base, and then see what it says about the special case of translations of proofs into formal derivations.
We have been in that room so long that we have to make an effort to see it. I especially recommend reading Larvor’s paragraph about Hamami’s analogy of formalization with compilation to see where this sort of thinking leads.
If, on the other hand, something is lost in translation, in either direction, then the “content” is actually not “the same.” In that case, I would ask why IPAM is not paying more attention to the difference.
In practice, of course, fully unwinding a proof complex enough to warrant such caution, like the classification of finite simple groups, would create an unreadable nightmare. But anyone really interested in the proof would click sparingly and with discernment.
…and, to judge by the quotations reproduced at the beginning of this essay, apparently do…
Buzzard writes that “Bringing down the time it takes to write a proof in an ITP to something nearer to the time it takes to write it on paper would greatly increase take-up of these systems by mathematicians.” Such optimistic projections have been a consistent feature of the formalization rhetoric for several decades. Massot's efforts to make formal proofs readable obviously fits this logic.
Or, translated into 60s California dialect, It’s so sad to watch a sweet thing die.
Surveillance capitalism gets you anyway, I know. My university grants me almost unlimited access to Springer-Verlag publications online but when I’m in a hurry to find a reference I forget to turn off their “Cookies that measure website use, Cookies that help with our communications and marketing, Cookies that help show personalised advertising.” In this way I allow them, in spite of myself, to turn my attention to research into a commodity.
I asked two people who were present at the lecture whether or not Massot had explained how his system works. The next three paragraphs are (essentially) copied from the question I asked in one case. Both agreed that the system is based on a dictionary, but the two gave opposing answers as to whether or not he had actually provided an explanation.
Note added May 11: This is confirmed in an article in today’s Times Higher Education:
Alan Winfield, professor of robot ethics at the University of the West of England, said it was not surprising to see university-based AI fall behind industry given the “vast resources” deployed by private companies. “The energy costs for running a big natural language system can run into several million dollars – for just one training round. How many universities can afford that?” he said.
Some novels do look like this, and that’s not necessarily a bad thing.
I would like to see what Black Mirror would make of the enhancement of human communication, in the classroom or in interpersonal relations, with the help of instantaneous nested clickable hyperlinks. This hasn’t been done yet as far as I can tell. One early episode imagined the possibility of recording of all experience in a format that could be rewound and relived; naturally it didn’t end well.
Reviel Netz, The Shaping of Deduction in Greek Mathematics: A Study in Cognitive History (Cambridge: Cambridge University Press, 2003), 145.
The article is behind a paywall but an enterprising reader can find copies on open websites.
Well it would have been nice...
Hi Micheal, I generally enjoy Silicon Reckoner but was put off by the tone of your first paragraph. Perhaps I am misreading, but one can read the first paragraph as "look at this sorry (and small) bunch of fools who aren't enjoying the sun and are listening instead to a formal proof from Bourbaki's general topology". I was one of this sorry bunch, really enjoyed the talk, and felt that my excitement afterwards was greater than had I used the time for surfing or tooling down Wilshire Boulevard :)
Re how Massot did it? My understanding is that there is no language model involved. Rather it is a "routine" translation from Lean to English, with a (hand coded) dictionary providing subject specific keywords. The result is almost certainly clunky in places, but I think it would be quite good in general. (I like to think of it as writing in the same way that an inexperienced undergraduate might write, when they first learn how to write a proof: very formulaic, somewhat inflexible, easy to get lost in the thickets of needless detail, but comprehensible for the most part.)