Abstract. State-of-the-art proof presentation systems suffer from several deficiencies. First, they simply present the proofs without motivating why the proof is done as it is done. Second, they neglect the issue of user modeling and thus forgo the ability to adapt the presentation to the specific user. Finally, they do not allow the user to interact with the system to ask questions about the proof. As a first step to overcome these deficiencies, we developed a computational model of user-adaptive proof explanation, which is implemented in a generic, user-adaptive proof explanation system, called P.rex (for proof explainer). To do so, we used techniques from three different fields, namely from computational logic to represent proofs ensuring the correctness; from cognitive science to model the users mathematical knowledge and skills; and from natural language processing to plan the explanation of the proofs and to react to the user’s interactions.