Computer Mathematics

I am rather swamped with things to do at the moment, so my computability logic escapades have been put on halt. This recent upswing in the number of things to do has led me to wish that my computer could do some of them for me. Perhaps the hard bits such as, oh I don't know, proving my theorems. Yeah. That would be grand.

There are two possible routes to follow when getting computers to attack theorems. On the one hand, we can ask that the computer does everything on its own. We just give it the statement of the theorem and away it churns creating a proof. Most succesful theorem provers of this kind more or less use souped up versions of resolution. The most prominent example is OTTER, which handles first order logic with equality.

What's resolution? Say you have a clause C that contains some literal x and another clause D which contains the negation ~x. Then, the resolution rule says to pass to the union of C\{x} and D\{~x}. A resolution refutation is one which consists of a sequence of applications of the resolution rule and ends in the empty clause. As such, it is a negative procedure: feed in the negation of your statement. If your statement is a theorem then the negation is not satisfiable and resolution will be able to pick up on this.

As you might suspect, just using resolution is not a particularly good way of deriving theorems that mathematicians are actually interested in. Moreover, doing things only in first order logic vastly limits what you can even express to begin with. So, not much analysis can be done, for example.

The other approach is to have some amount of user interaction. The most prominent approach to this style of theorem proving is dubbed the "LCF philosophy". LCF stands for the Logic of Computable Functions, which was introduced by Dana Scott around 1970. LCF is also the name of a theorem prover, originally developed in Lisp at Edinburgh. Its philosophy is to have a trusted kernel of procedures that are "trusted" to be correct. Typically, these would be some set of rules characterising higher order logic or some sort of typed lambda calculus. Everything else in the system is built on top of this kernel and compiled down to functions that only use the kernel rules. Much like how a modern operating system is built. While LCF itself is no longer around, many famous modern interactive theorem provers are directly descendent from it, for example Isabelle and HOL4. Incidentelly, the language ML was designed and built specifically for the task of interactive theorem proving which led inter alia to the first incarnation of Isabelle. LCF-style theorem proving has shown up recently on mathematical radars with Georges Gonthier's recent verification of the proof of the Four Colour Theorem:

A Computer Checked Proof of the Four Colour Theorem; Georges Gonthier

Alas, interactive theorem provers do not free me from doing any work. Quite the opposite in fact. This is because, in order to give a fully verified proof of a theorem in an intereactive prover, one must grapple with the "gap problem". What's that? In almost any nontrivial proof, there are statements to the effect of "it is trivial to see that...", "The reader may verify that,...", "the other 1,987,456 cases go through without essential changes" etc. Now, you can't just say that to a computer. You have to fill in all of the gaps! It would be nice if these systems were able to automatically fill in the gaps but, alas, they can't. Oh dear. At any rate, for a light overview of the sorts of problems involved and stuff that has been done, look no further than:

The Challenge of Computer Mathematics; Henk Barendregt and Freek Wiedijk