Mathematics Just Changed Forever — Kevin Hartnett

Lean 由 Leo de Moura 独自开发，靠 Mathlib 社区众包，已能形式化 Peter Scholze 的前沿数学“完美域空间”。

数学家过去靠同行评议来判断定理对错，但面对几千页的计算机证明，这套方法已经撑不住。Lean 这类“形式化证明助手”让最前沿的抽象数学也能变成机器能查的代码。你会看到：Lean 如何从微软工程师的个人项目，变成数学家信任的工具；Mathlib 社区如何像开源软件一样众包构建庞大的数学库；以及形式化证明如何让数学协作和信任方式彻底变样。

数学家以前靠经验和抽查判断证明对错，但几千页的计算机证明让这套办法彻底失效。

• Kepler 猜想的证明：Thomas Hales 用 1767 个独立程序验证球堆积密度，论文投到 Annals of Mathematics 后，编辑和审稿人根本无法完整复查，最后只能“99% 确信”地发表。
• 同行评议的极限：传统做法是只查关键步骤，靠对作者的信任和经验判断，但超大规模证明让这种“社会性信任”变得脆弱。
• Lean 让机器能查对错：用 Lean 这类工具，证明过程变成机器可查的“证书”，即使是陌生人协作也能信任结果，不再全靠人肉检查。

Lean 最初只是微软研究员 Leo de Moura 的个人工程，后来被数学家社区“抢走”，变成了形式化数学的主力工具。

• Lean 的底层机制：Lean 是个编程语言+证明助手，底层有个极小的“内核”专门校验逻辑对错，其他 bug 不影响最终结论。内核越小，可信度越高。
• Mathlib 众包模式：Lean 的数学库 Mathlib，靠全球志愿者众包，从高中数学到前沿理论都能逐步形式化。每个新定义和定理都像开源代码一样“拉请求”，逐步完善。
• 社区带动成长：Kevin Buzzard 等数学家带学生、拉同事一起“教 Lean 学数学”，最初连复数都没有，几年后已能覆盖本科和部分研究生课程。

Lean 和 Mathlib 不只是做“老数学”，已经能形式化 Peter Scholze 的“完美域空间”等极前沿对象，证明机器形式化已能跟上顶级数学创新。

• 形式化“完美域空间”：Buzzard、Massot、Commelin 等人用 Lean 形式化了 Scholze 的前沿理论，向业界证明 Lean 能覆盖最难的现代数学。
• 定义先于证明：最难的不是翻译 100 页证明，而是先把新概念和定理的“定义”写进机器语言，消除人类论文里常见的歧义和遗漏。

“Lean 不只是验证对错，更是让陌生人也能协作、信任彼此的数学成果。”

• 做新理论或复杂系统设计时，先用“形式化定义”把核心概念写清楚，比直接写长篇证明更容易发现歧义和漏洞。
• 协作大项目时，可以学 Mathlib 的众包模式，把任务拆成可验证的小模块，让不同水平的人都能安全贡献。