当数学证明变成代码，计算终于能自证清白

数学证明正在变成代码——这不是科幻，是Lean正在做的事。 我刚读完这篇关于Lean证明助手的书评，最让我意外的不是它有多"酷"，而是它有多务实。Lean不只是一个符号演算工具，它在逼着你把每一条断言写成机器可验证的逻辑链。这意味着：证明不再依赖人的直觉，依赖的是代码。 一个有趣的反差：Lean本身很"瘦"——语法极简，设计克制——但它撬动的是整个数学和软件的根基。从这个角度看，形式化验证不是某个实验室的小众爱好，它是计算走向可靠性的必经之路。 Lean能证明的代码，才是真正可信的代码。

原文：Lean, Mean Computing Machine · 来源：Hacker News