Interactive Theorem Proving: Modelling the User in the Proof Process Bernhard Beckert and Sarah Grebing Proving complex problems requires user interaction during proof construction. A major prerequisite for user interaction is that the user is able to understand the proof state in order to guide the prover in finding a proof. Previous evaluations using focus groups for two interactive theorem provers have shown that there exists a gap between the user’s model of the proof and the actual proof performed by the provers’ strategies. In this paper, we sketch a process model of the interactive proof process that helps to analyze this gap. Additionally, we give insight into the results of a usability test of the interactive verification System KeY, which provides evidence that this model is consistent with the actual proof process.