A Lean 4 Formalization of Euclidean Domain Algorithms from a 1986 Icon Experimentation Package
本文呈现了对 1986 年 ICON 欧几里得域算法的完整 Lean 4 形式化实现，通过将数学定义、可计算实现以及遗留输出复现进行分离，在为核心程序提供机器检查证明的同时，保留了原始基准测试结果。
原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。 阅读完整免责声明
想象一下，你有一本来自 1986 年、由一位名叫 Lars 的厨师编写的陈旧且落满灰尘的食谱书。这本书包含了 14 个特定的、复杂的关于“烹饪”数字的食谱（例如寻找最大公约数、解决余数谜题以及操作多项式）。这本原始食谱是用一种叫做 Icon 的语言编写的，这种语言在当时就像一种非常棒的专业化厨房工具，但现在的计算机已经很难理解它了。
这篇论文讲述了一个团队如何将这本 1986 年的食谱书翻译成 Lean 4——一种现代的、极其严苛的用于证明数学真理的语言。但他们不仅仅是翻译了文字，他们还重建了整个厨房，以确保做出的食物味道完全一致，同时还增加了一位“安全检查员”来检查数学是否真的正确。
以下是他们是如何完成这项工作的，通过简单的概念进行了拆解：
1. 三层厨房架构
最大的挑战在于，现代数学工具（称为 Mathlib）就像是一个高科技、自动化的厨房。它们完美且经过证明，但它们是“不可计算的”——这意味着你无法在屏幕上实际运行它们来查看结果；它们只作为抽象的证明而存在。然而，1986 年的 Icon 软件包却是一个“运行并观察”的系统。
为了弥补这一差距，作者构建了一个拥有三个不同楼层的厨房：
- 第一层：证明层（安全检查员）。 这一层使用现代的高科技 Mathlib 工具。它包含了“金标准”级别的数学定义。如果你问这一层：“这个食谱正确吗？”它会给你一个机器检查过的“是”。但是，你无法在这里进行实际的烹饪。
- 第二层：可计算层（工作厨房）。 这一层是一个专门构建的、复古风格的厨房，它精确地模仿了 1986 年的 Icon 系统。它使用纯粹的、逐步执行的指令，计算机可以实际运行这些指令来产生结果。它还没有配备“安全检查员”，但它产生的数字与 1986 年的原版完全一致。
- 第三层：报告层（服务员）。 这一层负责格式化输出。它从“工作厨房”中获取数字，并以与 1986 年报告完全相同的字体、间距和风格进行打印。这让团队能够进行“抽查”，以确保新系统是旧系统的完美克隆。
2. 机器中的“幽灵”（发现笔误）
这个项目中最令人兴奋的部分之一是一个历史性的谜团。在 1986 年的报告中，有一个关于特定计算（称为 PREM）的结果表格。打印出来的表格显示了一个巨大且复杂的数字作为答案。
然而，当作者在现代计算机上运行原始的 1986 年代码时，答案却是 零。
论文解释说，1986 年的报告在打印表格时有一个笔误。数学逻辑其实很简单：用一个多项式除以一个常数，余数应该始终为零。新的 Lean 系统通过实际“烹饪”食谱并发现结果为零（而不是打印出的那个巨型数字），从而抓住了这个错误。他们通过运行代码，修复了一个长达 40 年的文档错误。
3. 他们真正证明了什么（以及没能证明什么）
作者非常诚实地说明了哪些内容是“已证明的”，哪些仅仅是“被信任的”。
- “已证明”的内容（A 级）： 对于基础整数运算（如寻找两个整数的最大公约数），他们使用了现代的“安全检查员”。他们拥有机器检查过的保证，证明这些特定的算法在数学上是完美的。
- “被信任”的内容（B 级）： 对于更复杂、更高级的食谱（如多项式除法或快速傅里叶变换），他们尚未证明这些内容与现代“安全检查员”相匹配。相反，他们依赖于回归测试。这意味着他们运行了新代码，并将其输出与 1986 年的输出进行逐行对比。由于 1986 年的代码运行了 40 年且表现良好，而新代码与其完美匹配，因此他们“信任”它。
- “待办事项”（C 级）： 他们确定了“一致性义务”。这就像是对未来工作的承诺：“我们承诺最终会证明‘工作厨房’（第二层）产生的精确结果与‘安全检查员’（第一层）是一致的。”他们目前还没有完成这一点，但已经明确勾勒出了证明需要进行的路径。
4. 为什么这很重要
这篇论文并不是关于发明新数学，也不是关于将这些算法用于医疗诊断或太空旅行。它是关于保存与验证。
- 保存： 他们通过将 1986 年的 Icon 软件包翻译成一种在 50 年后仍能被阅读的语言，保存了一段计算机科学的历史。
- 验证： 他们展示了即使是“旧”算法也可以被严谨地检查。他们证明了 1986 年的逻辑是成立的，即便原始的打印报告中存在笔误。
- 透明度： 他们清晰地标注了哪些代码部分是经过数学证明的，哪些部分仅仅是“我们检查了它并发现它与旧书匹配”。
简而言之，这篇论文是一次时光胶囊的翻修。他们接手了一座旧的、略显落尘的房子，用现代钢材（Lean 证明）加固了地基，保留了原有的家具布局（1986 年的算法），甚至还发现了一处长达 40 年无人察觉的墙壁裂缝（那个笔误）。
您所在领域的论文太多了？
获取与您研究关键词匹配的最新论文每日摘要——附技术摘要，使用您的语言。