Formalizing the Real Numbers in Homotopy Type Theory with Cubical Agda
本文在 Cubical Agda 中形式化了同伦类型论中柯西实数的构造，证明了该方法避免了其他构造性定义中固有的可数选择、集合论开销及宇宙层级追踪问题，且无需公设即可通过类型检查。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象你正在试图建造一把完美的、无限长的尺子，用以测量宇宙中的一切。在经典数学的世界里，这把尺子很容易描述：你只需取所有可能的“近似”测量值（如 3.1、3.14、3.141 等），并断言：“如果两个测量序列彼此越来越接近，它们就代表尺子上的同一个点。”
然而，在构造性数学中——这是一种坚持你必须能够实际构建或计算你所谈论之物的数学风格——这种简单的方法行不通。要证明你的尺子是完备的，你必须做出一个“神奇”的选择：你必须从无限多个选项中挑选一个具体的测量值来代表最终的点。构造性数学说：“不允许魔法。如果你不能向我展示如何挑选它，你就还没有建成这把尺子。”
几十年来，数学家们不得不做出妥协。他们要么使用让每个计算都变得混乱的“记账”技巧，要么以需要追踪复杂“宇宙层级”（就像给盒子的大小记分）的方式来构建尺子。
新蓝图（HoTT 书中的实数）
本论文提出了一种构建尺子的新蓝图，源自著名的《同伦类型论（HoTT）》一书。这种方法不是先通过拼接碎片再试图将它们平滑化来构建尺子，而是同时构建尺子及其“平滑性”规则。
这就像建造一座房子，墙壁和蓝图是在完全相同的时间被绘制出来的。
- 砖块：你从简单、已知的数字（如分数）开始。
- 粘合剂：你添加一条特殊规则，规定“如果两个点足够接近，它们实际上是同一个点”。
- 魔法：由于“接近”规则被内置于房子本身的定义中，你之后就不需要再做出那些“神奇”的选择了。一旦你铺完砖块，房子就完工了。
挑战：计算机翻译器
作者 Jackson Brough 将这一理论蓝图尝试翻译成计算机能够理解并验证的语言：Cubical Agda。
想象一下，试图向一个只理解严格、字面指令的机器人解释一套复杂的舞蹈动作。
- 问题：此前尝试翻译该蓝图的尝试之所以失败，是因为计算机语言缺乏正确的“动作”（具体来说，它无法处理尺子定义与接近性规则的同时定义）。翻译者不得不声称“假设这个动作存在”，这在数学中属于作弊。
- 解决方案：Cubical Agda 是一个更新、更聪明的机器人，它原生理解这些复杂的动作。它允许作者完全按照设计初衷来书写蓝图，无需作弊。
翻译过程中发生了什么？
这篇论文不仅仅关乎输入代码；它关乎作者试图让计算机理解数学时发生了什么。计算机的严格性迫使作者发现了原始解释中隐藏的漏洞：
- “替代”映射：原书描述了如何检查两个点是否接近。但当作者尝试编写代码时，他们意识到书中的方法就像一条“单行道”。你可以证明点是接近的，但无法轻易反向推导以理解原因。作者必须构建第二个“计算”映射（称为替代关系），它像倒挡一样，允许计算机实际计算出答案。
- 缺失的要素：书中描述了一条构建函数（如乘法）的规则，仿佛计算机可以“记住”原始的近似值列表。作者的第一版代码忘记了这种记忆。计算机拒绝了它。作者不得不重写该规则，明确地携带这种记忆，从而意识到原始文本对机器而言过于模糊。
- 多变量谜题：书中暗示，针对单个数字的规则可以轻松应用于数字对或三元组。计算机并不信服。作者必须证明一个新的、具体的引理，表明如果一个规则对一个变量有效，那么只要逐个检查，它对两个变量也有效。
结果
最终成果是一个庞大的开源代码库（超过 13,000 行代码），它证明了 HoTT 书中的实数完美运作。
- 它证明了这些数字构成了一个完备的有序域（你可以对它们进行加、减、乘、除和比较）。
- 它证明了这把尺子是“阿基米德”的（意味着无论你的间隙有多小，你总能找到一个分数填入其中）。
- 最重要的是，这一切都是在不作弊的情况下完成的。计算机检查了每一个步骤，代码运行无需任何“魔法假设”。
总结
这篇论文讲述了一个将优美的高层数学思想带入计算机验证的严谨、字面世界并使其生存的故事。通过这样做，作者不仅构建了一把数字尺子；他们还打磨了蓝图本身，揭示了隐藏的细节，使该理论比以往更加强大和精确。该代码现已可供任何人使用，作为未来数学发现的坚实基础。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。