This and that

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.

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.)

Three things to read …

The death was announced a few days ago of W.W. Tait, whose work I have much admired over the years. His early technical work was on proof theory, and then he wrote with great knowledge and insight on the philosophy of mathematics and its history. His collection of papers The Provenance of Pure Reason is a must-read, and more excellent papers can be found on his otherwise minimalist website here. One piece of Tait’s which I can’t remember reading before and which will surely be of interest to anyone reading this blog is his piece contributing to Philosophy of Mathematics: 5 Questions: you can read it here.

Brian Leiter’s blog linked yesterday to a piece by a one-time colleague of mine, Leif Wenar, lambasting the pretentions of the “effective altruism” cult. I laughed out loud at his (surely just) comment that “To anyone who knows even a little about aid, it’s like [Will] MacAskill has tattooed “Not Serious” on his forehead.”. But this is serious stuff, and well worth a read here.

For some hard-core logical reading, here is another one-time colleague in action. Tim Button has just posted on the arXiv a forthcoming JSL paper “Wand/Set Theories: A realization of Conway’s mathematicians’ liberation movement, with an application to Church’s set theory with a universal set”. Tim describes a template for introducing mathematical objects which prima facie is much more liberal than standard set theory provides. Indeed it seems to very nicely encapsulate Conway’s liberation movement, allowing that (in Conway’s words)

(i) “Objects may be created from earlier objects in any reasonably constructive fashion.

(ii) Equality among the created objects can be any desired equivalence relation.”

Note, though, that Conway expected that any theory whose objects are so created in such a “reasonably constructive” fashion can be embedded within (some extension of) ZF. Tim aims to prove a stronger theorem: all loosely constructive implementations of the Wand/Set Template are not merely embeddable in (some extension of) ZF, but synonymous with a ZF-like theory. Which seems a surprise.

Markdown joy

A minor improvement here …

You can now use simple Markdown syntax (you know the kind of thing, *italics* for italics, **bold** for bold) in comment boxes.

This is explicitly signalled in comment boxes on the blog; but it is also the case with comment boxes on static pages.

(Nerdy trivia: this is enabled by using the multi-purpose Jetpack plugin — which is wild overkill: but I’ve turned off more or less every other Jetpack option so I hope that nothing is inadvertently broken.)

Core logic again

I have mentioned Neil Tennant’s system(s) of what he calls Core Logic once or twice before on this blog, in friendly terms. For the very shortest of introductions to the core idea of his brand of relevant logic, see my post here on the occasion of the publication of his book on the topic. (And there is a bit more info here in a short note in which I respond to some criticisms on Neil’s behalf — unnecessarily, it turned out, as he published his own rejoinder.)

I notice that Neil has now written a piece outlining his developed ideas on Core Logic for Philosophia Mathematica. If you want to know more, this might be a good place to start. You can download this paper here.

The blog is eighteen!

Post #1 was back on March 9th, 2006. And here we are again, with post #1715, and with the blog yet another year older, if not a year wiser. I’ll raise a glass.

Since its last birthday, I’ve started to put together archive pages to make it easier to find those old posts which may (or then again, may not) be still worth reading. I really must make the effort to complete that job.

But I’m afraid that just recently there hasn’t been so very much happening here. However, the end of the category theory project really, really, is in sight now, and when it at last gets off my desk, I do hope to have a bit more time and energy to devote to posting more often. For a start, there’s a pile of books — and not just logic books — I’d like to say something about.

Today though, my self-denying ordinance stands: it’s back to concentrating on reworking the final few pages of Category Theory II … Wish me luck.

Miracle on St David’s Day.

St Davids Cathedral. Wales

I have just noted, with delight, that the poet Gillian Clarke — the much admired, much loved, one-time National Poet of Wales — has a new collection of poems coming out from Carcanet Press this month. We have read and reread and read her work again ever since we lived in Wales, and find it so deeply appealing. If by some ill chance, you haven’t really come across her poetry, try — yes, do try — her Selected Poems of 2016, or at least browse her website.

In this new book, we are told, “The poems in … The Silence begin during lockdown, to whose silences Clarke listens so attentively that other voices emerge. As the book progresses, that silence deepens, in the poems about her mother and childhood, about the Great War and its aftermaths, and in her continuing attention to Welsh places and names, and the rituals which make that world come in to focus. In these scrupulous, musical poems, Clarke finds consolation in how silence makes room for memory and for the company of the animal- and bird-life which surrounds us. These poems, compulsively returning to key images and formative moments, echo and bring back other ways of living to the book’s present moment.”

Since the poem is on her website, I hope that Gillian Clarke will forgive me if I reproduce here a particularly touching poem of hers, appropriate to the day, dating back to a real event in the 1970s.

Miracle on St David’s Day.

‘They flash upon that inward eye
which is the bliss of solitude’
(from ‘The Daffodils’ by William Wordsworth)

An afternoon yellow and open-mouthed
with daffodils. The sun treads the path
among cedars and enormous oaks.
It might be a country house, guests strolling,
the rumps of gardeners between nursery shrubs.

I am reading poetry to the insane.
An old woman, interrupting, offers
as many buckets of coal as I need.
A beautiful chestnut-haired boy listens
entirely absorbed. A schizophrenic

on a good day, they tell me later.
In a cage of first March sun a woman
sits not listening, not feeling.
In her neat clothes the woman is absent.
A big, mild man is tenderly led

to his chair. He has never spoken.
His labourer’s hands on his knees, he rocks
gently to the rhythms of the poems.
I read to their presences, absences,
to the big, dumb labouring man as he rocks.

He is suddenly standing, silently,
huge and mild, but I feel afraid. Like slow
movement of spring water or the first bird
of the year in the breaking darkness,
the labourer’s voice recites ‘The Daffodils’.

The nurses are frozen, alert; the patients
seem to listen. He is hoarse but word-perfect.
Outside the daffodils are still as wax,
a thousand, ten thousand, their syllables
unspoken, their creams and yellows still.

Forty years ago, in a Valleys school,
the class recited poetry by rote.
Since the dumbness of misery fell
he has remembered there was a music
of speech and that once he had something to say.

When he’s done, before the applause, we observe
the flowers’ silence. A thrush sings
and the daffodils are flame.

Scroll to Top