专家警示:Lean 仅能验证代码编译,无法保证数学命题正确

AlexKontorovich · x · 2026-08-02

针对“Lean 能自动验证数学证明”的观点，数学家 Alex Kontorovich 在 ICM 演讲中指出：Lean 的作用仅限于验证代码能否成功编译（假设内核无 Bug），从而确保给定的命题（包括定义本身）存在正确的证明。然而，它无法判断这些形式化命题是否与人类自然语言想要表达的数学直觉完全一致。这并非计算机能解决的问题，最终仍需依赖容易出错的 LLM 或人类来进行判断。