Towards an Intelligent Tutor for Mathematical Proofs

TL;DR

This paper presents a novel intelligent tutoring system for teaching mathematical proofs, leveraging an adapted proof assistant and dialog analysis to provide personalized, effective instruction in textbook-style proof learning.

Contribution

It introduces a new approach to developing an ITS for mathematical proofs by integrating assertion-level proof strategies and dialog analysis based on real tutorial data.

Findings

Prototype successfully evaluated on tutorial dialogs

Yields good instructional results

Reuses proof representations and search strategies

Abstract

Computer-supported learning is an increasingly important form of study since it allows for independent learning and individualized instruction. In this paper, we discuss a novel approach to developing an intelligent tutoring system for teaching textbook-style mathematical proofs. We characterize the particularities of the domain and discuss common ITS design models. Our approach is motivated by phenomena found in a corpus of tutorial dialogs that were collected in a Wizard-of-Oz experiment. We show how an intelligent tutor for textbook-style mathematical proofs can be built on top of an adapted assertion-level proof assistant by reusing representations and proof search strategies originally developed for automated and interactive theorem proving. The resulting prototype was successfully evaluated on a corpus of tutorial dialogs and yields good results.