Also, in this process of mathematical theory exploration, storage and retrieval of knowledge plays an important role. The way how one proceeds in building up a mathematical theory in successive, well structured, layers has significant influence on the ease of proving individual propositions that occur in the buildup of the theory and also on the readability and explanatory power of the proofs generated. Furthermore, in the practice of mathematical theory exploration, different reasoning methods are used for different theories and, in fact, reasoning methods are expanded and changed in the process of exploring theories, whereas traditional automated reasoning systems try to get along with one reasoning method for large parts or all of mathematics. We describe a methodology for the algorithmic support of mathematical theory exploration. Starting from any mathematical knowledge base (collection of formulae that may be axioms, definitions, propositions, lemmas, theorems, problem specifications, algorithms), in one exploration round, we introduce a few new notions by axioms or definitions and then explore the possible interactions of these notions with all existing notions as completely as possible before we proceed to the introduction of the next notions. Achieving a certain degree of completeness in the current exploration round is crucial for decreasing the complexity of proving in the subsequent exploration rounds. The invention of axioms and definitions, the invention of propositions that describe interactions between notions, the invention of problems involving the new notions, and the invention of algorithms that solve these problems is something which, typically, needs a certain degree of human intervention. However, we show that significant algorithmic support for these invention steps is possible by the use of {\em formula schemes}. Formula schemes are formulae with higher order variables for functions and predicates that describe fundamental properties of functions and predicates, as for example commutativity, isomorphy, etc., that have proved to be useful in the practice of mathematics. The application of formula schemes provides a kind of bottomup support in the exploration of mathematical theories. A second idea is orthogonal to the use of formula schemes and provides topdown support in the exploration: We provide tools for the analysis of failing proofs. Failing proofs contain a lot of creative information. They give us hints about missing links in the systematic exploration of notions. For example, a failing induction proof of a conjecture may give us a hint about which lemmas we should try to prove before going back to the proof of the conjecture. The extraction of intermediate lemmas from failing proofs can, however, also be applied for the synthesis of algorithms. We illustrate the interplay between the use of formula schemes, lemma extraction from failing proofs and automated reasoning (special reasoners for special theories) in a couple of examples. Our main example is the theory of Groebner bases that has found numerous applications in many different areas of mathematics (algebraic geometry, symbolic analysis, algebraic combinatorics etc.). Particular emphasis is put on a new method for the algorithmsupported synthesis of algorithms, which we call lazy thinking method, that combines the use of formula schemes and the extraction of conjectures from failing (automated) proofs in a specific way: Our algorithm synthesis method is strong enough, for example, to automatically synthesize an algorithm for the construction of Groebner bases. This is surprising because the construction of Groebner bases is a completely nontrivial problem which  in the early days of computer algebra  was even conjectured to be algorithmically unsolvable. We also give some remarks, again in the example of Groebner bases theory, on the use of special theorem provers and the expansion and change of provers during the process of mathematical theory exploration and the implications of these facts on future reasoning systems for mathematics. All the examples are given in our Theorema system, which tries to implement the above approach to mathematical theory exploration.
