为 mathlib4 设计了一个语义搜索引擎，可以接收非正式查询并找到相应的定理，同时还建立了一个用于评估各个搜索引擎性能的基准。

Mar, 2024

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

Jun, 2024

该研究实现并运用了一些适当的标准去分析 HOL Light 和 Flyspeck 等正式数学库中的引理图，从而提高了自动化定理证明的效率和准确性。

Feb, 2014

通过提取来自 GitHub 的大规模形式数据集 LEAN-GitHub，经过对 InternLM-math-plus 的微调，模型在 Lean 4 miniF2F 测试中实现了 48.8% 的准确率，在一次通过中实现了 54.5% 的准确率，超过了 52% 的现有模型方法的最新成果，并在两个其他 Lean 4 基准测试（ProofNet 和 Putnam）中取得了最新成果，该数据集对于广泛的数学主题的形式推理是有益的。

Jul, 2024

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

Nov, 2022

我们提出了 Llemma 这个大型数学语言模型，通过将 Code Llama 进行预训练得到了 Llemma，并在 MATH 基准测试中表现优于所有已知的开源基础模型，同时还能进行工具使用和形式定理证明而无需进一步微调。

Oct, 2023

本文讨论了如何发展 21 世纪的全球数学图书馆，提出了利用机器学习和社区协作的方式，将全球数学文献中的信息和知识以链接开放数据的形式更好地提供给研究人员，以此建立数学信息的集成式系统。

Apr, 2014

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

Jun, 2023

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

Apr, 2024

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

Mar, 2024