Proof Presentation

Abstract

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