这周 Lean 圈子算是彻底炸了，三天三件事，观望了很久的朋友，我觉得有必要把话说明白：现在到底值不值得入坑，以及怎么入最不亏。
先说这周发生了什么。
8月15日，森多夫猜想（Sendov’s Conjecture）被 AI、Lech Mazur 和陶哲轩联手攻破，知乎相关问题浏览量直接冲到120万+。有意思的是评论区：已经有人说自己搭好了数学证明专用 harness，本地装好了 Lean，“就差一个所有数学猜想的 list 了”——普通人开始认真琢磨自己上手证猜想了。知乎
8月16日，Lean 创造者 Leonardo de Moura 的最新播客访谈整理稿流出。他同时在 AWS 当高级首席应用科学家、是 Lean 背后非营利组织 LeanFRO 的首席架构师。他在访谈里说的一句原话流传很广——他已经不再写测试了，他写性质，然后 AI 替他证明。知乎
8月17日，Humanfia 团队登顶 Lean 官方 AI 定理证明排行榜 Lean-Eval，解出166道题，领先第二名整整10题，而且 token 总花费不到50k。知乎
Lean-Eval 里面是什么级别的题目？Green–Tao 定理、Feit–Thompson 奇数阶定理、Brouwer 不动点定理——以前研究生课程级别的大命题，现在 AI 成批地啃。知乎
这次火，跟以前有什么不一样
Lean 不是新东西，它既是一门编程语言，也是证明助手：你在里面写数学证明，Lean 替你逐行检查，通过了就意味着结论在数学上成立，没有模糊地带。它之前一直小众，原因就一个字：贵。
贵到什么程度？早期标杆项目 seL4，一个完全验证过的微内核，只有约8700行 C 代码，验证花了约20人年，折算下来每行代码的验证成本约350美元。知乎所以 AWS 用了十年形式化验证，也只敢用在最关键的安全组件上。
现在这个等式被 AI 改写了。de Moura 的同事 Kim Morrison 用大约一周时间，让 AI 把 C 语言压缩库 zlib 翻译进 Lean 并完成验证：1100多条定理、约32000行证明代码，没有一个未完成的占位符。知乎数学这边的进度更直观：2024年 DeepMind 的 AlphaProof 用 Lean 拿了 IMO 银牌，当时整个社区觉得已经了不起；2025年已经有系统做到金牌水平；今年 Humanfia 团队宣称在 IMO 2026 拿下满分。知乎de Moura 的原话是：几年前认为拿金牌不可能，“现在大家把它当作简单问题的基准”。
最反常识的一点是：AI 解决的不是"第一次证明"的成本，而是"维护证明"的痛苦。程序一改，证明就可能跟着崩，过去修证明比修测试还难。de Moura 说 AI 在这个环节表现极好，他前一天的经历是：让 AI 重写一批自己都没读过、不知道讲什么的证明，“AI 瞬间给出了新版本”。他还有个说法我印象很深：“我曾以为我的超能力是能忍受很多痛苦。这个超能力现在不重要了。”
对了，还有个彩蛋：Lean 的 tactic 模式每写一步，右侧面板立刻刷新剩余目标，把目标清零就算赢。有用户跟 de Moura 说：“你给我造了我最喜欢的电脑游戏。”
值不值得入坑，分人
如果你是程序员，想对本职工作有用：实话实说，Lean 离日常开发还有距离，工业落地目前集中在最关键的安全组件。但趋势值得盯：Rust 代码已有 Aeneas 这类工具映射到 Lean 做验证，蚂蚁技术研究院今年也开出了 Lean 形式化验证方向的校招岗。微博现在学，买的是三五年后的窗口期，不是下个月的产出。
如果你是数学爱好者或 AI 从业者：这是目前最值得入坑的人群。门槛从来没有这么低过——浏览器里就能玩自然数游戏，AI 工具链成熟了，跟着 agent 工作流，普通人真能去摸"前沿数学"的边。本周那个"自己搭 harness 准备证猜想"的评论区氛围，就是这批人的真实状态。
如果你纯为找工作：冷静。岗位真实存在但还很窄，集中在头部机构的形式化方向，把它当求职跳板风险太大，当兴趣加分项正好。
最省时间的入门路径
结合社区里踩完坑的人的经验，路线可以压缩成这样：
第一步，别装环境，先玩 Natural Number Game（自然数游戏）的 Lean 4 网页版。用皮亚诺公理从加法乘法一路证过去，两三个小时就能体验到"证明归零"的游戏感，零安装成本，筛掉一半三分钟热度。知乎
第二步，确认上头了再装本地环境：elan 管理工具链 + VS Code 插件。这一步是社区公认的劝退点，B站上"代码小白的 lean4 环境安装"这类教程播放量都不低，卡住别硬刚，跟着教程走。
第三步，中文资源现在是真齐了：Lean-zh 项目组翻译的《逻辑验证漫游指南》2026中文版今年6月刚上线（源自阿姆斯特丹自由大学的 LoVe 课程），官方教程《Lean 4 定理证明》也有中文文档，入口统一在 Lean 中文文档站。知乎
第四步，进阶就去啃 Mathlib。提前打预防针：知乎上过来人的共识是，写 Lean 证简单逻辑命题不难，难的是面对 Mathlib 这种庞大数学库时的一脸懵，对数学底子有硬性要求。知乎
最后泼一点冷水
Lean 验证的是"推导过程是否符合定义"，但形式化代码是否准确表达了你的原意，这一步还是人的责任——这是社区里"Lean 是最后的人类堡垒"讨论的核心。知乎另外学习曲线陡峭、编译吃机器、英文一手资料为主，这些都是真实成本。
接下来值得持续盯的信号：Lean-Eval 排行榜的更替速度、LeanFRO 的路线图更新、以及中文文档的翻译进度。这三个指标任何一个加速，都说明这个坑还值得继续往下挖。
