A model of an analogy between mathematical proofs

A model of an analogy between proofs is built on the basis of an extendable model of mathematical practice. A source proof is generalized by replacing some its parts with global syntactic variables. The target proof is obtained from the generalization as the result of applying a syntactic substitution instead of global syntactic variables. The tasks of analogy discovery, of building a target proof by analogy, of lemmas generation, which are necessary for building a target proof by analogy as well as for the generation of theorems analogous to a source one, consist in searching such syntactic substitution.