Saturday, November 22, 2008

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?


Artur Adib said...

Neat. I guess Hilbert's program is not completely dead yet!

So, in this dynamical system language, does the conclusion correspond to a fixed point? If so, in light of Goedel's theorem, does that mean that not all theorems have fixed points (computability)? Does it also mean that NP-completeness can be quantified in terms of the time to reach the fixed point (complexity)?

Carson C. Chow said...

Hi Artur,

Hilbert's program is partially dead. While you can fully verify a proof, you still cannot decide if some conjecture is provable. Goedel's first incompleteness theorem says that there will remain statements that are true but not provable.

I wouldn't call a theorem a fixed point because the system is not really a dynamical system. Moves are never forced. A conclusion is just another term, which can then be operated on or not. It's more like building with lego. At any point you can attach a piece. A proof is then showing that you can build a certain structure starting from another just using the pieces you have.

All proofs are in NP because they can be verified in polynomial time. Theorem proving is NP complete because it can be reduced to SAT. Your question is more one of implementation rather than complexity. The latter merely asserts the asymptotic properties of the algorithm while the former looks for best algorithms. Actually, even if P=NP you still might not be able to prove all theorems right away. Some algorithms might go like N^10000000, which is only better than exp(N) for N really really big. However, if P=NP it does mean that it is just a matter of time before all theorems are proved. If P not equal NP, then some theorems may be intractable.

Steve Hsu said...

"strategy for the proof was to show that all possible packings in infinite space could be reduced to a finite number of arrangements"

Is that really true, or is it more subtle how the seemingly infinite set of configurations is reduced to a finite set of things to check?

Carson C. Chow said...

Hi Steve,

It is a lot more subtle obviously. The bottom line as you surmised is that there are only a finite number of things to check. However, as I recall how Tom explained it to me (which was quite awhile ago), I think it does boil down to the fact that you only need to check a finite number of arrangements. The real trick was that you can use linear programming to do the test, which is why it was tractable. If you are out there Tom, is this right?


Steve Hsu said...

L. Fejes Tóth

Thus it seems that the problem can be reduced to the determination of the minimum of a function of a finite number of variables, providing a programme realizable in principle. In view of the intricacy of this function we are far from attempting to determine the exact minimum. But, mindful of the rapid development of our computers, it is imaginable that the minimum may be approximated with great exactitude.

Was Fejes Toth Tom's advisor?

Carson C. Chow said...

Hi Steve,

No, Fejes Tóth was not Tom's advisor. Tom's advisor was actually Langlands and until Kepler, Tom did representation theory.

Yes, essentially, it reduces to a manageable optimization problem.

slawekk said...

> HOL Light differs slightly from the Zermelo-Fraenkel-Choice axioms of set theory used in traditional mathematics.

Note that there are other proof assistants, like Mizar and Isabelle/ZF that implement ZF set theory, so it is possible to do formalized mathematics in the traditional setting as well.

Carson C. Chow said...

Absolutely, thanks for the comment.