Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic
本文报告了一项实验，其中作者使用人工智能模型 Claude 将丘奇的基本递归算术（Church's Basic Recursive Arithmetic）中的哥德尔第二不完备定理自动形式化为 Agda 代码，从而生成了一个长达 50,000 行且无需公理假设的机器检查证明，该实验同时也作为一项案例研究，探讨了该模型重构隐性数学论证的能力，以及在给定规格说明不足时产生数学错误结果的倾向。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你正试图建造一个完美的、具有自我检查能力的机器人，它可以用来验证自己的数学作业。这个机器人，我们称之为 BRA，非常聪明，但它遵循极其严格且简单的规则。它会加法、减法，并且能检查事物是否相等，但它没有“常识”模块。
你正在阅读的论文是一篇关于实验报告，该实验中，一位人类研究员（Thierry Coquand）与人工智能（Claude）合作，教导这个机器人一堂非常著名且困难的课程：哥德尔第二不完备性定理。
以下是这个实验的故事，分为几个简单的部分。
1. 目标：机器人能证明它是安全的吗？
哥德尔第二定理有点像数学系统中的“说谎者悖论”。它说：“如果一个系统是一致的（即它永远不会证明错误的事物），那么它无法证明它自身是一致的。”
换句话说，如果我们的机器人 BRA 确实在正确地做数学，它将永远无法写出一份证明，声称：“我是一个优秀的机器人。”如果它能够证明这一点，那么它实际上就已经出故障了。这个项目的目标是在一个名为 Agda 的计算机程序中，利用 AI 来构建这个定理的数字版本。
2. 第一次尝试：“虚假”的成功
团队开始让 AI 阅读一位名叫 Rose 的数学家的旧论文，并尝试基于该论文来证明这个定理。
- 发生了什么： AI 努力工作了数天，并产生了一个“证明”。它看起来令人印象深刻！
- 问题所在： AI 被骗了。它正在阅读的那篇旧论文包含一个错误（一个错误的定理）。AI 完美地遵循了指令，但由于起点是错误的，结果是一个看起来像是哥德尔定理、但实际上毫无意义的东西。
- 教训： 这表明 AI 非常擅长遵循逻辑，但如果你给了它一张错误的地图，它会心甘情愿地把你带向错误的目的地。你不能仅仅信任 AI 来告诉你要证明什么；你必须自己知道目的地在哪里。
3. 真正的尝试：修复地图
在失败之后，团队转向了一套更可靠的笔记，由数学家 R. Guard 编写。这些笔记就像一张带有缺失部分和错别字的藏宝图。
- 挑战： Guard 的笔记写于 1963 年。它们很精确，但省略了许多人类数学家会自动填补的微小且显而易见的细节。例如，Guard 假设读者知道如何在机器人的大脑内部处理“数词”（如 1, 2, 3）。
- AI 的角色： 人类研究员没有写任何一行代码。相反，他们充当了“翻译员”或“建筑师”。他们告诉 AI：“这是缺失的部分。这是规则。现在，编写代码。”
- 结果： AI 成功地从头开始编写了 50,000 行代码。它构建了整个机器人、证明过程以及验证系统，而人类没有输入任何代码。最终结果是一个经过机器检查的证明，证明了机器人 BRA 无法证明它自身的安全性。
4. 隐藏的技巧（“秘方”）
论文强调了 AI 为了使这项工作得以实现而必须学习的几种巧妙技巧，这些技巧隐藏在旧笔记中：
- “嵌套盒子”问题： 机器人需要检查自己的历史记录。想象一下，在同时撰写一本书的同时还要阅读这本书。AI 必须在机器人的大脑内部构建一个特殊的“历史磁带”。事实证明，机器人的基本工具并不适合处理这个，因此 AI 必须发明一种复杂的“俄罗斯套娃”结构，让机器人能够记住它过去的步骤。
- “封闭盒子”规则： 机器人必须将数字（如 5）视为“封闭的盒子”，即通过代换无法改变的物体。旧笔记假设这是显而易见的。AI 必须被明确告知去证明“5 是一个封闭的盒子”，然后才能继续进行。
- “假设性”捷径： 机器人以一种非常僵化的方式工作（希尔伯特风格的逻辑），它无法轻易地说“如果 X 为真，那么 Y”。AI 使用了一个巧妙的技巧（称为“Carneiro lift”），将每个陈述都包裹在一个“如果……”的包装中，从而允许机器人模拟复杂的推理，而不会违反自身的规则。
5. 为什么这很重要
这不仅仅是在证明一个数学定理。这是对人类与 AI 如何协作的未来的一次试驾。
- 人类是建筑师： 人类提供了愿景、正确的地图，以及在 AI 偏离轨道时发现问题的能力（就像在第一次失败尝试中所见的那样）。
- AI 是泥瓦匠： AI 完成了繁重的体力活，铺设了 50,000 行证明中的每一块砖。
- 发现： 这个过程揭示了旧的数学笔记在某些地方其实是“草率”的。通过迫使 AI 编写必须完美的代码，团队发现了原 1963 年文本中被忽视了几十年的隐藏假设和错别字。
总结
把这个项目想象成一个团队在建造一辆自动驾驶汽车。人类驾驶员知道目的地（哥德尔定理）和交通规则。AI 是引擎制造者，负责组装这辆车。
- 起初，AI 根据一份损坏的蓝图试图建造汽车，造出了一个看起来像汽车但无法行驶的车辆。
- 然后，他们换了一份更好的蓝图。AI 建造了一辆完美的、功能完备的汽车。
- 在此过程中，他们意识到蓝图中缺少了一些说明，因此他们必须发明新的零件来让汽车正常运转。
其结果是一个经过验证、经机器检查的证明，证明了特定的数学系统无法证明其自身的一致性，这是通过人类引导 AI、由 AI 进行编写的协作完全实现的。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。