A Proof Presentation Suitable for Teaching Proofs

. The paper addresses comprehensible proof presentation for teaching and learning that can be provided by an automated proof planner that is a component of the proof development environment\Omega mega. Starting from empirically discovered requirements for the comprehensibility of proofs we show that, given a proof plan representation of a proof, the problem of automatically presenting a mathematical proof in a comprehensible manner becomes feasible in a way that was impossible before. We show how, based on a proof plan, a structured presentation at the level of proof methods can be automatically constructed 1 Introduction Computer algebra systems have been successfully used in teaching mathematics (see, e.g. a summary of Dana Scott's courses [12]). Can automated theorem proving systems be useful for teaching mathematical proofs? and under which conditions? The traditional automated theorem provers' output is at best a presentation of steps representing logic calculus rules. 1 Ther..