William Thurston was the first example Thomas Hales gave in his talk on Thursday morning about formal proof. To be clear, Thurston was not an example of a formal prover but of the imprecision with which mathematicians often treat their subjects. Hales cited a passage from Thurston in which he used the phrase “subdivide and jiggle,” clearly not a rigorous way to describe mathematics.
Although I never met Thurston, I am one of his mathematical descendants. His approach to mathematics, particularly his emphasis on intuition, has permeated the culture in my extended mathematical family and has a great deal of influence on how I think about mathematics. That is why it was so refreshing for me to go to a session where intuition wasn’t really on the radar.
Hales was certainly not insinuating that Thurston was not a good mathematician. Thurston was the first mathematician he mentioned as an example of less-than-rigorously stated mathematics, but a few slides later he mentioned the Bourbaki book on set theory. Yes, even that paragon of formal mathematics sucked dry of every drop of intuition, falls short when it comes to formal proofs.
By formal proofs, Hales is not referring to Bourbaki-style mathematics but to proofs that can be input into a computer and verified all the way down to the foundations, whichever foundation one chooses. Hales is famous for his proof of the Kepler conjecture that says that the way grocers stack oranges is indeed the most efficient way to do it. The proof was a case-by-case exhaustion, and Hales was not satisfied with a referee report that said the referee was 99% sure the proof was correct. So he did what any* mathematician would do: he spent the next decade-plus writing and verifying a formal computer proof of the result. (Read more about this project, called Flyspeck, on the Aperiodical.)
Hales’ talk was for me a nice overview of the formal proof programs are out there, some mathematical results that have been proved formally (including some that were already known), and a nice introduction to where the field is going. I’m particularly interested in learning more about the QED manifesto and FABSTRACTS, a service that would formalize the abstracts of mathematical papers, a much more tractable goal than formalizing an entire paper.
The most amusing moment of the talk, at least to me, was a question from someone in the audience about the possibility of using a formal proof assistant to verify Shinichi Mochizuki’s proof of the abc conjecture. Hales replied that with the current technology, you do need to understand the proof as you enter it, so there aren’t many people who can do it. Perhaps Mochizuki can write it himself? Let’s just say I’m not holding my breath.
I attended two talks in the AMS special session on mathematical information in the digital age of science on Thursday morning. The first was Hales,’ and the second was Michael Shulman’s called “From the nLab to the HoTT book.” He talked about both the nLab, a category theory wiki, and the writing of the Homotopy Type Theory “research textbook,” a 600-page tome put together during an IAS semester about homotopy type theory. The theme of Shulman’s talk was “one size does not fit all,” either in the way people collaborate (contrasting the wiki and the textbook) or even in the foundations of mathematics (type theory versus set theory).
I don’t know if it was intended, but I thought Shulman’s talk was an interesting counterpoint to Hales,’ most relevantly to me in the way it answered one of the questions Hales posed: why don’t more mathematicians use proof assistants? Beyond the fact that proof assistants are currently too unwieldy for many of us, Shulman’s answer was that we do mathematics for understanding, not just truth. He said what I was thinking during Hales’ talk, which was that to many mathematicians, using a formal proof assistant does not “feel like” mathematics. I am not claiming moral high ground here. It is actually something of a surprise to me that the prospect of being able to find new truths more quickly is not more tantalizing.
You never know what you’re going to get when you wander into a talk that is well outside your mathematical comfort zone. In my case, I got some interesting challenges to my thinking about how and why we prove.