我知道的最近的论文是Deep Network Guided Proof Search和Deep Math。这两者都通过建议下一个要使用的前提或策略，修剪搜索树来减少当前基于非 ML 的定理证明者的搜索空间。（非常类似于 Alpha Zero 仍然依赖传统的博弈树搜索，但对其进行了大量修剪！）

End to End Differentiable Proving采用的一种更直接的方法侧重于反向链接证明搜索技术。它将哪个变量替换为哪个规则（例如：将“John”替换为规则：If Human(x) then Alive(x)）的硬性决定替换为一个评分函数，该评分函数为每个可能的替换的好坏分配一个数字是。然后使用束搜索来找到得分最高的替换集。

我会质疑使用模式识别无法解决寻找证据的想法——我在证明事物时非常依赖我的直觉，这几乎只是根据我以前见过的类似问题猜测下一步要尝试哪个方向。这种方法似乎与上述论文非常相似。换句话说，我的直觉是进行模式识别。

另一方面，与人类证明者相比，当前的定理证明者——无论有没有 ML——都相当弱，所以我不会试图用一个来证明雅可比猜想。

很抱歉，因为添加了另一个答案，但我无法取消删除我的消息，并且我没有到达与管理员交谈。

该领域与自动定理证明有关。但据我所知，没有足够强大的自动定理证明器来创建这样的证明。

实际的自动定理证明器使用命题演算或一阶逻辑或二阶逻辑来证明或反驳定理。

例如，如果你想问一个自动定理证明者雅可比猜想是真是假，你必须问这样一个问题：定理“交换代数和集合论和分析意味着雅可比猜想”是对还是错。