💻 computer science

Auto formalisation of Chaitin and of the surprise incompleteness Theorem

本文通过一个案例研究，展示了利用大语言模型（Claude）将蔡廷的第一不完备性定理证明以及 Kritchman-Raz 版本的第二不完备性定理悖论自动形式化为 Agda 代码，旨在证明该模型构建复杂计算模拟并生成经机器验证之证明的能力，同时强调了其在数学推理方面的当前优势与局限性。

原作者： Thierry Coquand

发布于 2026-06-12

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Thierry Coquand

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

大局观：教机器人做数学

想象你有一个非常聪明的机器人（一个名为 Claude 的 AI）和一本非常严格、充满规则的数学教科书，名为“基础递归算术”（Basic Recursive Arithmetic）。这本教科书就像一个有着极其特定规则的游戏：你只能使用基础计数和简单的逻辑，不能使用任何花哨的捷径或“魔法”技巧。

这篇论文的目标是观察这个机器人是否能够阅读一段复杂的、著名的数学证明（关于为什么数学存在极限），并完全用那本严格教科书中的语言将其重写，且过程中不需要人类编写任何一行代码。

答案是肯定的。机器人成功地将两个深刻的数学思想翻译成了这种严格的语言，创造出了一个可以让计算机验证为 100% 正确的证明。

两个核心思想

论文聚焦于两个著名的概念：蔡廷证明（Chaitin's Proof，与第一不完备定理相关）和惊喜考试悖论（Surprise Examination Paradox，第二不完备定理的一个版本）。

1. “短描述”游戏（蔡廷证明）

想象你有一个图书馆，里面收藏了使用有限字符集所能写出的所有可能的的故事。

规则： 有些故事非常短，容易描述；而另一些故事则非常复杂，以至于描述它们的最短方式就是直接把整个故事写下来。
问题： 蔡廷的证明试图寻找一个故事，它如此复杂，以至于无法通过一个短程序来描述。
机器人的挑战： 为了证明这一点，机器人必须在数学教科书内部构建一台“机器”，这台机器能够读取一个故事、运行它并观察它的行为。
障碍： 数学教科书过于简单，无法自然地处理“运行程序”这一过程，因为这通常需要一个复杂的函数（例如阿克曼函数），而教科书并不允许使用它。
解决方案： 人类作者建议了一个被称为“Gandy/Howard majorisation”的技巧。你可以把它想象成给机器人一个油箱。与其要求机器无限期地运行，不如让机器人计算出一个程序完成任务究竟需要多少“燃料”（步数）。它构建了一个特殊的“油表”，保证程序会在油箱耗尽前停止。
结果： 机器人自主构建了这个油表。它证明了，如果你试图描述一个“过于复杂而无法被简单描述”的数字，最终会导致逻辑矛盾（比如证明 0 等于 1）。

2. “惊喜考试”与沙堆

论文的第二部分涉及一个著名的悖论：一位老师宣布下周会有一场惊喜考试。学生们推理说，这不可能是周五（因为如果到了周四还没考试，他们就会知道是周五了），所以也不可能是周四，以此类推……直到他们得出结论：根本不会有考试。但随后老师在周三举行了考试，这确实是一个惊喜。

论文使用了一种由逻辑（由 Kritchman 和 Raz 提出）构成的版本来证明：一个数学系统无法证明其自身的相容性（即证明它不包含矛盾）。

旧方法： 之前的证明通过计算天数或数字的数量来寻找矛盾。
新方法（索里特斯/沙堆悖论）： 作者将此与沙堆悖论进行了对比。
- 如果你有一个沙堆，拿走一粒沙，它仍然是一个沙堆。
- 再拿走一粒，它还是一个沙堆。
- 如果你不断地一粒一粒地拿走，最终你会剩下零粒沙。但在哪一个确切的点上，它不再被称为“沙堆”了呢？
应用：
- 想象一个从 0 到一个巨大数字 $N$ 的数字列表。
- 该逻辑试图证明：“不可能所有的这些数字都拥有短描述。”
- 机器人逐步进行证明。它说：“如果我们假设 0 到 $N$ 的所有数字都有短描述，就会产生矛盾。”
- 然后它移除 0。“好吧，如果 1 到 $N$ 都有短描述，我们仍然会得到矛盾。”
- 它不断地逐个移除数字（就像移除沙粒一样）。
- 最终，它到达了一个点，此时列表已空，但逻辑仍然强制产生了一个矛盾。
转折点： 论文认为这并不是一种“自我指涉的恶性循环”；它更像是沙堆。你可以安全地拿走一粒沙（一个数字），但如果你一直这样做，整个结构就会崩塌。这种崩塌证明了，该数学系统如果不破坏自身，就无法证明它是安全的（相容的）。

为什么这很重要（根据论文所述）

AI 作为数学助手： 论文表明，目前的 AI（如 Claude）已经足够擅长处理复杂数学证明中那些微小、繁琐的细节。它可以构建解析器、评估机器，并处理人类通常需要手动完成的逻辑步骤。
构造性数学： 论文强调，在“构造性数学”（即你必须实际构建出你所谈论的事物）中，“部分函数”（可能永远运行下去的程序）的概念非常微妙。机器人必须使用一个可能永远运行下去、但证明保证其会停止的“循环”程序。这是一个细微但至关重要的区别，而 AI 正确地处理了它。
没有魔法技巧： 机器人没有使用任何“策略”（tactics，即捷径）或高级库。它仅利用基础规则，从零开始构建了一切。这使得证明非常稳健，且易于计算机验证。

结论

这篇论文是一个案例研究，展示了 AI 现在可以成为形式化数学的强大伙伴。它可以将高层级的思想（例如“数学是有极限的”）转化为一种严谨的、可由机器检查的格式。

作者指出，虽然 AI 需要人类的引导（例如建议使用“油箱”技巧），但 AI 随后可以自主编写代码、构建逻辑并记录整个过程。其结果是一个经过完全验证的证明，它阐明了这些深刻的逻辑悖论究竟是如何运作的，剥离了歧义，只留下硬核的逻辑事实。

技术摘要：Chaitin 与“惊喜不完备性定理”的自动形式化

问题与背景
本报告扩展了之前利用大语言模型（LLM）Claude 和证明助手 Agda 对哥德尔第二不完备性定理进行自动形式化的实验。主要目标是调查当前 LLM 在形式化复杂数学证明（特别是涉及计算内部表示的证明）方面的能力与局限性。本文重点关注两个特定目标：Chaitin 对第一不完备性定理的证明，以及 Kritchman-Raz 的“惊喜考试悖论”版本的第二不完备性定理。

一个核心的技术挑战在于在**基本递归算术（Basic Recursive Arithmetic, BRA）**中对计算进行编码。BRA 是由 Guard 提出的一个系统，它缺乏对象量词和标准的策略（tactics）。在这样的系统中，定义一个内部评估函数是不可能的，因为这会超过原始递归的界限（类似于阿克曼函数）。该问题要求在不依赖元层函数或外部库的情况下，完全在对象语言内部表示程序及其执行步骤。

方法论
本项目采用了一种“斯巴达式”的方法，即人类作者没有编写任何 Ag agda 代码；所有的形式化工作都是由 Claude 根据高层数学描述自主生成的。该方法论依赖于以下技术策略：

三进制字符串编码： 程序被表示为解释为三进制字符串（数字 1, 2, 3）的自然数。这使得长度至多为 $L^*$ 的程序集合可以被视为自然数的一个简单初始段 $\{p < N\}$ ，其中 $N = 3^{L^*+1}$ ，从而避免了复杂的枚举机制。
CK 机器实现： 为了绕过对全局评估函数的需求，Claude 自主构建了一个延续栈小步评估机（Landin CK 机器）。该机器分解表达式并管理一个延续栈，从而允许逐步模拟计算。
Gandy/Howard 极大化（Majorisation）： 一个关键障碍是在逻辑内部证明机器对于给定函数 $f$ 在特定步数内停止。由于步数不能是元层面的自然数，作者引导 Claude 使用 Gandy/Howard 极大化方法。这涉及通过原始递归定义一个闭合组合子 fuel(f)，该组合子可证明地极大化了 $f$ 的实际运行时间。这使得可以在 BRA 内部陈述并证明解释器的完备性。
作为索里特斯（Sorites）的惊喜考试： 第二不完备性定理的证明避免了 Kritchman 和 Raz 使用的计数论证。相反，它将论证建模为索里特斯（堆沙悖论）。它通过对阶段 $r$ 进行外部归纳进行推演，证明在区间 $[r, N]$ 内并非所有数字都具有短描述是不可能的。

主要贡献与结果
本文展示了在 Agda 中对 Church 的基本递归算术（BRA）的以下结果进行的完整机器检查证明：

自动形式化的 Chaitin 定理： 系统成功形式化了 Chaitin 的证明，该证明用柯尔莫哥洛夫复杂度取代了说谎句子。该形式化产生了一个显式的证明转换器 $G$ 。定理指出，如果项 $w$ 编码了不可压缩性语句 $K(out(w)) > L^*$ 的证明，那么 $G \cdot w$ 则编码了 $0=1$ 的证明。这被表述为一个正向的对象级蕴含，而非关于可证明性的元理论否定。
内部化的第二不完备性： 本文形式化了 Kritchman-Raz 的论证，以表明如果 $T$ 证明其自身的一致性（ $Con_T$ ），则 $T$ 是不一致的（ $0=1$ ）。证明通过从 $S(0)$ （抽屉原理）到 $S(N+1)$ （矛盾）的下降过程进行，其中每一步 $S(r) \to S(r+1)$ 恰好消耗一次一致性假设。
构造性洞察： 形式化强调了部分函数在构造数学中的作用。具体而言，对角线程序会枚举可导出的公式直到找到目标。虽然该程序在外部被证明是终止的，但其规模是在没有内部化终止证明的情况下计算的。这展示了 Blum 加速现象的一种体现，即允许使用部分递归程序（通过外部证明保持全函数性），可以比那些必须在内部证明停机的程序拥有无界缩短的程序。

意义与主张
本文声称，当前的编码 LLM（如 Claude）是理解数学论文细粒度细节的有效工具，前提是它们在持续监督下运行。该项目作为一个案例研究，证明了：

LLM 能够在高层结构提示的引导下，自主生成复杂的语法机制（解析器、评估机）和逻辑论证（极大化）。
类型论（特别是没有策略的 Agda）非常适合表达涉及计算和编码的具体数学，因为证明可以直接表示，而不需要函数外延性或商类型。
当形式化时，“惊喜”论证更接近于索里特斯悖论而非传统的惊喜考试悖论，因为矛盾源于可靠步骤的迭代，而非单个自我指涉循环。

作者总结道，虽然类型论的语言非常适合这种组合数学和计算数学，但一个关键的研究问题仍然存在：如何设计能够以类似自动化程度处理非组合对象的形式系统。该形式化澄清了 Chaitin 和 Kritchman-Raz 原作中隐含的细节，并在一个极简的算术框架内为这些论证提供了严谨的、机器验证的基础。