机器可检查的证明：Lean 形式化验证入门，及其对智能体系统的启示

近期，一批由 AI 生成的数学研究手稿被公开，数量超过 700 篇。其中约 42% 的顶层结果配有 Lean 形式化证明（公开材料自述），另有三篇因符号错误被撤回。这件事对工程师的价值不在数学内容，而在一个具体问题：当智能体批量产出结果时，“正确与否”由谁、用什么方式来判定。本文介绍 Lean 的基本用法、它能保证的和不能保证的，以及可迁移到智能体系统的做法。