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.
The post Timothy Chow on the NF consistency proof and Lean appeared first on Logic Matters.
