Teaching problem-solving in formal domains aims at two purposes: 1) increasing the students' skill in addressing the problem in a goal-oriented way, and 2) increasing their competence in expressing themselves formally. In a dialog, suitable tutoring strategies addressing both issues may be quite delicate, especially when meeting formally inaccurate or even faulty statements which nevertheless are useful from the problem-solving perspective. Based on evidence from Wizard-of-Oz studies on human tutoring in mathematical theorem proving, we have developed a model for addressing formally inaccurate statements within a problem-solving context. Based on an error recognition and correction module, the model performs a conceptually-motivated error categorization and generates a suitable response.