🔢 mathematics

Formal Foundations and Proof-Carrying Certificates for q-ary Covering Codes in Lean 4

本文在 Lean 4 中实现了 q 元覆盖码初等理论的形式化，建立了一个可重用、可审计的基础，并提供带有证明载体证书的机制，用于验证覆盖数的上界与下界。

原作者： Andreas Florath

发布于 2026-06-09

📖 1 分钟阅读🧠 深度阅读

原作者： Andreas Florath

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

想象一下，你正试图用有限数量的“安全网”覆盖一个巨大的、多维的棋盘。

在数学世界中，这就是**覆盖码（Covering Codes）**问题。你有一个可能的坐标网格（就像一个棋盘，但它可能是三维、四维甚至更高维度的）。你想在这个网格上放置少量的“中心点”。规则是：棋盘上的每一个方格都必须在距离其中至少一个中心点一定的距离内（比如一步之遥）。

核心问题是：要覆盖整个棋盘，我们绝对最少需要多少个中心点？

这篇由 Andreas Florath 撰写的论文并不是试图寻找一个新的、更小的中心点数量记录。相反，它构建了一个数字化的、不可破解的保险库，用以证明我们已知的那些数字是正确的。

以下是使用简单类比对该论文思想的拆解：

1. “携带证明的证书”（金票）

通常，当一位数学家说：“我发现了一个用 73 个中心点覆盖棋盘的代码，”他们会向你展示一串数字列表。你必须信任他们，或者得花好几个小时亲自检查这些数学过程。

这篇论文引入了**“携带证明的证书”（Proof-Carrying Certificate）。请不要仅将其视为一份数字列表，而应将其视为一张带有内置自检魔术功能的金票**。

这张票： 它写着：“这里有一组 73 个中心点。”
这个魔术： 这张票包含了一个微型自动化机器人（使用一种名为 Lean 4 的语言编写），它能瞬间检查棋盘上的每一个方格并确认：“是的，这个方格被覆盖了。是的，那个方格也被覆盖了。是的，所有方格都被覆盖了。”
结果： 你不需要信任作者。你只需要运行这个机器人。如果机器人显示“通过”，那么这个证明在数学上就是 100% 保证的。

2. “两部分拼图”

为了证明你拥有的是最完美（精确）的数量的中心点，你需要同时解决两个不同的谜题：

上界（构造法）： “我可以用 73 个中心点覆盖棋盘。”（你展示出清单）。
下界（不可能完成的任务）： “用 72 个中心点是不可能覆盖棋盘的。”（你证明无论如何尝试，总会留下漏洞）。

这篇论文构建了一个系统，使这两个谜题成为独立的碎片。你可以拥有一个关于“73”的证书，以及一个关于“72 不可能”的独立证书。当它们相遇时，就会严丝合缝地拼凑在一起，形成一个完美的、精确的答案。

3. 数学的“乐高”

作者构建了一个庞大的乐高积木库（形式化规则）。

有些积木很简单：“如果你能覆盖一个小棋盘，那么通过添加一些部件，你就能覆盖一个更大的棋盘。”
有些积木很复杂：“如果你将两种不同类型的棋盘组合在一起，覆盖规则会如何精确变化。”

这篇论文的美妙之处在于，这些积木是可互换的。如果其他人找到了新的覆盖棋盘的方法，他们只需将新的积木卡入这个现有的乐高结构中，整个系统就会自动验证它。

4. “真理数据库”

这篇论文包含了一个携带证明的数据库。想象一本图书馆里的书，它不仅印着答案“7”，还包含了证明过程的视频录像。

如果你在数据库中查找一个数字，它不仅仅给你一个数字。它会给你轨迹（trace）（即证明的逐步演示过程）。
你可以在 Lean 4 系统中重放这段“视频”，它会从头开始重新运行证明，以确保证明依然成立。

5. “足球集资”示例

论文使用了一个现实世界的类比来解释这个问题：足球集资（Football Pool）。
假设你正在对 8 场足球比赛进行投注。每场比赛有 3 种可能的结果（胜、平、负）。你想购买一组投注单。

目标： 无论实际结果如何，你都希望保证至少有一张投注单是“接近”的（比如只猜错 1 个）。
数学： 你需要购买多少张投注单才能保证这一点？
论文的角色： 该论文采用了针对这一问题的一个著名的已发表方案（即有人发现了一个需要 486 张投注单的方案），并将其转化为了一个机器可检查的证书。它证明了 486 张投注单确实有效，且毫无疑问。

这篇论文实际声称了什么（以及没有声称什么）

它声称： 它建立了一个坚实的、可重用的基础（一个“形式化基础”），可以在其中自动存储、检查和组合覆盖码证明。它利用这个新系统验证了几个特定的已知数值（例如 8 场比赛问题中的 486 张投注单）。
它并未声称： 它并没有声称发现了覆盖所需最少投注单数量的新纪录。它也没有声称解决了所有可能场景下的问题。这是一篇工具构建型的论文，而不是打破纪录型的论文。

大局观

你可以将这篇论文看作是在为数学真理建造一座高安全性保险库。以前，如果你想检查一个复杂的覆盖码，你必须信任人类或可能存在 Bug 的计算机程序。现在， thanks to 这篇论文，你拥有了一个系统，其中的证明本身就是一段软件，你可以运行它来瞬间验证真理。它将“我认为这是对的”变成了“计算机已经证明这是对的”。

技术摘要：基于 Lean 4 的 q 元覆盖码的形式化基础与证明携带证书

问题陈述
有限汉明空间中的覆盖码旨在寻找最小的字集（码字），使得其半径为 $r$ 的汉明球的并集覆盖整个空间 $A^n$ 。核心量是 $q$ 元覆盖数 $K_q(n,r)$ ，定义为此类码集的最小规模。尽管定义非常基础，但确定 $K_q(n,r)$ 的精确值或紧确界通常依赖于显式构造、计数论证、递归关系和计算机搜索的混合方法。该领域的一个显著挑战在于，精确陈述 $K_q(n,r) = k$ 需要两个独立的组成部分：一个证明上界的显式构造（ $K_q(n,r) \le k$ ）以及一个证明不存在更小码集的下界证明（ $K_q(n,r) \ge k$ ）。由于这些组件往往源自不同的来源，导致验证精确值的过程难以审计。

方法论
本文展示了在 Lean 4 定理证明器中对初等覆盖码理论的形式化实现。其方法论具有三个核心设计选择：

字的表示： 字被建模为从坐标类型到字母表的依赖函数。通用的 $q$ 元汉明空间长度为 $n$ 的表示形式为 Fin n → Fin q。这种函数式表示保留了抽象坐标类型的通用接口，同时简化了 $q$ 元特例化。
证书风格谓词： 本文并未将 $K_q(n,r)$ $K_{q} (n, r)$ 定义为一个不可计算的极小化函数，而是使用逻辑谓词来表示关于覆盖数的断言。
- KUpper r k：断言存在一个规模至多为 $k$ 的有限覆盖码（上界）。
- KLower r k：断言每一个有限覆盖码的规模至少为 $k$ （下界）。
- KSpec r k：结合两者以断言精确性（即 $K_q(n,r) = k$ ）。
  这种模块化方法允许将来自不同来源的上界和下界进行独立组合。
证明携带数据库： 本文实现了一个数据库，其中存储的界限不仅是数值，更是“证明携带”的对象。每个条目都包含一个推导轨迹。在 Lean 中重放此轨迹可以重建对应 QaryKUpper 或 QarrayKLower 谓词的形式化证明。系统区分了手工编写的数学定理（经内核检查）和生成的数据（来自不受信任的生产者，其输出通过轨迹重放进行验证）。

主要贡献
本文建立了一个可重用、可审计的机器检查覆盖码证书的形式化基础。其具体贡献包括：

形式化基础设施： 一个完整的 Lean 4 框架，用于处理有限汉明空间、汉明距离、闭球和覆盖谓词，并在定义中严谨地处理边缘情况（例如 $q=0, n=0, r \ge n$ ），而非将其作为非正式约定。
分析结果： $q$ 元汉明球体积公式和经典球面覆盖下界的正式证明。球面覆盖界被封装为一个可计算函数 sphereLower，用于生成经过认证的下界证书。
结构化定理： 初等精确情况的形式化（例如 $K_q(n,0) = q^n, K_q(n, n-1) = q$ ）以及结构化构造，包括乘积覆盖定理以及各种邻域关系（打孔、增长、字母表投影和拼接），这些关系可在参数三元组之间传递界限。
案例研究（Van Laarhoven 等人）： 一个展示已发表显式码形式化的端到端工作流。作者将 1989 年一篇论文（Van Laarhoven 等人）中的覆盖码转录为 Lean 代码，并将其编码为紧凑数组以避免阐述限制。系统验证了覆盖属性和基数，产生了关于 $K_3(6,1) \le 73, K_3(7,1) \le 186, K_3(8,1) \le 486$ 的机器检查上界证书。
数据库实现： 一个包含 52,822 个条目的证明携带数据库，参数范围为 $0 \le q \le 21, 0 \le n \le 48, 0 \le r \le 48$ 。该数据库包括小规模情况的精确证书（例如 $K_2(5,1)=7, K_3(3,1)=5$ ）以及通过轨迹重放得到的区间。

结果
该形式化成功验证了：

$q$ 元球体积公式和球面覆盖下界。
初等精确值，如 $K_2(5,1)=7, K_2(6,2)=4, K_3(3,1)=5$ 以及 $K_4(3,1)=8$ 。
源自显式码的三元足球问题（ternary football-pool problem）的上界，具体为 $K_3(6,1) \le 73, K_3(7,1) \le 186, K_3(8,1) \le 486$ 。
一个统一的两块循环构造，证明了 $K_q(3,1) \le \lceil q^2/2 \rceil$ 。

数据库闭合过程成功地通过经过认证的关系规则传播这些原始来源，从而生成了一张一致的界限表。系统支持两种证明模式：使用标准 decide 以获得更强重放保证的“内核模式”，以及使用 Lean 编译评估器以实现更快开发的“原生模式”，并为每种模式定义了清晰的信任边界。

意义与主张
本文明确指出，其主要贡献并非发现新的纪录级界限或复现现有文献中的表格。相反，其意义在于提供了一个用于覆盖码证书的形式化接口和可审计的基础。

这项工作架起了经典覆盖码文献与未来计算证书之间的桥梁。通过将上界见证、下界论证和精确性谓词分离，该形式化允许来自显式构造、组合计数以及（潜在的）SAT 或整数规划求解器的结果在单一的可信框架内被检查和组合。这种“证明携带”性质的数据库确保了报告的每个界限都可以追溯到机器检查的证明，解决了该领域固有的可复现性和验证挑战。本文将自己定位为迈向未来——即计算搜索结果能够无缝集成到形式化数学库中——的基础性一步。