Lean验证通过不等于证明是对的。剑桥和伦敦国王学院的三位数学家10月6日在arXiv发文逐条对照：OpenAI论文里一个引理说4阶导数就够，配套Lean代码用的却是5阶。 最扎心的是：出错的不是证明本身，是AI做自动形式化时的翻译环节。AI生成证明、AI翻译成Lean、机器验证，全链路AI，中间错一环就全错。

🌐 链接: https://x.com/taiyanghere/status/2108200071753798126
🏷️ 分组: X｜正在关注
🕒 时间: 2026-10-08 22:17:20
X (formerly Twitter)
太阳 (@taiyanghere) on X
Lean验证通过不等于证明是对的。剑桥和伦敦国王学院的三位数学家10月6日在arXiv发文逐条对照：OpenAI论文里一个引理说4阶导数就够，配套Lean代码用的却是5阶。

最扎心的是：出错的不是证明本身，是AI做自动形式化时的翻译环节。AI生成证明、AI翻译成Lean、机器验证，全链路AI，中间错一环就全错。