Any work on Automated theorem proving by Pattern Recognition? Are there some mathematicians or papers about Advanced ATP by Pattern recognition? 
Pattern recognition: recognize the patter from mathematic sentence, proof sequence.
 A: The question is a bit vague. There are multiple types of automated theorem proving, from basic electronic adders as gate arrays (arithmetic is proving a theorem about concrete objects in finite groups) to higher order logic. The areas that often receive the most attention are first order resolution, because its semidecidable and can encompass most of mathematics with axiomatic set theory and SAT, because its fully decidable and so closely related to the P vs NP problem.
SAT and first order resolution are closely related in that they attempt to prove theorems by doing search in similar ways. These search for satisfiability of a statement, or the existence of a contradiction. Pattern matching is a required part of the resolution algorithm, as you need to recognize if two sentences match, but I suspect that's not quite what you meant. 
More advanced techniques for automated theorem proving seek to look at 'proof sketches' of previous lemmas and theorems proved to prune the search tree when adding lemmas to a set of support, and this is something that Prover9 supports. It's probably closest to the spirit of your question about pattern recognition, in that it looks at other proofs and attempts to follow similar chains of reasoning based on other successful theorems.
http://www.cs.unm.edu/~mccune/prover9/manual/2009-02A/hints.html
