Assisted Proof Document Authoring

Recently, 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 eort and time, and there is a significant gap between the resulting formalised machine-checkable 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 for- mat 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 diering 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 architec- ture for Proof General, bringing the extra advantage that it works in a uniform interface, generically across various interactive theorem provers.