Proof planning is an application of AI-planning in mathematical domains. As opposed to planning for domains such as blocks world or transportation, the domain knowledge for mathemat- ical domains is difficult to extract. Hence proof planning requires clever knowledge engineering and representation of the domain knowledge. We think that on the one hand, the resulting domain definitions that include operators, supermethods, control-rules, and constraint solver are interesting in itself. On the other hand, they can provide ideas for modeling other realistic domains and for means of search reduction in planning. Therefore, we present proof planning and an exemplary domain used for planning proofs of so-called limit theorems that lead to proofs that were beyond the capabilities of other current proof planners and theorem provers.