arXiv:2502.03321v1 通知类型: cross 摘要：正式证明生成的挑战历史悠久，但随着现代技术的进步，我们可能终于处于解决实际数学问题的阶段。本文探讨了将ChatGPT与基本搜索技术结合以简化正式证明生成的方法，特别关注miniF2F数据集。我们展示了如何通过将类似于ChatGPT的大语言模型与形式语言Lean相结合，后者还具有可验证的优势，来提高正式证明生成的效率和可访问性。尽管非常简单，我们表现最好的基于Lean的模型在所有已知基准中的通过率达到了31.15%。我们将实验扩展到包括其他数据集，并使用了不同的语言模型，展示了我们的模型在不同环境中的可比性能，从而使我们能够对结果进行更细致的分析。我们的发现为AI辅助形式证明生成提供了见解，暗示了形式数学证明未来研究的一个有前景的方向。