在Agda中证明算术基本定理

# 博客 :: Brent -> [String] 来源：https://byorgey.github.io/blog/posts/2026/06/26/FTA.lagda.html **tl;dr**：这是一份完全注释的、从头开始用 Agda（https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.HomePage）证明算术基本定理的完整代码，面向那些已经了解一些 Agda 但可能受益于阅读和完成一个较大示例的人。请参阅下面的引言和目录（https://byorgey.github.io/blog/posts/2026/06/26/FTA.lagda.html#table-of-contents）以获取更多细节。 ## 引言 今年早些时候的春天，我正在为我的函数式编程（https://hendrix-cs.github.io/csci365/）课程的学生们随意构思最后的项目想法。刚给我的离散数学学生讲完算术基本定理（http://ozark.hendrix.edu/~yorgey/forest/00EG/index.xml），我好奇是否能在 Agda（https://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.HomePage）中将其形式化——我的意思是*从头开始*形式化：当然，算术基本定理已经在 Agda 标准库（https://agda.github.io/agda-stdlib/v2.3/Data.Nat.Primality.Factorisation.html）中了。后来我才知道，它是 Nathan van Doorn 添加进标准库的，也就是 Taneb（https://github.com/Taneb）。——这可能是一个不错的项目。 所以我决定花大约一个小时在 Agda 中尝试证明它，以评估项目的难度。一小时后，我学到了两件事：(1) 证明算术基本定理对我的学生们来说*不*是一个合适的项目（他们只有几周的 Agda 练习经验）；(2) 在我自己完成证明之前，我根本停不下来！ 在接下来的一周左右，我完全从头完成了这个证明——没有使用任何标准库的内容，也没有查阅任何参考资料。我只依靠我的 Agda 经验、对非正式层面相关证明的掌握，以及我在过程中学到的 Agda 技巧（例如来自 *Conor McBride*、*Jacques Carette*、宾夕法尼亚大学的同事们以及其他地方）。 我决定发布这个证明，并附上额外的注释，希望能作为一个中级参考资料。也就是说，也许你已经学了一些基本的 Agda（如果还没有，我建议从这本教程开始（https://agda.readthedocs.io/en/latest/getting-started/a-taste-of-agda.html）），并对 Curry-Howard 对应有基本的了解，但通过看到一个完整的中等规模证明示例会有所收获。另一份不错的资料是 Jesper Cockx 的这篇博文（https://jesper.sikanda.be/posts/formalize-all-the-things.html）。最终的博文非常长，但我不为此道歉——如果你想要一篇有趣的 5 分钟阅读，那请另寻别处。 整篇博文和证明都可用作一篇文学化 Agda 文档（https://github.com/byorgey/blog/blob/main/posts/2026/06/26/FTA.lagda.md）。**更好的是，我还发布了这篇博文的另一个版本，其中几乎所有的证明都被替换成了洞（http://ozark.hendrix.edu/~yorgey/pub/FTA-holes.lagda.md）。** 为了最大程度的学习体验，我建议下载它并尝试在阅读的同时自己填写这些洞。 以下是目录。根据你的背景，你当然可以选择跳过某些部分。例如，如果你已经有很好的经验处理 Agda 中基本的自然数算术、等式和不