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

Nov, 2012

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

Sep, 2013

在Mizar的40周年庆典上，我们成功地开发了一个AI/ATP系统，可以在30秒内自动验证最新版本的Mizar数学库(MML)中约40%的定理，成功地实现了对MML的大规模AI/ATP方法的改进，并将最有用的方法高效地实现使其适用于MML中的150,000个公式，从而将训练时间从大规模语料库中缩短至1-3秒，将该方法简单地部署到Mizar用户的在线自动推理服务(MizAR)中。

Oct, 2013

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

Jun, 2014

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

Jan, 2017

CD Tools是一个使用证明结构为中心的形式化视图来实践压缩分离的Prolog库，其中包括基于证明结构枚举的专门证明器，其中SGCD具有特别灵活的混合证明搜索方式，并在实验中显示了该方法的特征和应用潜力。

Jul, 2022

本文对自动证明系统(Automated Theorem Proving, ATP)在一阶模态逻辑问题的QMLTP库中的表现进行了评估，主要采取了嵌入法将问题转换为TPTP语言中的高阶逻辑，使用高阶逻辑ATP系统进行求解，并将原生模态逻辑ATP系统的结果与嵌入法进行比较，得出结论：(一)嵌入过程是可靠和成功的；(二)后端ATP系统的选择会显著影响嵌入方法的性能；(三)原生模态逻辑ATP系统胜于嵌入方法；(四)嵌入方法可以处理比原生模态系统涵盖更广的模态逻辑。

Dec, 2022

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

Mar, 2023

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

Jun, 2024

本文解决了大型语言模型在逻辑推理任务中准确性不足的问题。研究提出了一种神经符号架构，通过将LLM作为翻译前端并结合自动推理引擎来解决逻辑问题，实现了基于自动定理证明器的语义错误修正。结果表明，该方法显著减少了语义错误，提高了LLM的推理准确性。

Aug, 2024