Proof Presentation

The talk is based on a book about the human-oriented presentation of a mathematical proof in natural language, in a style as we may find it in a typical mathematical text book. How can a proof be other than human-oriented? What we have in mind is a deduction systems, which is implemented on a computer, that proves – with some human interaction – a mathematical textbook as may be used in an undergraduate course. The proofs generated by these systems today are far from being human-oriented and can in general only be read by an expert in the respective field: proofs between several hundred (for a common mathematical theorem), for more than a thousand steps (for an unusually difficult theorem) and more than ten thousand deduction steps (in a program verification task) are not uncommon. Although these proofs are provably correct, they are typically marred by many problems: to start with, that are usually written in a highly specialised logic such as the resolution calculus, in a matrix format, or even worse, they may be generated by a model checker. Moreover they record every logical step that may be necessary for the minute detail of some term transformation (such as, for example, the rearrangement of brackets) along side those arguments, a mathematician would call important steps or heureka-steps that capture the main idea of the proof. Only these would he be willing to communicate to his fellow mathematicians – provided they have a similar academic background and work in the same mathematical discipline. If not, i.e. if the proof was written say for an undergraduate textbook, the option of an important step may be viewed differently depending on the intended reader. Now, even if we were able to isolate the ten important steps – out of those hundreds of machine generated proof steps – there would still be the startling problem that they are usually written in the "wrong" order. A human reader might say: "they do not have a logical structure"; which is to say that of course they follow a logical pattern (as they are correctly generated by a machine), but, given the convention of the respective field and the way the trained mathematician in this field is used to communicate, they are somewhat strange and ill structured. And finally, there is the problem that proofs are purely formal and recorded in a predicate logic that is very far from the usual presentation that relies on a mixture of natural language arguments interspersed with some formalism. The book (about 800 page) which gives an answer to some of these problems is to appear with Elsevier