Formal Proof

This month's Notices of the American Mathematical Society is highlighting formal proof, which is a proof where every step is justified with respect to the axioms of mathematics so there is no chance of error. Generally, this would be extremely tedious to do by hand so people have been developing computerized proof assistants to help do the job. My good friend and former colleague at the University of Pittsburgh, Tom Hales penned one of the articles. I actually lured Tom from Michigan to Pittsburgh several years ago. At that time, Tom had recently finished his proof of the Kepler conjecture, which asserts that the densest arrangement of balls in three dimensional space is face-centered cubic (FCC) packing. He had been battling with the editors of the Annals of Mathematics to get his proof published. The problem was that Tom's proof was quite long (300 pages) and used a computer. Tom's strategy for the proof was to show that all possible packings in infinite space could be reduced to a finite number of arrangements, which needed to be tested individually. Tom and a student then wrote a program with about forty thousand lines that used interval arithmetic to show that none of these other arrangements was ever denser than FCC. A panel of experts worked on reviewing the proof and essentially gave up. They were pretty sure it was right but were unwilling to certify it. Eventually, the Annals published the proof with an asterisk that it was not fully checked by referees. I may have played a small part in helping Tom finally get the proof published. I remember going down to Tom's office one day. He was slumped in his chair and declared that he was giving up on the Annals and writing a book instead. I convinced him not to give up and gave him some tips on the strategy to deal with the editors and referees. I'm not sure exactly what happened but the next time I saw Tom he was beaming that the work would finally be published.

However, Tom was so frustrated with the whole episode that he decided that he needed to prove the Kepler conjecture formally, so that the asterisk could be removed. He began what he called the Flyspeck project, which is a stylized acronym for Formal Proof of Kepler. He's already recruited a number of mathematicians around the world to work on Flyspeck and nearly half of the computer code used to prove the Kepler conjecture is now certified. He estimates that it may take as long as twenty work years to complete the project so if he gets enough people interested it can be done quite quickly in real time.

A formal proof essentially involves translating mathematics into symbol manipulation that is encapsulated within a foundational system. Tom uses a system called HOL Light (an acronym for lightweight implementation of Higher Order Logic), which I'll summarize here. The details are fairly technical; they involve using a new axiomatic or logical system that involves types (similar to what is used in computer languages like C). HOL Light differs slightly from the Zermelo-Fraenkel-Choice axioms of set theory used in traditional mathematics. The use of types means that certain incongruous operations that any mathematician would deem nonsensical (like taking the union of a real number and a function), would automatically be disallowed. The system then involves mathematical statements or objects called terms involving symbols and logical operations or inference rules. Theorems are expressed as a set of terms called the sequent that imply the truth (or more accurately the provability) of another term called the conclusion. Proofs are demonstrations that using the allowed inference rules and axioms, it is possible to arrive at the conclusion.

What I like about formal proofs is that it reduces mathematics to dynamical systems. Each term is a point in the theorem space of all terms (whatever that means). A proof is then a trajectory between the initial condition (the sequent) and the conclusion. Technically, a formal proof is not a true dynamical system because the next step is not uniquely specified by the current state. The fact that there are multiple choices at each step is why theorem proving is hard. Interestingly, this is connected to the famous computer science problem of whether or not P=NP. Theorem proving is in the complexity class NP because any proof can be verified in polynomial time. The question is whether or not a proof can be found polynomial time. If it can be shown that this is possible then you would have a proof of P=NP and get a million dollars from the Clay foundation. It would also mean that you could prove the Riemann Hypothesis and all the other Clay Millennium problems and collect for those as well. In fact, if P=NP you could prove all theorems in polynomial time. This is one of the reasons why most people (including myself) don't think that P=NP.

I think it would be very interesting to analyze the dynamics of formal proof. So many questions immediately come to my mind. For example, what are the properties of theorem space? We know that the set of all theorems is countable but the set of possible terms is uncountable. A formal system consists of the space of all points reachable from the axioms. What does this look like? Can we define a topology on the space of all terms? I suppose a metric could be the fewest number of steps to get from one term to another term, which might be undecidable. Do people even think about these questions?