We have that automation is possible even while producing an explicit proof, but how much do we actually want? Despite some tours de force by automated theorem provers, the emphasis in applications is moving increasingly towards interactive systems, where the user guides the prover. In mathematics this seems reasonable, since the proofs are important, and we don't usually want an ex cathedra assertion that something is true from a machine. On the other hand, we also don't want to have to direct proofs at very low levels, so some automation of 'obvious' steps is required.

As pointed out by John McCarthy, there is an important distinction between what is mathematically obvious and what is logically obvious. In mathematical proofs we want to skip over levels of reasoning which we can intuitively see to be trifling; but this intuition may be based on quite sophisticated domain-specific knowledge, and the step may not be at all obvious in the sense of having a formal proof which is easy to find using one of the common techniques for automated proof search. An interesting discussion of just what is logically obvious is given by [rudnicki-obvious]. It seems that we need more work on automating what is mathematically obvious, whereas existing technology may already be capable of automating much larger logical steps than we can perceive as obvious, e.g. very large tautologies or even subtle predicate calculus reasoning like the following theorem due to \los:

(x y z. P(x,y) P(y,z) P(x,z))
(x y z. Q(x,y) Q(y,z) Q(x,z))
(x y. Q(x,y) Q(y,x))
(x y. P(x,y) Q(x,y))
(x y. P(x,y)) (x y. Q(x,y))

However, there are certain steps which are completely routine for a machine to check, and baffling to a human being, which we probably do want to automate, simply because carrying out the proof in detail is no more illuminating to the human than knowing, based on confidence in the correctness of the theorem prover, that it is valid. A good example is the following identity:

(x² + y² + z² + w²) (x'² + y'² + z'² + w'²) =
(x x' + y y' + z z' + w w')² +
(x y' - y x' + w z' - z w')² +
(x z' - z x' + y w' - w y')² +
(x w' - w x' + z y' - y z')²

It's used as a lemma in the proof that every integer is expressible as the sum of four squares. But proving it, at least simply by multiplying it out in a routine way, is no more illuminating than checking the result of a numerical calculation by hand. Of course a proof which exhibited a deep, simple reason for the above (e.g. something based on quaternions) is a different matter.

In any case, automating what is mathematically obvious is itself a research project in the artificial intelligence line. In the short term, it's probably better to accept a lower level of automation. As theorem-proving technology improves, it should be possible to simplify proofs automatically by excising intermediate steps which are now unnecessary for the machine. There is the important lesson that the theorem prover must admit extension with domain-specific reasoning without compromising soundness. We believe that this problem has already been solved by LCF-style systems.

John Harrison 96/2/22; HTML by 96/4/5