Syntax-directed discovery in mathematics

It is shown how mathematical discoveries such as De Moivre's theorem can result from patterns among the symbols of existing formulae and that significant mathematical analogies are often syntactic rather than semantic, for the good reason that mathematical proofs are always syntactic, in the sense of employing only formal operations on symbols. This radically extends the Lakatos approach to mathematical discovery by allowing proof-directed concepts to generate new theorems from scratch instead of just as evolutionary modifications to some existing theorem. The emphasis upon syntax and proof permits discoveries to go beyond the limits of any prevailing semantics. It also helps explain the shortcomings of inductive AI systems of mathematics learning such as Lenat's AM, in which proof has played no part in the formation of concepts and conjectures.