I think the two things that you mentioned, `examples of an idea in action' and `general ideas about how to use an idea' are closely related. It is necessary to have a classification of ideas for efficient mathematics. An easily accessible, well linked, explained, expandable and searchable list of distinct and nontrivial manifestations of an idea will facilitate the tasks of understanding the idea and coming up with how one can make use of it at a particular problem at hand (either by analogy with an earlier example or perhaps, and luckily, inventing a new way to use the idea).

It is shocking to me that a classification of mathematical ideas is lacking in our time and this is one of the reasons I am very excited about tricki. For example, when we read a book, it must be a simple task to answer the questions: `What are the algorithms, ideas used in this book?' `What is new in terms of ideas?' Unfortunately our mathematical writing is not at a stage where this is particularly simple. I think and hope that tricki is a great step in that direction.

I think these are also related with your ideas on automated proofs.

What are general ideas about how to find good substitutions? I think two important advice are these: look at the change of variables that appeared in problems similar to yours and to look carefully at this aspect of problem formulation as it will determine how we will think about the problem. Other than these, I can think of area and structure dependent ideas. For example, in probability theory, one idea must be to look for a formulation of the problem where the underlying distribution is a product measure or Markovian: i.e., to see if there is a way to write the problem where various variables/processes are natural functions of independent random variables or Markov processes.