本研究使用大型语言模型(Codex)探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于120个定理，Codex可以在本科水平上以近75％的准确率进行短数学陈述的形式化。同时在选择合适的输入和后处理策略下，Codex可以以自然语言形式翻译本科水平的13个定理的证明，这些具有两到三自然段长度的证明可以在12次中有至少一次完成翻译，这表明大型语言模型是完全或部分自动化形式化的有前景的途径。

Nov, 2022

本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从Lean中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。 我们使用此数据，开发了 ReProver：第一个增加检索功能的基于LLM的证明程序。其成本低廉，只需要一台GPU进行一周的训练，并且可以有效地选择定理中的前提。我们构建了一个包含96962个定理和证明的新基准，并将其用于培训和评估。实验结果表明，相对于非检索基线和GPT-4，ReProver非常有效。我们发布了代码和数据集，以促进进一步的研究。

Jun, 2023

DS-Prover是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在MiniF2F和ProofNet两个标准数据集上实现了显著的性能提升。

Dec, 2023

利用Lean框架，将复杂的逻辑推理问题形式化为定理后进行求解，以减少逻辑不一致性的风险并提升处理复杂推理任务的能力，取得了在FOLIO数据集上的最先进表现，并在ProofWriter上接近该水平的成果。值得注意的是，这些结果是在每个数据集的不到100个领域内样本进行微调实现的。

Mar, 2024

该研究论文介绍了使用大型语言模型作为辅助工具的 Lean Copilot 框架，用于证明定理过程中的自动化，证明步骤建议、自动完成中间证明目标、选择相关前提条件等。实验证明了该方法较现有的基于规则的证明自动化方法在证明定理过程中对人类的辅助和自动化程度的有效性。

Apr, 2024

基于大规模合成数据，使用Lean 4 proof数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高LLMs中的定理证明能力的潜力。

May, 2024

通过提出一种新的流程，我们利用合成数据来将自然语言数学问题转化为Lean 4语句，并相应地进行过滤，从而为解决LLMs在理解复杂数学问题和证明上的性能提供有用的训练数据。最终数据集包含约57K个正式-非正式问题对以及来自数学竞赛论坛的搜索证明和21个新的IMO问题。

Jun, 2024

使用Lean等计算机可验证形式语言来证明数学定理具有重大影响，本文提出了TheoremLlama框架，通过生成对齐的数据集和训练方法，使大型语言模型成为Lean4专家，实现了高于GPT-4基准的累积准确率。

Jul, 2024

传统基于语言模型的定理证明假设在足够数量的形式证明数据上训练后，模型将学会证明定理。研究观察到非形式证明中蕴含的丰富信息对于学习证明定理是有用的。因此，使用回顾性的真实策略生成合成思考来训练语言模型，Lean-STaR框架通过在每个证明步骤的预测策略之前直接生成思考来提升模型的证明定理能力，并通过专家迭代进一步微调模型。在Lean定理证明环境中，Lean-STaR在miniF2F-test基准上取得了最先进的结果，显著优于基准模型（$43.4% ightarrow 46.3%，$ Pass@64），同时对增强思考对定理证明过程的各个方面的影响进行了分析，提供了洞察力。

Jul, 2024

本文针对现有形式证明在可读性、简洁性等方面的优化问题提出了新的解决方案。通过引入ImProver这一基于大型语言模型的智能体，本文实现了对形式证明的自动化优化，使得优化后的证明在长度、模块化程度及可读性等指标上显著提升。研究结果表明，该方法在多种数学定理的优化中表现出色，具有广泛的应用潜力。

Oct, 2024