Abstract:

Assisted Proof Document Authoring

David Aspinall and Christoph Lüth and Burkhart Wolff


Significant advances have been made in formalised mathematical texts for large, demanding proofs. But although
such large developments are possible, they still take an inordinate amount of effort and there is a significant gap 
between the resulting formalised machinecheckable proof scripts and the corresponding human-readable 
mathematical texts. We present an authoring system for formal proof which addresses these concerns. It is based
 on a central document format which, in the tradition of literate programming, allows one to extract either a formal 
proof script or a human-readable document; the two may have differing structure and detail levels, but are 
developed together in a synchronised way. Additionally, we introduce ways to assist production of the central 
document, by allowing tools to contribute backflow to update and extend it. Our authoring system builds on the 
new PG Kit architecture for Proof General, bringing the extra advantage that it works in a uniform interface, 
generically across various interactive theorem provers.