Automation of Diagrammatic Proofs in Mathematics

Introduction

1 + 3 + 5 + · · · + (2n- 1) = n 2

It requires only basic secondary school knowledge of mathematics to realise that the diagram above is a proof of a theorem about the sum of odd naturals.

It is an interesting property of diagrams that allows us to "see" and understand so much by looking at a simple diagram. Not only do we know what theorem the dia­ gram represents, but we also understand the proof of the theorem and believe it is correct. Is it possible to simulate and formalise this sort of diagrammatic reason­ ing on machines? Or is it a kind of intuitive reasoning peculiar to humans that mere machines are incapable of? Roger Penrose claims that it is not possible to automate such diagrammatic proofs . 1 We are taking his position as an inspiration and are trying to capture the kind of diagrammatic reasoning that Penrose is talking about in order to be able to simulate it on a computer.

Theorems in automated theorem proving are usually proved by logical formal proofs which often do not con­ vey an intuitive notion of truthfulness to humans. The inference steps are just statements that follow the rules of some logic. The reason we trust that they are cor­ rect is that the logic has been previously proved to be sound. Following and applying the rules of such a logic guarantees us that there is no mistake in the proof.

However, there is a subset of problems which humans can prove in a different way by the use of geometric oper­ ations on diagrams, so called diagrammatic proofs (such as the one given above). Insight is more clearly perceived in these than in the corresponding algebraic proofs: they capture an intuitive notion of truthfulness that humans find easy to see and understand. We are identifying and automating this diagrammatic reasoning on math-

1 Roger Penrose presented his position in the lecture at International Centre for Mathematical Sciences in Edinburgh on 8 November, 1995.