本论文提出了基于机器学习的前提选择方法，通过构建依赖关系知识库并提出核方法的前提选择算法，在大型数学理论证明中实现了50％的性能提升。

Aug, 2011

该论文介绍了自动推理的Mizar（MizAR）服务，该服务将多种自动推理，人工智能和表现工具与Mizar及其编写环境集成在一起。服务基于Mizar语言到一阶ATP系统语言的良好转换，并依赖于在包含数万个可用事实的大型理论应用ATP系统的最新进展。

Sep, 2011

该论文结合Flyspeck项目中的数学知识与机器学习方法，提出一种能够自动回答数学问题的人工智能系统，并在评估中表现出较高的效率。该系统的实现涉及到HOL Light逻辑的转换以及机器学习的选择和集成。

Nov, 2012

HOL(y)Hammer 是一个基于HOL Light编码的在线人工智能/自动定理证明(ATP)服务，提供自动处理基于HOL Light的任意正式开发项目和攻击上传项目的任意猜想的功能。

Sep, 2013

本文初步探讨了在ACL2系统上使用外部ATP进行实验的情况，旨在为解决ACL2问题提供外部推理和人工智能系统的初步效用评估。

Jun, 2014

利用深度学习技术来辅助自动的定理证明，通过对Mizar库的证明进行数据训练和选择处理，改进ATP的证明搜索引导，从而大幅度减少证明搜索的步骤和提高定理的证明率。

Jan, 2017

我们发展出了一种AI/TP系统，通过使用基于学习的前提选择方法和增量训练方法，可以自动验证大量Mizar定理，证明效率高达60％和75％。

Mar, 2023

MLFMF 是一个数据集合，用于评估用于支持证明助手形式化数学的推荐系统的性能，数据集包含了来自 Agda 或 Lean 证明助手中的形式化数学库，提供了网络结构和语法树表示两种方式，可用于机器学习方法在形式化数学中的进一步研究和评估。

Oct, 2023

利用自动定理证明方法解决国际数学奥林匹克竞赛（IMO）几何问题的研究中，AlphaGeometry模型与Wu的方法的结合超越了IMO金牌得主的表现，解决了30个问题中的27个。

Apr, 2024

本文使用数种ATP和AI方法证明了3000多个以前未证实的Mizar/MPTP问题，并将ATP解决的Mizar问题的数量从75％提高到80％以上。我们首先尝试了cvc5 SMT求解器，并使用了几个和超级位置系统不同的基于实例化的启发式方法，从而增加了很多新的解决方案。然后，我们使用自动化策略发明来开发cvc5的策略，大大提高了cvc5在困难问题上的性能。总之，这些方法解决了14163个以前未解决的难题中的3021个（21.3％），这是对Mizar大型理论基准的新里程碑和对Mizar的强化。

Jun, 2024