Towards a Science of Interactive Proof Reading

Proof assistants such as Coq are powerful tools for formally verifying the correctness of software. We are interested in the process of reading the proofs produced in this mechanized context, with a goal of building tools to reduce sources of friction and misunderstanding. In this paper, we summarize the early steps we have taken to explore the design space for proof reading support, the results of a pilot study to better understand the proof reading process, and our future plans for this ongoing research.