  The application of contemporary artificial intelligence techniques to address
geometric problems and automated deductive proof has always been a grand
challenge to the interdiscipline field of mathematics and artificial
Intelligence. This is the fourth article in a series of our works, in our
previous work, we established of a geometric formalized system known as
FormalGeo. Moreover we annotated approximately 7000 geometric problems, forming
the FormalGeo7k dataset. Despite the FGPS (Formal Geometry Problem Solver) can
achieve interpretable algebraic equation solving and human-like deductive
reasoning, it often experiences timeouts due to the complexity of the search
strategy. In this paper, we introduced FGeo-TP (Theorem Predictor), which
utilizes the language model to predict theorem sequences for solving geometry
problems. We compared the effectiveness of various Transformer architectures,
such as BART or T5, in theorem prediction, implementing pruning in the search
process of FGPS, thereby improving its performance in solving geometry
problems. Our results demonstrate a significant increase in the problem-solving
rate of the language model-enhanced FGeo-TP on the FormalGeo7k dataset, rising
from 39.7% to 80.86%. Furthermore, FGeo-TP exhibits notable reductions in
solving time and search steps across problems of varying difficulty levels.
