In a corpus of student/tutor dialogues on mathematical proofs, tutors
use their evaluations of the correctness of proof steps in order to
generate pedagogically suitable feedback. This motivates the need for
support from a reasoning module for verification of proof steps in
mathematics tutorial dialogue systems. In such a system the support
from the mathematical domain reasoner is combined with the benefits of
natural language interaction with a simulated tutor.

In this talk I will present two important steps towards realising such
a system. First, I present a domain-independent method for
automatically verifying correct proof steps and detecting standard
reasoning errors which utilises general-purpose mathematical
knowledge. Second, I show how a dialogue manager can interface with
the domain reasoner. The dialogue manager can thus provide a single
representation of information, like the linguistic and mathematical
interpretation of the previous proof step, which is needed to
instantiate tutor actions such as hints.