Focus Windows: A New Technique for Proof Presentation Bruno Buchberger Proceedings of the Rhine Workshop on Computer Algebra, Mannheim, March 15, 41 pages. ABSTRACT: We first summarize our view of symbolic computation as a magma of provers, solvers, and simplifiers (computers) w.r.t. various mathematical theories. Then we concentrate on the technical and didactic aspect of presenting proofs generated by (automated) provers in a form suitable for the check by human readers. For this, we describe the technique of focus windows which we introduced in 2000 and which was recently implemented in our Theorema system by Florina Piroi. By the focus window technique, in each step of a proof, the reader obtains window that contains exactly those formulae that are relevent in this step. In more, detail, in each step we first display an "attention window" that displays the current proof goal and all the relevant formulae from the knowledge base that are used in this proof step and, then, we display a "transformation window" that, in addition, shows the new formulae generated in this step. We illustrate the focus window technique by displaying a proof on equivalence relations and partitions generated by the Theorema set theory prover both in the ordinary linear representation and in the focus windows representation. We conclude by sketching future improvements on the focus windows technique and some theoretical implications.