本文提出了使用机器学习自动化证明助手交互的问题。研究人员通过构建 CoqGym 数据集和 ASTactic 模型，能够生成高效的策略程序并用于自动证明定理。

May, 2019

Drori 等人（2022 年）使用符号代数包 Sympy 而非神经网络解决了大学数学问题，并通过计划合成和少量学习回答了 81％的问题，此外，它的 “解释” 仅是代码行的改写且在某些情况下似乎使用测试语料库中给定的答案来指导其解决问题的步骤。

Aug, 2022

提出了一种定理证明算法，该算法使用几乎没有领域启发式来指导其连接风格的证明搜索，而是运行许多蒙特卡罗模拟，通过强化学习来指导以前的证明尝试。

May, 2018

本文提出了一种用于高级数学推理的数据集，研究了神经序列到序列模型的推理能力。实验结果表明，该任务具有挑战性，但神经模型能够捕捉到非平凡的数学推理，提出的分层 Transformer 的性能也好于基准 Transformer。

Jun, 2020

自动定理证明器和形式证明助手是理论上能够证明任意难题的一般推理系统，但在实践中面临组合爆炸所以包括很多启发式算法和选择点来影响系统性能。机器学习预测器可以引导这些推理系统的工作。本文概述了几个自动推理和定理证明领域及目前对它们进行的学习和人工智能方法，包括前提选择、证明引导、协同推理和学习的 AI 系统以及符号分类问题。

Mar, 2024

本文提出了一种利用机器智能在数学数据中找到抽象模式生成数学不等式的猜想的系统方法，以 < f<g 类型的严格不等式为重点研究对象，并将它们与一个向量空间相关联，并在这个称为猜想空间的空间中执行几何渐进式下降算法，生成了有关素数计数函数和非阿贝尔简单群的 Cayley 图直径的新猜想，并突显了该空间中数学发现的重要性和领域专业知识的必要性。

Jun, 2023

该研究探讨了自动解决数学问题的挑战，包括语言和逻辑之间的语义鸿沟，综述了将人工智能用于代数和几何问题的主要技术及其性能，并探讨未来的研究方向。

Aug, 2018

介绍了一个基于不等式定理证明的学习辅助定理证明基准，旨在测试代理程序的泛化能力。该基准提供了轻量级且用户友好的定理证明环境，并评估了基于学习的基线和 Monte Carlo 树搜索。

Jul, 2020

该研究介绍一种归纳逻辑编程方法，结合否定和谓词发明，以应对从少量例子中推广的挑战，在多个领域的试验结果表明，该方法改善了预测精度和学习时间。

Jan, 2023

本文介绍一种使用 Isabelle 证明助手对自动推理课程学习成果进行测试的方法，该方法允许测试不同逻辑证明系统中形式证明的一般理解和特别是在 Isabelle/HOL 高阶逻辑中证明的理解，最终讨论了使用该方法考试并进行评分的经验和未来潜在的工作。

Mar, 2023