nonmathAI 与形式化数学 [AI4FP]

2026-01-24

这一周我参加了求真书院组织的 “AI与形式化数学” 冬令营, 学写 Lean, 思考形式化数学的未来.

虽然 LLM (大语言模型) 不一定是 AI 的最终答案, 但形式化数学工具的出现, 使得我们不得不面对这样一个未来: 随着被形式化的命题与证明构成的工具库的增长, LLM 的数学能力将会稳步上升, 成为数学家的有力合作者或竞争对手. 所以, 至少了解这位潜在的合作者或竞争对手, 成为了我学习 Lean 的动机.

经过简单的调研, 我发现不出所料, Lean 对于范畴论的实现完全停留在严格 $1$-范畴的层面, 对于高阶范畴没有丝毫推广的潜力. 恐怕本质的原因是 Lean 的一个等式的任何两个证明都相等, 换言之等式类型仅仅是 $(-1)$-截断的 “命题”; 这让我相信它不可能在现代数学的许多分支 (如导出代数几何) 中发挥作用.