TITLE: Lest We Forget the Mathematicians AUTHOR: Eugene Wallingford DATE: November 13, 2008 6:35 PM DESC: ----- BODY: Just before I left for the SECANT workshop, I wrote an entry on programming based on a conversation with a colleague in the math department. Then I went off to SECANT, which gave me a chance to think about the intersection of CS and science, which took my mind off of the role CS plays in mathematics. But the gods are reminding us: Computer science is changing how some mathematicians work, and not just via programming. The December 2008 issue of the Notices of the American Mathematical Society features four papers on the use of computers in mathematical proof, both to create new results and to ask and explore "new mathematical questions about the nature and technique of such proofs". This idea is known as formal proof. All four papers of the special issue are available as PDF files on the web site. (This is an excellent feature of Notices: the current issue is openly available to the community!). The lead article of the issue, by Thomas Hales, lays out the problem for which Formal Proof is the solution. In a nutshell: mathematicians verify their results by a social process, which means those results are fallible.
Traditional mathematical proofs are written in a way to make them easily understood by mathematicians. Routine logical steps are omitted. An enormous amount of context is assumed on the part of the reader.
Many of you probably already know that this is true, from your own negative experience. I know that I often felt as if I was missing a lot of context when I was reading proofs in the abstract algebra book we used in grad school! How are these proofs validated? By other mathematicians reading them and accepting them as valid. The best known and most important proofs have been read and understood by many mathematicians, so we can trust that they are probably correct. If there were something wrong with the result, someone would have found out by now -- either by by finding an error in the proof or by discovering that something else breaks when we rely on it. Programmers know that this is how most programs are "proven" correct: by using them reliably for a long time under many different conditions. One problem with this process is that some proofs are so long and so complicated that the number of people who can read and understand them is quite small. For the results that break the most new ground, even the best mathematicians have to learn a lot to understand the proof. These "proof assistants" may not have the time, energy, or attention span to validate a result well enough that we "know" it is correct. A formal proof is an attempt to bypass the social process of mathematicians reading a result, providing the necessary context, filling in the details, and approving the result by automating those steps:
A formal proof is a proof in which every logical inference has been checked all the way back to the fundamental axioms of mathematics. All the intermediate logical steps are supplied, without exception. No appeal is made to intuition, even if the translation from intuition to logic is routine.
A formal proof will be less intuitive to most human readers, especially the advanced ones, but it should be less susceptible to errors by relying on formal specification of the context and of all the intermediate steps. "Show your work!" Specifying all of the extra detail completely is something humans are not so good at. Many great mathematicians -- and programmers -- are great in some part because they are able to take improbable intuitive leaps onto new ground. But computers thrive on such tedious detail, so work on formal proof comes naturally to rest in the realm of programs that aid the process. Computerized "proof assistants" are nothing new. Hales cites examples going back to 1954 and the Johniac computer. I can't go that far back (my parents were still in grade school!), but I remember working with programs of this sort back in the mid- to late-1980s as a grad student in AI. Prof. Rich Hall, a philosophy professor specializing in epistemology and philosophy of mind, was a treasured member of my Ph.D. committee. For the philosophy component of my comprehensive, Hall asked me to study two such programs, Tarski's World and Computer Assisted Logic Lessons (CALL), intended as logic tutors and proof assistants for beginners. (Tarski's World is discussed here. CALL was a program home-brewed at Michigan State. I found one reference to it via Google, in an MSU prof's syllabus from 1998.) My task was to identify the fundamental distinctions between the two programs, especially with regard to their respective assumptions, and to evaluate their instructional utility. Remarkably, I still have the paper I wrote for my exam -- formatted in nroff! Formal proof sounds perfect: Let a program do the grunt work to validate even our most complex proofs. But formal proof offers up to problems... The first is that the human has to specify some of the initial detail for the program in some logical language. One thing that many years in AI taught me is that logic languages are just like programming languages, and writing proofs in them encounters all the same perils as writing a program. Writing proofs is the cross borne by mathematicians, though, and this problem is exactly the one formal proof seeks to solve (a recursive problem!): making sure that our proofs contain all the necessary detail, written and used correctly. The second problem is that now we have to consider whether the computer program itself is correct. To use the program to validate a proof, we need first to validate the program. This is a different recursion. Fortunately, we have some things on our side. One is scale, both relative to large programs and to the proofs we hope to construct. As Hales points out:
The computer code that implements the axioms and rules of inference is referred to as the kernel of the system. It takes fewer than 500 lines of computer code to implement the kernel of HOL Light [a particular computer proof assistant]. (By contrast, a Linux distribution contains approximately 283 million lines of computer code.)
The "kernel" of the system is small enough to be amenable to validation in several ways. One is the social process used for other programs: make the code open source and let everyone and his brother study it and use it. I love the way Hales embraces this approach:
I wish to see a poster of the lines of the kernel, to be taught in undergraduate courses, and published throughout the world, as the bedrock of mathematics. It is math commenced afresh as executable code.
(The emphasis is mine. More on that later.) This replaces the social process for validating proofs, up one level. Even if we validate the proof assistant only informally, it will be used repeatedly to validate proofs, and every use is an opportunity to find errors in the program. We can even use the program to validate proofs we already understand well just for the purpose of validating the program. (The world of mathematics is full of test data!) We use a social process to build a tool which then serves us over and over. Building tools is an essence of computer science. Given the small size of the program, we could also use formal methods to prove its correctness or at least offer evidence that it is correct. John Harrison used HOL Light to something akin to a formal proof of its own soundness. This is the first time in a long while that I have read about Gödel's incompleteness theorem coming into play with a real program... This approach made me think of the compiler-writing technique known as bootstrapping, though that's not quite what Harrison did. Finally, we might try to validate the program using another proof assistant. Hales calls this "exporting" a proof. The idea is this. Translate a proof written for one assistant into the language of another.
If a proof in one system is incorrect because of an underlying flaw in the theorem-proving program itself, then the export to a different system fails, and the underlying flaw is exposed.
For some reason, this reminded of cross-compilation, where we use a compiler on one platform to generate code for another platform. The purpose of cross compiling is to propagate programs onto systems where they do not exist yet. The purpose of exporting is different, to increase our confidence in one or both proof assistants. When we combine the confidence we have in the program via social acceptance with the confidence we gain from validating exported proofs, we have even more reason to trust the program, and thus the proofs it validates. Our confidence grows. This process reminds us all that math, while not a natural science, is imbued with the spirit of science:
With a computer -- indeed with any physical artifact, whether a codex, transistor, or a flash drive made of proteins from salt-marsh bacteria -- it is never a matter of achieving philosophical certainty. It is a scientific knowledge of the regularity of nature and human technology, akin to the scientific evidence that Planck's constant lies reliably within its experimental range. Technology can push the probability of a false certification ever closer to zero: 10-6, 10-9, 10-12, ....
We never know our proofs are correct. We only have good reason to believe so. The same is true of programs. That's another reason for a computer scientist like me to be fascinated by this direction in mathematics. The connection to the topic of the SECANT workshop is strong. Computing is helping to revolutionize how mathematicians work, just as it is revolutionizing how scientists work. Part of the math revolution will resemble the one in science, because some math research is itself inherently computational. The changes we talk about with formal proofs are a bit different, in that they are about how we validate results, not how we create them. Both traditional mathematics and computational mathematics depend ultimately on validation. Formal proof is aimed at addressing the former, but what of the latter? Certainly some scientists have recognized the problem and embarked on efforts to solve it. I wrote about one such effort early this year, a simulation-and-documentation system that interleaves programs, their execution, and the papers written to publish the results. Not surprisingly, such thinking and the systems that implement it require a change in mindset, one that will likely come only after a long... social process. Hales recognizes what the use of computing to generate and check proofs means for his discipline: It is math commenced afresh as executable code. I think many disciplines will find themselves redefined in just this way. -----