Supporting the formal verification of mathematical texts

The formal verification of mathematical texts is one of the most interesting applications for computer systems. In fact, we argue that the expert language of mathematics is the natural choice for achieving efficient mathematician–machine interaction. Our empirical approach, the analysis of carefully authored textbook proofs, forces us to focus on the language and the reasoning pattern that mathematician use when presenting proofs to colleagues and students. Enabling a machine to understand and follow such language and argumentation is seen to be the key to usable and acceptable math assistant systems. In this paper, we first perform an analysis of three textbook proofs by hand; we then describe a computational framework that aims at mechanising such an analysis. The resulting proof-of-concept implementation is capable of processing simple textbook proofs and constitutes promising steps towards a natural mathematician–machine interface for proof development and verification.