On the shape of mathematical arguments (Q1188723)

The book deals with ``human'' theorem proving, and not with mechanical verification or mechanical theorem proving. The author does not address psychological questions like: ``How do people find solutions``; she addresses more technical questions like: ``How can proof design be guided by syntactic analysis of the demonstrandum''. The book consists of two parts. The first one contains a mosaic of expositional essays, each of them dealing with one particular theorem; their proofs are used to illustrate what formalism is suitable to represent them in a form acceptable for computer scientists. Several technical criterions by which one argument can be objectively less streamlined than another are presented. Among the topics explored are proofs by cases, exploitation of symmetry, the problem of what to name, the exploitation of equivalence, proofs by calculation and their influence on the choice of notations, the degree of detail of proofs, and linearization of proofs. The second part consists of several more general chapters dealing in a more general setting with naming, clarity of exposition and notations. Although the book is written as the ``explanation-by-examples'' it may be of interest for computer scientists dealing with program verification or mechanical theorem proving.