arXiv:2502.03321v2 Announce Type: replace-cross 摘要：形式证明生成的挑战有着丰富的历史，但借助现代技术，我们可能终于到达了在实际数学问题上取得真正进展的阶段。本文探讨了将ChatGPT与基本的搜索技术集成以简化形式证明生成的方法，并特别关注miniF2F数据集。我们展示了将大型语言模型ChatGPT与形式语言Lean（其优点是可以验证）结合使用如何提高形式证明生成的效率和可访问性。尽管非常简单，我们最好的基于Lean的模型在所有已知基准测试中的通过率为31.15%，超过了所有已知基准。我们扩展了实验以包括其他数据集，并使用了其他语言模型，展示了我们的模型在不同环境中的可比性能，从而为我们结果的更细致分析提供了依据。我们的发现为AI辅助形式证明生成提供了见解，表明了形式数学证明未来研究的一个有前景的方向。