Recent advancements in the application of Large Language Models (LLMs) to formal theorem proving in Lean have unveiled new prospects in complex logical reasoning scenarios. Acknowledging that the difficulty across reasoning steps in a formal theorem proof is not uniform, prior proof search algorithms have not systematically investigated which proof steps are more crucial to explore. This paper introduces Entropy-Based Best-First Search (EBFS), an entropy-inspired heuristic tree search algorithm that enhances the efficiency of proof generation models to explore proof trees, thereby increasing the probability of finding the correct proof. We also introduce a reinforcement fine-tuning approach specifically for proof tree search. Using EBFS during the generation stage further boosts the model’s performance in proof generation. Evaluations demonstrate that our fine-tuned EBFS model achieves consistent improvements over the baseline models. Under the same sample budget, it outperforms whole proof generation by 3.2% on the ProofNet testset, with further gains of 1.9% on MiniF2F and 1.5% on ProverBench.