FOM: Are machines better in math?

[Roger Bishop Jones]

On Wednesday 20 February 2002  7:36 pm, Gordon Fisher wrote:
> charles silver wrote:
> >     I previously posted the question whether chess is as interesting
> > as mathematics, intending to stimulate discussion on the role of
> > mathematical insight in obtaining results.   However, immediately
> > after posting the earlier question, I happened to stumble upon
> > a short account documenting the success of theorem provers in
> > "discovering" new theorems.
> > *****************************************
>
> It has been a while since I made a short foray into automated
> theorem proving, but my recollection is that I concluded that
> one had to be very careful to build into programs for
> proving theorems some carefully chosen ingredients of
> the proofs one expected to get.  Can anyone challenge me
> on this cynical opinion?

>From my limited familiarity with the work at Argonne I make the
following two observations.

Firstly I think it is incorrect to describe this as 
	the success of theorem provers in "discovering" new theorems.
(which Charles does but the document he cites does not.)

I think the most relevant Argonne work is with the Otter resolution theorem
prover which does proof by reductio absurdum.
This can find proofs of interesting and previously unproven mathematical
results, but the discovery is of the proof, not of the result.
I don't think there is any problem in getting similar technology to "discover"
new theorems, but some difficulty in selecting what is "interesting" without
human intervention.

Secondly, as to the alleged need:

> to be very careful to build into programs for
> proving theorems some carefully chosen ingredients of
> the proofs one expected to get.  

This doesn't sound to me like a reasonable comment on the capabilities
of Otter, but its to vague to be susceptible of refutation.
Of course, one does have to be very careful in chosing the ingredients
of proofs, insofar as all the allowable ingredients must be sound inferences,
but presumably that was not what was meant.

Roger Jones