Lemmas can provide valuable help for constructing a proof, by providing intermediate steps. However, not all the formulae supplied to an ATP system as lemmas are necessarily helpful. It is therefore necessary to develop lemma management techniques that use the right lemmas at the right time, to improve the problem-solving ability of ATP systems. This paper presents three lemma management techniques, reports on their implementation, and illustrates their potential with example problems.