Defining the Mapping
Observed regularity in human texts between type of formal reasoning and form of sentence produced
Use regularity to define Mathematical Communication Conventions (MCCs) that indicate the communication information necessary at each proof node
- Each MCC represents a type of high-level formal proof step.
- Each MCC specifies what proof information from the node should be used.
- Each MCC is uttered in a regular manner.