在Agda中证明算术基本定理

- 本文用Agda（一种依赖类型的函数式编程语言，也是定理证明器）来证明算术基本定理——即每个大于1的自然数都可以唯一地分解为质数的乘积。 - Agda基于Martin-Löf类型论，允许将数学命题直接写为类型，证明则是满足该类型的程序。这类工作属于“形式化验证”领域，即用计算机检查数学证明的每一步是否严格正确。 - 算术基本定理看似简单，但用形式化方法完全证明需要处理质数定义、整除性、存在性（每个数都能分解）和唯一性（分解方式唯一）等多个层面的细节。 - 这类形式化工作通常用Coq、Isabelle/HOL或Lean等系统完成；Agda方案相对少见。读者若不了解依赖类型，可将Agda理解为一种让数学证明可被机器自动检查的编程语言。