An Interactive Proof Development Environment + Anticipation = A Mathematical Assistant?

Current semi-automated theorem provers are often advertised as “mathematical assistant systems”. However, these tools behave too passively and in a stereotypic way to meet this ambitious goal because they lack the capability to adequately take into account requirements on proof search control and user demands for their own actions. Motivated by this deficit, we have incorporated several facilities into the MEGA proof development system that anticipate a number of divergent factors, based on mathematical knowledge, proof search defaults, and expectations about users. The techniques enhance the system’s functionality through proof planning by knowledge-intensive methods, proof search guidance by default suggesting agents, and proof presentation by redundancy avoidance measures. The system’s behavior suggests that anticipation is without doubt a central driving force in a mathematical assistant.