This article discusses existing and possible usages of deduction in education systems as well as challenges that have to be met in order to make certain deduction techniques effective for education. In particular, we will show how the ActiveMath system realises features that are essential for (mathematics) learning and suggest some main challenges.