My principal line of research is the study of the integration of XML-based Mathematical Knowledge Management technologies with Interactive Theorem Proving.