arXiv:2502.03321v3 通知类型: 替换-交叉 摘要：形式证明生成的挑战具有丰富的历史背景，但借助现代技术，我们可能终于处于能够解决现实生活中的数学问题的实际进展阶段。本文探讨了将ChatGPT与基本的搜索技术相结合以简化形式证明生成的方法，并特别关注miniF2F数据集。我们展示了将一个大型语言模型（如ChatGPT）与形式语言（如可验证的Lean）相结合如何提高形式证明生成的效率和可访问性。尽管方法简单，但我们基于Lean的最佳性能模型超过了所有已知基准，通过率达到31.15%。我们将实验扩展到其他数据集，并使用不同的语言模型，展示了我们的模型在不同环境下的性能相似性，并允许对我们的结果进行更详细的分析。我们的发现为AI辅助形式证明生成提供了见解，表明了未来形式数学证明研究的一个有前景的方向。