Lean是《数学原理》的终极回响？论形式化验证的哲学分野

doodlestein · x · 2026-07-30

作者深入对比了定理证明器 Lean 与罗素、怀特海《数学原理》的渊源。指出 Lean 成功实现了《数学原理》中“数学符号化、依赖明确化、证明规则化、机器可验证”的认识论与技术理想。

然而，Lean 并未实现逻辑主义的本体论哲学：它并未证明数学对象本质上是逻辑客体，也未证明存在一个能涵盖所有数学真理的固定系统。因此，Lean 是机械验证数学的最强工具，但并非无假设的绝对真理。