学习证明三角恒等式
利用深度学习技术来辅助自动的定理证明，通过对Mizar库的证明进行数据训练和选择处理，改进ATP的证明搜索引导，从而大幅度减少证明搜索的步骤和提高定理的证明率。
Jan, 2017
为了解决自动定理证明中有限的人工编写定理和证明的问题，我们提出了一种学习神经生成器自动生成定理和证明来训练定理证明器的方法，并通过实验验证，证明该方法的合理性，并成功推动了Metamath自动定理证明的发展。
Feb, 2020
本文探讨了基于Transformer的语言模型在自动定理证明中的应用，提出了基于语言模型的生成能够解决自动定理证明器与人类相比的主要限制之一——原始数学术语的生成问题。我们提出了一个自动证明器和证明辅助工具GPT-f，使用Metamath形式语言，并分析了其性能。 GPT-f发现了新的简短证明，并被采纳为正式数学社区所接受，这是我们所知道的第一次基于深度学习的系统为正式数学社区做出的贡献。
Sep, 2020
我们提出了TRIGO，一个自动定理证明基准测试，要求模型能够逐步证明简化三角表达式，并评估生成型语言模型在公式推理、数字项操作、分组和因式分解方面的推理能力。我们从互联网收集三角表达式及其简化形式，并用``Lean''形式语言系统注释简化过程，然后自动从标注样本中生成额外的示例来扩充数据集。通过基于Lean-Gym的自动生成器创建不同难度和分布的数据集来全面分析模型的泛化能力。我们的广泛实验显示，TRIGO对于包括在大量开源形式定理证明语言数据上预训练的GPT-4在内的先进生成型语言模型提出了新的挑战，并为研究生成型语言模型在形式和数学推理上的能力提供了新工具。
Oct, 2023
DS-Prover是一个用于定理证明的创新动态抽样方法，通过根据剩余时间和总分配时间来调整探索和开发之间的平衡，以提高证明搜索过程的效率，并通过拆分简化和重写策略为具有单个前提的策略来扩充训练数据集，从而在MiniF2F和ProofNet两个标准数据集上实现了显著的性能提升。
Dec, 2023
该论文提供了一项深度学习在定理证明中的全面调研，包括现有方法的综述、数据集和策略的详细总结、评估指标和最先进技术的性能分析，以及未来研究的挑战和发展方向的批判性讨论。该调研旨在成为深度学习在定理证明中的基础参考，促进这个迅速发展领域的进一步研究。
Apr, 2024
基于大规模合成数据，使用Lean 4 proof数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高LLMs中的定理证明能力的潜力。
May, 2024