Automated `Plugging and Chugging'

Introduction

In [zeitz:taacops], Paul Zeitz discusses how to solve mathematical problems. One technique he proposes is to calculate some examples of objects in the problem statement and try to spot a pattern or property which provides insight into the nature of the problem. Zeitz suggests:

Plug in lots of numbers. Keep playing around until you see a pattern ... and try to figure out why the pattern you see is happening. It is a well kept secret that much high-level mathematical research is the result of low-tech ``plug and chug'' methods.

Theory Formation to Produce Suggestions

In number theory, starting with only a few background concepts such as multiplication, HR can form thousands of concepts such as prime numbers, etc. For the above problem we plugged and into the formula for the product of four consecutive integers: . The results from the calculation were: and . We then asked HR to form concepts in number theory and output the definition for any number type which the numbers and all satisfied. The first answer it produced was: even numbers, which didn't help with the problem.

After a few minutes, HR's 15th suggestion was that the above numbers are all squares minus one. This is the eureka step that Paul Zeitz was hoping the reader would make through the plug and chug technique. To finish the solution, the user must show that the product of 4 consecutive integers is always a square minus one, using some algebraic manipulation:

Finally, they must state that the distribution of the positive square numbers means that a square minus one is never a square, hence the product of four consecutive integers is never a square.

Conclusion

We have detailed one way in which calculation can be used to help deduction. One can imagine the initial calculations and algebraic manipulation being undertaken by a computer algebra system and the transformed conjecture being easier for an automated theorem prover to solve (although this is possibly not the case for the above example). However, the main application of this approach may not be to produce entire proofs of theorems, but to make intelligent suggestions to the user about tricky problems. Transforming the conjecture involved an inventive step whereby a new concept was introduced. We have shown how this can be done by a theory formation program such as HR, although other methods involving knowledge bases and/or machine learning techniques may be faster.

To conclude his discussion about the Hungarian problem, Zeitz says:

Getting to the conjecture was the crux move. At this point the problem metamorphosed into an exercise!

Acknowledgments

This work is supported by EPSRC grant GR/M98012.

References

[zeitz:taacops]
P. Zeitz.
The Art and Craft of Problem Solving.
John Wiley and Sons, 1999.

[colton:ijcai99]
S. Colton, A. Bundy, and T. Walsh.
HR: Automatic concept formation in pure mathematics.
In Proceedings of the 16th International Joint Conference on Artificial Intelligence, 1999.