The final session of the first day of the joint British Mathematical Colloquium in Cambridge was a panel discussion on The Future of Proof. The panellists were June Barrow-Green, Timothy Gowers, Andrew Pitts and David Tranah.
David Tranah, from Cambridge University Press, said he was invited to ‘say something controversial’, and duly obliged, by making an alarmingly persuasive case that mathematics journals—he described them as ‘junk mail’—were now pointless as a way of disseminating new results, and that since the author (or her institution, via REF funding) is the main person to benefit from publishing in a refereed journal, she (or it) should pay.
He also commented on the inconsistency and burden of refereeing, and endorsed a system of post publication review, organized around an arXiv-like frontend (but better). I’m starting to believe this will happen. In some sense it already does for the best papers, since they’re read on the arXiv, and discussed informally, long before they appear in journals. Maybe in fifty years only bad papers will get published in the traditional way: then journals will once again serve a useful purpose.
Back onto proof, the role of computers dominated the discussion. It transpired that David was not the only panel member trying to do himself out of a job. Timothy Gowers mentioned his work on theorem proving by computer and predicted that by 2100 computers would be so good at proving theorems that there would be ‘not much room left for the practice we currently engage in’.
Gowers began, less worryingly, by emphasising that proofs are not just certificates of correctness: ideally they should give an idea of ‘why it’s true’, and have a beauty and interest in their own right. He asked whether it was possible to formalize these aspects. I’m even more sceptical about this. These feel like aesthetic qualities to me that I think will resist formalisation. However, there was agreement across the panel that any computer that could prove new theorems would also have the exploratory capacities needed to discover new results likely to be of human interest: this seems to imply some kind of limited aesthetic judgement. (And regrettably, it rules out the remaining job for a human pure mathematician, as ring-master of a computational circus.) Gowers later said that getting a computer to find proofs should be a strictly easier problem than AI.
In 75 minutes there were many aspects that weren’t touched on. Thinking about Lara Alcock’s talk at the meeting Evidence Based Mathematics Teaching earlier this month, I started to think dangerous thoughts about the usefulness (or otherwise) of putting proofs at the centre of our teaching, when most of the people we are teaching clearly get little out of them. June mentioned the controversial article by Jaffe and Quinn, and subsequent responses in the letters page of the AMS Bulletin. I was surprised no-one mentioned Zeilberger’s enthusiastic use of computers in his work.
There was some light-hearted scorn for foundations: Gowers gave the ‘normal mathematicians’ view that foundations don’t really matter for most work: anything we’re likely to do can be formalised, if necessary, in ZF, or maybe ZFC. Andrew Pitts said that set theory was not a very convenient foundation for automated theorem proving, and that a foundation that allowed easy inductive proofs and definitions was more important in his work. As a small counterargument, June Barrow-Green gave a very interesting historical perspective, pointing out that while formalism and logicism were ultimately undermined by Gödel’s Incompleteness Theorem, the work of Peano and others does at least put proofs on a rigorous footing. If Gowers’ optimistic-for-computers / pessimistic-for-humans view is right then maybe formal proofs (or at least, proofs produced by a recognisably formal process) will get new life. Zeilberger, however, would disagree.