本文提出了HybridProver，一种结合战术生成与整体证明合成的双模型证明框架，旨在解决形式化方法在关键系统可靠性验证中的应用障碍。实验结果显示，其在miniF2F数据集上的成功率达到59.4%，超越了之前的记录，为定理证明的自动化提供了新的视角。