An internal model of mathematical practice for interactive systems of theorem proof construction. Part 3. A proof model

The paper completes the series of 3 articles describing the model of mathematical practice for an automated theorem proving system. Reasoning rules used in proof construction are formulated. A model of a complete proof is determined. The examples of mathematical statements in MMD language – a formal model of a mathematical dialect – and a model of correct complete proof for one of them are presented.