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

The e ective use of automated theorem provers is frequently augmented by embedding these systems into interactive proof development environments. However, in order to act as a competent mathematical assistant, which is the ambitious goal behind these interactive extensions of automated provers, these tools behave too passively and in a stereotypic way, 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 de cit, 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, but this concept must be interpreted in meaningful ways for a variety of techniques, and its manifestations need to be elaborated in greater detail