Boris Giltburg and the Pavel Haas play Brahms

We had tickets for the Sunday morning Wigmore Hall concert with the Pavel Haas Quartet playing Smetana and Janacek, our first post-Covid occasion to see them play live.

But, so it turned out, there were no trains from Cambridge North that morning. Which was, shall we say, massively disappointing.

Consolation: three of the Quartet played again at Wigmore Hall on Monday night too, joining Boris Giltburg to play the first two of Brahms’s Piano Quartets, and that concert was broadcast live on BBC Radio 3. You can listen here for another month.

I’m not (yet) bowled over by the second quartet — the piece, not the performance. But the first quartet (after the interval) is terrific and the playing everything you’d expect and more. Listen from 1.17 into the concert. Wonderful!

The shape of categorial things to come

The headline news: there is now a new version of my category theory notes, in one document, as Introducing Category Theory, available here.

In more detail: I’ve decided against my previous plan of two volumes, in part because there just wasn’t a satisfyingly natural way of carving things between them. (Friends and relations, by a large majority, also voted for one big book rather than two smaller ones.)

As the notes are now arranged, Part I says something about what can be found inside individual categories (products, quotients, limits more generally, exponentials and the like). Part II says a very little about those categories which are elementary toposes. Part III, which can be read independently of Part II, introduces the distinctive categorial  ideas of functors, natural transformations, the Yoneda Lemma, and adjunctions.

If you haven’t seen earlier versions, I have gone for a fairly conventional mode of presentation but at a pretty gentle pace (which makes for quite a long book — but I make no apology for that: faster-track alternatives are available in you want them!). The result is aimed at those who want an entry-level warm-up before taking on an industrial-strength graduate-level course, or perhaps just want to get an idea of that the categorial fuss is about.

The state of play? Part I should be in a good state. One chapter is missing from Part II. Part III needs a concluding note on further reading. The index needs work. But I’m getting there!

A print-on-demand version will be inexpensively available (Amazon only, to minimize cost) in due course — by the end of July, I hope.

A print-on-demand version of Part I (and a little more) has been available under the title Category Theory I: A Gentle Prologue. This now strikes me as making an unsatisfactory division of the material, stopping precipitously. [Updated] However, I have decided to keep it in print for the moment, and in a day or so a new version, updated to correct typos and a few thinkos, should go live on Amazon.

Another round with ChatGPT

ChatGPT is utterly unreliable when it comes to reproducing even very simple mathematical proofs. It is like a weak C-grade student, producing scripts that look like proofs but mostly are garbled or question-begging at crucial points. Or at least, that’s been my experience when asking for (very elementary) category-theoretic proofs. Not at all surprising, given what we know about its capabilities or lack of them.

But this did surprise me (though maybe it shouldn’t have done so: I’ve not really been keeping up with discussions of  the latest iteration of ChatGPT). I asked — and this was a genuine question, hoping to save time on a literature search — where in the literature I could find a proof of a certain simple result about pseudo-complements (and I wasn’t trying to trick the system, I already knew one messy proof and wanted to know where else a proof could be found, hopefully a nicer one). And this came back:

So I take a look. Every single reference is a total fantasy. None of the chapters/sections have those titles or are about anything even in the right vicinity. They are complete fabrications.

I complained to ChatGPT that it was wrong about Mac Lane and Moerdijk. It replied “I apologize for the confusion earlier. Here are more accurate references to works that cover the concept of complements and pseudo-complements in a topos, along with their proofs.” And then it served up a complete new set of fantasies, including quite different suggestions for the other two books.

Now, it is one thing ChatGPT being unreliable about proofs (as I’ve said before, it at least generates reams of homework problems for maths professors of the form “Is this supposed proof by Chat GPT sound? If not, explain where it goes wrong”). But being utterly unreliable about what is to be found in the data it was trained on means that any hopes of it providing even low-grade reference-chasing research assistance look entirely misplaced too.

Hopefully, this project for a very different kind of literature-search AI resource (though this one aimed at philosophers) will do a great deal better.

Climate change

Some years ago, the University Botanic Gardens here in Cambridge started a special area for the interest of local gardeners, displaying plants particularly tolerant of the low local rainfall. Because this part of East Anglia officially counted as a ‘semi-arid’ region.

Today, another sodden day. And our garden, if not awash, is lush to say the least. We used to get a lot of grey days with occasional drizzle; but recently it has repeatedly been raining proper rain, extraordinarily so for Cambridge.

At least the students revising and revising before Tripos starts (this week, for many) aren’t sweltering. An old Cambridge trick was glorious weather before and during exams, breaking just in time for the post-exam festivities ….

I see the first Maths Part III examination is on Thursday. Oh, so very good luck to all: I still feel for you! And heavens, there are now over 250 candidates for Part III. Back in the olden days, it didn’t used to be quite like that. A friend found he still had a copy of the Reporter with exam results for the year we graduated, and sent me this:

The stars indicate distinction (yes, yes, it’s been downhill all the way since). And “Ds” is for “dominus”, i.e. someone who had already graduated — so those whose names are unadorned took Part III at the end of their third year, while still undergraduates, which now seems crazily fast.

And no “Dna” for “domina”? Indeed no. Not one single woman took Part III that year.

So here at least there has been a welcome climate change. It’s still very male dominated, and we can debate the reasons for that: but it certainly isn’t now an exclusive boys’ club.

Two category theory books

One of the best freely available sets of lecture notes on category theory available is the one by Paulo Perrone, which can be downloaded from the arXiv here. He has now turned these notes into a printed book, Starting Category Theory from World Scientific. There is a long added chapter on monoidal categories, but the earlier five chapters appear again with only some small additions as far as I can see on a quick browse (the significantly higher page count for these chapters being mostly due to the difference in formatting).

Since the lecture-note version is freely and officially available, I won’t comment in detail here: suffice to say that Perrone makes the material pretty accessible, and I can well imagine many students liking his style. I really, really doubt that they (or you) will want to fork out for the book, however. Its USA price is $148 (there’s a whopping $11 discount on Amazon); its UK price is £135. That is worse than absurd.

I may just possibly have said something here about another category theory book’s being on its way. Namely, my Category Theory II. But plans are a bit fluid right now. For various reasons, I’m increasingly minded to in fact combine Parts I and II (with again a slightly re-arranged ordering of chapters) into a single big book, perhaps reverting to that earlier title Category Theory: Notes towards a gentle introduction for the whole.

In fact the cost of one big printed book would only be about the price of a large coffee more than a separate Category Theory II, and the small additional overall cost to someone who already has Category Theory I would be more than compensated by avoiding the repeated annoyance of having to chase up cross-references between books (or between PDFs). And there are other significant potential gains too: the combined book as I now see it has a nicer shape. But I’ll keep thinking this through: so watch this space.

Timothy Chow on the NF consistency proof and Lean

Timothy Chow has sent a long comment, adding to the discussion following the previous post NF is really consistent. I think the points he makes are interesting enough to highlight as a standalone guest post. He writes:

First, let me congratulate Randall and Sky on a magnificent achievement!

I’m afraid I have to agree with Randall that the likely response of the mathematical community is a polite yawn. That is unfortunate, because there are several reasons why people should be excited about this work.

The first reason is simply that a difficult, well-known, and longstanding conjecture has finally been proved, via a brilliant argument that uncovers deep structure in an unexpected place. I don’t know what mathematics is, if not the uncovering of deep and unexpected structure. If the subject in question were anything other than mathematical logic, which many mathematicians are unjustly prejudiced against, the champagne corks would already be popping.

Even many set theorists seem to be prejudiced against NF. There are standard complaints that it presents a strange and unmotivated foundation for set theory. But as you can see from older papers on his webpage, Randall has long ago addressed these objections. The time is long overdue for a re-evaluation of the possible role that NF might play in the foundations of mathematics. Note that NF has type-theoretic origins; type theory is experiencing a renaissance of sorts nowadays, so it is especially appropriate for NF to be given a fresh look.

A second, and totally different, reason to be excited about this piece of research is that it convincingly demonstrates the value of proof assistants in the process of producing new mathematical knowledge. Not all readers of this blog may be aware of the history of this proof of the consistency of NF. Randall announced the result over ten years ago, and submitted a paper for publication, but the editor did not want to publish it until a referee could be found who was able to independently vouch for its correctness, and no such referee was forthcoming, because the proof was so complicated. This state of affairs highlights one of the weaknesses of our peer review system; if a proof is very complicated and there is uncertainty about its correctness, then referees are typically reluctant to invest a lot of time checking it, because if the proof turns out to be wrong, then they will likely have wasted a lot of time that they could have spent pursuing more rewarding activities. People don’t want to read the proof until they’re sure it’s correct, but there’s no way for the proof to be recognized as correct until people read it. In the absence of a proof assistant, an author in possession of a correct but complicated proof is caught in a vicious cycle.

This is one major reason we should be grateful for proof assistants; they allow us to break the impasse. Rowsety Moid’s initial comment betrays a lack of understanding of this point. To say that the correctness of a proof rests on “the judgement of competent mathematicians who understand the proof” is partially correct, but fails to acknowledge that sometimes, human mathematicians are unable to arrive at such an understanding and judgment without machine assistance. Randall began with a basically correct proof, but the process of communicating the proof to other humans (which you might think is a purely human activity) turned out to be impossible until a proof assistant entered the picture. Furthermore, Lean did not simply play a purely passive role, dully checking a proof that had been completely spelled out by the humans in advance. As Randall will be quick to acknowledge, the process of coaxing Lean to certify the argument was not a monologue by the humans, but a dialogue that forced the humans to rethink, clarify, and improve the argument. Lean is truly an interactive proof assistant; we are entering a new era in which proof assistants are becoming vital partners in the creation of proofs, not just by performing routine calculations, but by engaging us in interactive dialogue.

Of course, some of these lessons were already learned with Flyspeck or Gonthier’s proof of the four-color theorem, etc. But a new feature of the proof that NF is consistent is that it demonstrates that what might seem to be a purely sociological issue (the difficulty of persuading a referee to check a proof and thereby allowing the proof to be assimilated into the body of accepted mathematical knowledge) can in fact be addressed with the help of an interactive proof assistant, which has infinite patience, and no pressing need to advance its own career by spending its time on more “important” tasks.

NF really is consistent

About eighteen months ago, I noted here that a project was underway to verify Randall Holmes’s rather impenetrable claimed proof of the consistency of NF, using the Lean proof verification system.

The project has now been completed by Sky Wilshaw, a Part III student in Cambridge, building on the earlier work of some other students. Here is a new paper by Holmes and Wilshaw explaining the proof in its current version. The introduction reads:

We are presenting an argument for the consistency of Quine’s set theory New Foundations (NF). The consistency of this theory relative to the usual systems of set theory has been an open question since the theory was proposed in 1937, with added urgency after Specker showed in 1954 that NF disproves the Axiom of Choice. Jensen showed in 1969 that NFU (New Foundations with extensionality weakened to allow urelements) is consistent and in fact consistent with Choice (and also with Infinity and with further strong axioms of infinity).

The first author showed the equiconsistency of NF with the quite bizarre system TTT (tangled type theory) in 1995, which gave a possible approach to a consistency proof. Since 2010, the first author has been attempting to write out proofs, first of the existence of a tangled web of cardinals in Mac Lane set theory … and then directly of the existence of a model of tangled type theory. These proofs are difficult to read, insanely involved, and involve the sort of elaborate bookkeeping which makes it easy to introduce errors every time a new draft is prepared. The second author (with the assistance of others initially) has formally verified the proof of the first author of the existence of a model of TTT, and so of the consistency of New Foundations, in the Lean proof verification system, and in the process has suggested minor corrections and considerable formal improvements to the argument originally proposed by the first author. The second author reports that the formalized proof is still difficult to read and insanely involved with nasty bookkeeping. Both authors feel that there ought to be a simpler approach, but the existing argument at least strongly resists attempts at simplification.

‘Quite bizarre system’, ‘insanely involved with nasty bookkeeping’ eh? There have been rather more inviting introductions to papers! But still, an insanely intricate and messy but verified-in-Lean proof of consistency relative to a fragment of ZFC is a consistency proof.

My strong impression, however, is that the general lack of love for NF among set-theorists hasn’t latterly been really grounded in lively doubts about its consistency. So I rather suspect that, even though the proof resolves a very long-standing open problem, its wider impact might be quite modest. Still, all credit to Randall Holmes for having brought his proof project to a successful outcome.

Jonathan Bennett (1930-2024), Michael Tanner (1934-2024)

The deaths have been announced of two Cambridge philosophers.

Jonathan Bennett was here from 1956–1968, and I was and remain a huge admirer. His early little book Rationality is a masterpiece, and for a good few years I was much intrigued by his defence of a Gricean programme in the philosophy of language which comes to fruition in his Linguistic Behaviour. And when it came to my retirement and I had to radically downsize my ludicrously big library, one of the few history of philosophy books that I couldn’t bear to let go was his Kant’s Analytic which still strikes me as the very paradigm of how to make the Great Dead Philosophers live as exciting interlocutors with something to say which is still worth grappling with. His energetic, direct, straight-talking style as a philosopher I found inspirational over the years.

Bennett was a prolific publisher, not so Michael Tanner, who spent his whole career in Cambridge, first as an undergraduate and then from 1961 until his retirement in 2002 as a lecturer. But he had a great cultural influence on many students over the years, in the way that dons of a different era could do. His Wagner evenings were legendary (and his eventual short book Wagner is a terrific read, even for those of us who never quite caught the bug). And he became a wonderful reviewer of CDs for the BBC Music Magazine, and of opera for the Spectator. He was passionately engaged, opinionated, insightful because — as a loyal Leavisite — he thought such things really mattered to life. (For some reminiscences, see the comments on Brian Leiter’s blog here.)

Scroll to Top