Case study: proving sqrt(2) irrational with LPTP and an LLM

想象一下，你是一名正在试图破解一个困扰了人类两千多年的谜题的侦探：$\sqrt{2}$ 是一个“有理数”吗？在数学世界里，有理数就像是一个完美的切片，是完美的饼干（比如 $3/4$ 或 $5/2$）。而无理数则是混乱、永无止境的小数，永远无法写成一个简单的分数。$\sqrt{2}$ 是一个边长为 1 的正方形的对角线长度，古代数学家已经证明它是“混乱”的——它无法表示为一个分数。

现在，想象你有两个截然不同的工具来帮助你解决这个问题。第一个工具是一个超级严格、像机器人一样的裁判，名叫 LPTP。它使用一种非常精确、逻辑严密的语言（基于 Prolog），只有当每一步在数学上都完美无瑕时，它才会接受一个证明。如果你犯了哪怕一个微小的错误，它就会落下法槌并宣布：“不对，无效。”第二个工具是一个大语言模型（LLM），它就像一个超级聪明、极具创造力的学生，几乎读过人类写过的所有东西。这个学生擅长猜测故事或数学问题的下一步，但有时它也会“幻觉”——编造一些听起来很有道理但实际上是错误的事实。

现在的科学界面临的一个大问题是：我们能否将这两者结合起来？我们能否让这个富有创造力的学生负责繁重的写作工作，同时让这个严格的裁判检查每一句话，以确保这个学生没有撒谎？这篇论文正是通过这个案例，探讨了这种伙伴关系，并以 $\sqrt{2}$ 的无理性作为测试用例。

---

伟大的证明检查协作

在这篇论文中，作者们试图探索是否可以使用一种现代 AI（具体来说是一个名为 Claude 的模型）来帮助证明 $\sqrt{2}$ 是无理数，但有一个转折：证明必须以一种非常特定、严格的格式编写，以便让机器人裁判（LPTP）能够理解并验证。他们不仅仅是想让 AI 说“它是正确的”；他们希望 AI 能够写出实际的逐步逻辑，然后由裁判进行评分。

故事始于一个简单的想法。要证明 $\sqrt{2}$ 是无理数，通常你会假设其相反的情况：即它是一个由两个整数 $p$ 和 $q$ 组成的分数，且这两个数没有公因数（它们是“互质”的）。如果你进行计算，最终会遇到一个矛盾：这两个数都必须是偶数，这意味着它们确实有一个公因数（2）。这打破了它们是互质的规则，从而证明了最初的假设是错误的。

作者尝试让 AI 用 LPTP 的严格语言来编写这个证明。起初，这个 AI 就像一个知道故事内容却无法按照要求的格式写出论文的学生。它会试图跳过步骤或进行逻辑飞跃，而这些行为是不会被裁判接受的。

这就是协作发生的地方。作者建立了一个反馈循环：

1. AI 尝试编写一个证明步骤。
2. 裁判（LPTP）对其进行检查。
3. 如果裁判发现错误，它会指出逻辑出错的具体行。
4. 作者将这个错误展示给 AI。
5. AI 再次尝试，修正特定的错误。

这个过程就像是在玩一场“热与冷”的游戏。裁判不仅仅是说“错了”，它还会说“你在第 4 步犯了错”，从而让 AI 能够纠正航向。

结果：部分的胜利

实验取得了成功，但也存在一些限制。AI 能够独立完成许多较小、较简单的部分。例如，它成功证明了“如果一个数是偶数，那么它的平方也是偶数”或者“2 倍于一个数也是偶数”。作者称这些为“引理”（小的辅助证明）。AI 成功完成了这些任务，有时甚至能提出一些人类并未想到的新的辅助思路。

然而，对于证明中最难的部分——即展示为什么 $\sqrt{2}$ 不可能是一个分数的特定逻辑——AI 卡住了。它无法靠自己找到正确的路径。因此，人类作者不得不介入，给 AI 一个“提示”，甚至亲自编写了证明的主干结构，然后要求 AI 去填充其中的微小间隙。

最终，他们完成了一个完整的、形式化的证明，证明了 $\sqrt{2}$ 是无理数。这个证明部分由 AI 编写，并由机器人裁判进行了全面检查。裁判给了它一个合格的分数，确认了逻辑是严密的。

这意味着什么

这篇论文并不声称 AI 现在可以独立解决所有的数学问题。事实上，作者明确指出，如果没有人类的引导和严格工具的检查，AI 可能会产生一个虚假或破碎的证明。

相反，这篇论文提出了一种新的工作方式：AI 作为草稿撰写者，人类作为编辑，而形式化工具作为事实核查员。 AI 快速且富有创造力，能够生成想法并填充细节，而形式化工具（LPTP）则扮演着一个不眨眼的眼睛，捕捉幻觉和错误。

作者还测试了其他自动化数学工具（称为 ATP），看它们是否能更快地完成工作。这些工具虽然速度快且免费，但它们生成的证明难以被人类阅读，也无法轻易添加到经过验证的数学库中。相比之下，AI 的方法虽然较慢且需要人类协助，但它生成的证明具有可读性，并且可以安全地存储以备后用。

简而言之，这篇论文表明，我们不需要在人类直觉和机器精度之间做选择。通过让 AI 承担繁重的起草工作，让严格的工具进行评分，我们可以建立一个系统，让 AI 帮助我们证明复杂的数学真理，只要我们保持人类在其中引导方向，并配备一名严格的裁判来检查地图。$\sqrt{2}$ 依然是无理数，但现在我们有了一种全新的、协作的方式来证明它。