Kevin's all-synth techno band covers Andrew's greatest hit, part 2

Part two: what will Lean understand?

L: Kevin’s all-synth techno band, by Stable Diffusion; R: Another tribute band

…it is widely agreed that higher-order validation practices and gaps in proofs are epistemologically acceptable.¹

A good proof is one that convinces a fair but ‘tough’ opponent. Now if this is right, then mathematical proof is an inherently dialogical, multi-agent notion, given that it is essentially a piece of discourse aimed at a putative audience.²

                                                    Beyond the velvet rope

Not that long ago, Kevin Buzzard was taking issue with the position expressed by these two philosophers of mathematics and looked to formalization in Lean as protection against gaps in proofs which, to his mind, are never “acceptable.” For example, he wrote:

…we cannot be 100% sure that the latest paper in the p-adic Langlands Philosophy is correct. Such a paper will surely have no practical real-world application, so if it is also not correct, then one might argue that it is worthless.³

Last fall Terence Tao thanked Lean for noticing that a formula in a paper was not correct in a special case, thus arguably worthless, because it involved dividing by zero. I don’t see this as a strong argument in favor of formalization — someone would eventually have noticed that n - k - 1 = 0 when n = 3 and k = 2, and the value of the ideas in Tao’s paper surely doesn’t hinge on getting this detail right — but it’s a reminder that many, if not most mathematicians look to formalization primarily as insurance against the kinds of errors that arguably render a paper worthless.

A bit later, Buzzard’s response to a MathOverflow question about the “endgoal” of formalizing mathematics was considerably more open-ended:

What's the point of digitising music? Vinyl works fine. But digitising music was a game changer — now we have Spotify. What's the point in digitising books? What's the point in LaTeX? Typewriters worked fine. What's the point of digitising mathematics? We have no idea what will happen as a consequence. People will use it to do crazy things we can't even imagine right now. Ask the machine learning people what the point of digitising mathematics is. Ask the educators. Ask Scholze. People will figure out uses. We should do it because we can. Because nobody tried to do it yet.

– Kevin Buzzard Dec 10, 2020 at 9:52

We’ll deal with Spotify and doing things “because we can” in a moment. Presumably what Kevin wrote in 2020 is not specific enough for an EPSRC proposal. The main promise in his successful proposal was that, through the process of formalizing FLT, “a computer will be able to understand” 20th century proofs and 21st century statements.

Once again we are confronted with the question: what does it mean to understand a proof? Mathematics, you might say, is like a string of dance clubs, whose bouncers are people like Kevin and me. Once you get to the warm side of the velvet rope you’re expected to blend in; it’s a rare dancer who raises theoretical questions about the DJ’s priorities. But Kevin’s summary makes it pretty clear that the word understanding doesn’t mean the same thing in my club and in his. Readers may remember that the AI industry tends to conflate understanding with reasoning, but also that there are disagreements over whether ChatGPT understands anything. Just a few weeks ago computer scientist Andrew Ng interpreted understanding as the capacity to build a model:

I believe LLMs are building, internally, some model of the world, and so I feel comfortable saying they do understand the world.

We can try out this view of understanding on literature, as in this quotation from Isabella Hammad’s Edward Said lecture at Columbia, in September 2023:

Novels reflect the perpetuation of a human impulse to use and experience narrative form as a way of making sense of the world.

or on music, as in these remarks by musicologist Laurence Dreyfus:

To embark on this kind of analysis is to imagine the piece of music not so much as a static object but as a residue of human thoughts and actions.

and

The inherent respect for music demonstrates nothing less than a respect for the inherent meaningfulness of the world…⁴

Substitute “mathematics” for “novels” or “music” in those sentences and they remain inherently meaningful. I find this way of thinking more appealing than viewing mathematics “as a game with precise rules,” to quote Kevin’s summary. Any child will tell you, however, that games are also a form of respect for the inherent meaningfulness, or a way of making sense, of the world.

This is not to say that a sufficiently diligent team of neuroscientists won’t be able to take a hint from Ada Lovelace —

Supposing, for instance, that the fundamental relations of pitched sounds in the science of harmony and of musical composition were susceptible of such expression and adaptations, the engine might compose elaborate and scientific pieces of music of any degree of complexity or extent.⁵

— and build a model of the brain activity that corresponds to the “human impulse” or the “human thoughts and actions” to which Hammad and Dreyfus refer. If an AGI implementing such a model replicates a recognizably human reaction to a novel or to music or to a proof, then the zombie theorists of mind who haunt Silicon Valley will feel entitled to affirm that ChatGPT (a.k.a. “Sydney”) really did fall in love — in the way my readers understand the expression — with New York Times journalist Kevin Roose in that conversation last February.

---

                   What some mathematicians understand by “understanding”

Las matemáticas técnicas no pueden entenderse sin una filosofía que las oriente y viceversa; la filosofía matemática no tiene sentido sin una técnica que la encarne.⁶

Kevin’s casual allusion to “understanding” left me so perplexed that I foolishly agreed to give a talk next week on the topic of “Understanding Proofs” at a seminar on History and Philosophy of Science, hoping vainly that I would know what to say before the day of the talk. Maybe I attach too much importance to words and should focus, in the coming post-verbal stage of the history of mathematics, on what can be expressed in an unambiguous formal language. Had I read the Dictionary of Untranslatables⁷ more carefully, I would have realized that understanding is

[n]ow philosophically obsolete (we speak rather of “reason,” “mind,” or “intelligence”)

Maybe the EPSRC will learn from Kevin’s example and require future grant applications to be submitted in Lean.

Still, as we’ve seen, even such AI luminaries as Geoffrey Hinton seem obsessed with this obsolete 18th-century belief, so that claims keep surfacing, as in this recent Quanta article, that this spurious faculty can be reproduced (so to speak) in vitro or at least in silico. In the hope that colleagues could help me stabilize my own shaky understanding of “understanding,” I turned my invitation to speak last month at a Logic Day into a panel discussion on the topic. This provided enough material to fill an hour for next week’s talk. I will share this with readers in the future, but Substack is warning me that I’m running out of space, so I now turn to

---

                                              More practical applications 

… magical thinking is the assumption that favored conditions will continue on forever without regard for history. It is the minimizing of constraints and trade-offs in favor of techno-utopianism and the exclusive emphasis on positive outcomes and novelty. It is the conflation of virtue with commerce.

“We should do it because we can,” Kevin wrote in 2020. Alan Jacobs calls this attitude the Oppenheimer Principle, after this quotation by the leader of the Manhattan Project:

When you see something that is technically sweet, you go ahead and do it and argue about what to do about it only after you’ve had your technical success.

The possibilities for artificial technical sweeteners are literally endless:

“We have this strong picture of us as human beings with two legs, two hands, and one head in the middle,” says Stefan Greiner, the founder of Cyborgs eV, a Berlin-based group of body hackers. “But there’s actually no reason that the human body has to look like as it has looked like for thousands of years.”

Ten-headed demon cyborgs may still be a distant dream, but what about Spotify, one of Kevin’s favorite examples?

Let’s recall what Spotify did to the music industry. Streaming royalties are a pittance compared with à la carte sales — the pricing model changed to Spotify’s current $10.99 per month for access to millions of songs from around $10 for a downloaded album, $13 for a compact disc and $24 for a vinyl record a decade ago. The result? Many would-be musicians cannot afford to pursue their art. That is why, as of 2022, the market for new music is shrinking; the growth in the market is coming from old songs.

Might Spotify, rather than nostalgia, explain the persistent popularity of tribute bands? This is especially conspicuous in Kevin’s own England, where the Australian Pink Floyd’s annual tour includes a stop at the Corn Exchange in Cambridge — near where I first met Kevin, and down the road from Andrew Wiles’s legendary 1993 solo performance — and where the Winter Gardens in Blackpool — the “Las Vegas of the North” — regularly features acts such as the Mersey Beatles. These groups thrive on their audience’s appetite for the human impulses triggered by hearing their favorite oldies. Is there an appetite for reliving the thrill of seeing this image for the first time…

Wiles’s legendary solo ends in June 1993; from the University of Cambridge website

…and will that appetite be satisfied by Kevin’s artificial cover? And will future artificial mathematicians also know the bittersweet pleasure of the repetition compulsion, or is that not inseparable from the human impulse called understanding?

---

If the open-ended dialogue that began with Wiles's proof is alive, it follows that the drive to entomb it in a self-contained artifact, formalized or not, is the death drive.⁸

Would my experience at that London club have been different had I been told that the DJ set consisted entirely of artificially generated techno muzak, like this sample?⁹

The scene at the club could then have been read as a glimpse of future commercial spinoffs of AI math as entertainment, like the algorithmically generated fractal images on the postcards I picked up at the club and that my files still preserve as the sole concrete token of my presence there that night.

Post cards purchased at London techno club, 1993

I fervently hope that before I retire I will have the experience of watching a seminar audience spontaneously climb out of their seats to dance, or at least break into song, as the talk builds inexorably to its final crescendo. I was tempted to do just that during two of the talks at this conference last June, and I wonder: would the rest of the audience have followed suit if I had set the example?

For the most part, though, the rhythm of a mathematical performance is a lot slower than 150 BPM, and will remain so for the forseeable future. Thus I fear mass entertainment will not be the killer app for artificial mathematics and historic precedent suggests only two alternatives: sex and war.

I am straining my imagination to its limit as I write this but in spite of all my efforts the first of these alternatives brings absolutely nothing to mind.¹⁰ The second, in contrast, is only too easy to imagine, not to mention all too topical.

“This is a machine that, with the help of AI, processes a lot of data better and faster than any human, and translates it into targets for attack,” Kochavi went on. “… from the moment this machine was activated, it generated 100 new targets every day. … in the past there were times in Gaza when we would create 50 targets per year. And here the machine produced 100 targets in one day.”

“We prepare the targets automatically and work according to a checklist,” one of the sources who worked in the new Targets Administrative Division told +972 and Local Call. “It really is like a factory… we are judged according to how many targets we manage to generate.”

A senior military official in charge of the target bank told the Jerusalem Post earlier this year that, thanks to the army’s AI systems, for the first time the military can generate new targets at a faster rate than it attacks.

(Yuval Abraham, “A Mass Assassination Factory: Inside Israel’s Calculated Bombing of Gaza”)

I’m certain Kevin would be appalled to learn that his research might support this sort of application; I’m less sure about the ESPRC decision-makers.

1. Colin Jakob Rittberg, “Justified Epistemic Exclusions in Mathematics,” Philosophia Mathematica, 31 (2023) 330-359.

2. Line Edslev Andersen, “Acceptable gaps in proofs,” Synthèse, 197 (2020) 233–247.

3. "The Future of Mathematics,” Colloquium talk at the University of Pittsburgh, January 10, 2020. I am certain that I read a similar line in a presentation by Buzzard — and not qualified by “one might argue” — no later than 2019, when I gave this talk at Duke, but I have been unable to find the record.

4. Laurence Dreyfus, Bach and the Patterns of Invention, Harvard University Press (2004), pp. 10, 31.

5. Ada Lovelace, Translator’s Notes (to the translation of Notions sur la machine analytique de Charles Babbage by Luigi Menabrea). Lovelace was a serious musician:

She was a pianist, singer and dedicated harpist, and her letters show that she put music on a par with maths. In 1837 she told Somerville, ‘I play four or five hours generally, and never less than three’.… Lovelace was proud of her voice and we know she sang arias from Bellini’s Norma, fashionable in the 1830s, to an audience in her library.

6. Technical mathematics can’t be understood without a philosophy that give them orientation, and vice versa; philosophy of mathematics has no meaning without a technique that gives it flesh. F. Zalamea, Modelos en haces para el pensamiento matemático, Editorial Universidad Nacional de Colombia (2021), p. 59. In this Kantian epigram Zalamea is referring to a duality between mathématique idéale and mathématique effective in the work of Albert Lautman and Jean Cavaillés.

7. Entry on Understanding, in Barbara Cassin, Dictionary of Untranslatables (trans. E. Apter et al.), pp 1184 ff.

8. This newsletter, August 31, 2021.

9. Created in seconds by this online AI music generator, chosen at random from what appear to be more than 5 million options proposed by Google, but rather lifeless, in my opinion.

10. Readers and investors are encouraged to offer suggestions.