This article was published in Scientific American’s former blog network and reflects the views of the author, not necessarily those of Scientific American
This is a revised version of a post that originally appeared on the American Mathematical Society’s Joint Mathematics Meetings blog.
Earlier this month, I attended the Joint Mathematics Meetings in Seattle. One of the reasons I enjoy going to the JMM is that I can get a feel for what is going on in parts of mathematics that I’m not terribly familiar with. This year, I attended two talks in a session called “mathematical information in the digital age,” that got me thinking about what mathematicians do.
First, a confession: I went to the session because I like oranges. The first talk was by Thomas Hales, who is probably best known for his proof of the Kepler conjecture. In short, the conjecture says that the way grocers stack oranges is indeed the most efficient way to do it. The proof was a long 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 took more than a decade to write and verify a formal computer proof of the result. I attended the talk because I figured there’s a small chance that any talk that mentions the Kepler conjecture might have oranges for the audience.
On supporting science journalism
If you're enjoying this article, consider supporting our award-winning journalism by subscribing. By purchasing a subscription you are helping to ensure the future of impactful stories about the discoveries and ideas shaping our world today.
Hales’ talk was called simply “Formal Proofs.” These are not proofs that are written using stuffy language, with every single step written out, but proofs that can be input into a computer and verified all the way down to the foundations of mathematics, whichever foundations one chooses.
Hales began his talk with some examples of less-than-formal proofs, starting with a passage from William Thurston in which he used the phrase “subdivide and jiggle,” clearly not a rigorous way to describe mathematics. (Incidentally, Thurston also did mathematics with oranges. He would ask students to peel oranges to better understand 2- and 3-dimensional geometry.)
Although I never met Thurston, I am one of his many mathematical descendants. his approach to mathematics, particularly his emphasis on intuition and imagination, has permeated the culture in my extended mathematical family and has had a great deal of influence on how I think about mathematics. That is why it was so refreshing for me to go to a talk where intuition wasn’t a primary focus.
Hales was certainly not insinuating that Thurston was a bad mathematician. Thurston was only the first mathematician he used as an example of less-than-rigorously stated mathematics. 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, is not really full of formal proofs.
Hales’ talk was a nice overview of the formal proof programs 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 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. The logical response: why doesn’t Mochizuki do it himself? Let’s just say I’m not holding my breath.
The second talk I attended in the session was Michael Shulman’s called “From the nLab to the HoTT book.” He talked about both the nLab, a wiki for category theory, and the writing of the Homotopy Type Theory “research textbook,” a 600-page tome put together during an IAS semester about homotopy type theory, an alternative to set theory as a foundational system for mathematics. 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 and verify new truths more quickly is not more important to me.
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 didn’t end up with any oranges, but I got some interesting new-ti-me perspectives about how and why we prove.
*almost no