Mathlib4的语义搜索引擎
该论文介绍了Thor，一个集成语言模型和自动定理证明器的框架，它采用一种称为“hammers”的方法来选择前提，从而增加了语言模型在PISA数据集上的成功率并解决了相当一部分问题，同时比现有最佳方法在MiniF2F数据集上具有更小的计算量。
May, 2022
本研究使用大型语言模型(Codex)探讨将使用自然语言书写的数学（即定义，定理陈述和证明）转化为可以被程序检查正确性的形式语言的能力，并发现对于120个定理，Codex可以在本科水平上以近75％的准确率进行短数学陈述的形式化。同时在选择合适的输入和后处理策略下，Codex可以以自然语言形式翻译本科水平的13个定理的证明，这些具有两到三自然段长度的证明可以在12次中有至少一次完成翻译，这表明大型语言模型是完全或部分自动化形式化的有前景的途径。
Nov, 2022
本文介绍了 LeanDojo：一个开源、可交互的证明环境，它从Lean中提取了证明中的数据及注释，提供了有价值的前提数据，以便于选取前提。 我们使用此数据，开发了 ReProver：第一个增加检索功能的基于LLM的证明程序。其成本低廉，只需要一台GPU进行一周的训练，并且可以有效地选择定理中的前提。我们构建了一个包含96962个定理和证明的新基准，并将其用于培训和评估。实验结果表明，相对于非检索基线和GPT-4，ReProver非常有效。我们发布了代码和数据集，以促进进一步的研究。
Jun, 2023
GPT-4的研究调查发现，尽管该模型可以重复、改编和润色其之前见过的数学证明，然而它并未实际理解基本数学概念，而在形式语言中证明数学定理的任务与搜索引擎如Google的方法相当，而预测句子中的下一个词可能是一种错误的方法，往往会导致过度推断和最终失败。
Nov, 2023
为了发现并判断几何定理的有趣性，本文针对自动发现几何定理和其性质的不同方法和度量进行讨论，并引入了一个不可判定性结果来证明判断定理生成程序是否能产生有趣定理是一个非确定性任务。此外，还强调了需要通过专家调查和相关度量和方法的研究明确定理生成程序和有趣几何定理之间的关系。
Jan, 2024
这篇论文通过 EvoGPT-f 回答了关于五种形式数学语言（Lean 3、Lean 4、Coq、HOL 4、HOL Light）和四种标记化方法（字符、词级、字节对编码和 StarCoder 标记器）之间的差异化机器学习能力的定量分析，为进一步开展社区间系统定量和定性比较研究奠定了基础。
Feb, 2024
人工智能在定理证明方面，尤其是在交互定理证明中，已经产生了许多基准和方法。本文介绍了BAIT，一个公正而简化的比较学习方法在交互定理证明中的框架，通过对多个基准的深入比较，展示了BAIT的能力。我们发现结构感知变换器表现特别好，改进了与原始问题集相关的技术。BAIT还允许我们评估基于交互环境构建的系统的端到端证明性能。通过简化机器学习算法在ITP上的实现和比较，我们预计BAIT将成为未来研究的跳板。
Mar, 2024
基于大规模合成数据，使用Lean 4 proof数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高LLMs中的定理证明能力的潜力。
May, 2024
使用Lean等计算机可验证形式语言来证明数学定理具有重大影响，本文提出了TheoremLlama框架，通过生成对齐的数据集和训练方法，使大型语言模型成为Lean4专家，实现了高于GPT-4基准的累积准确率。
Jul, 2024