形式验证专家警告：Lean 证明不等于代码正确

形式验证专家 Grigore Rosu 对 AI 圈提出批评，指出这个始于 1960 年代的计算机科学老领域正被热门新方向反复"重新发现"，此前是区块链，如今是 AI。他特别警告拥抱"用 Lean 证明即正确"理念的新一代 AI 计算机科学家：脱离程序语言的形式语义，根本无法定义"正确性"，即所谓"垃圾语义进，垃圾验证出"。

2026-09-20 ~ 2026-09-20 · 2 条相关

• 形式验证老兵批 AI 圈:垃圾语义进,垃圾验证出 — tianyin_xu · 2026-09-20
• 形式化验证大佬泼冷水:没有形式语义,Lean 证明≠代码正确 — JiaweiLiu_ · 2026-09-20