新论文：数学证明过 Lean 检查不代表原证明正确，忠实翻译不可判定
rohanpaul_ai · x · 2026-10-08
一篇新论文指出，AI 把数学证明翻译成 Lean 形式化语言时，通过 Lean 检查并不能说明原证明是对的。
- 作者展示了一个案例：聊天模型把一个错误的证明「悄悄修正」后翻译成合法的 Lean 证明，Lean 校验照样通过——即翻译过程中可以静默改变数学内容。
- 理论上更强：判断一个陈述能否被忠实翻译，被证明比停机问题还难，因此不存在永远可靠的形式化翻译器。
这对当下「Lean certificate 证明 AI 数学结果」的验证热潮是个重要警示：证书通过 ≠ 原命题成立。
所属事件:剑桥论文质疑 Lean 验证可信度，直指 OpenAI Navier-Stokes 证明(14 条相关)→
「研究」频道最新
- Cyber Index 方法论详解：三套基准合成，Grok 4.7 与 MiMo-V2.6-Pro 公开版并列 56 分 — ArtificialAnlys · 2026-10-09
- LightOnOCR-3 训练秘辛：用 OCR 参考文本引导逻辑分块 — IgorCarron · 2026-10-09
- LightOnOCR-3 揭示：单一版面模型无法覆盖全部文档类型 — IgorCarron · 2026-10-09
- Text2Sim 用文本生成物理仿真场景，输出可编辑的真物理视频 — erwincoumans · 2026-10-09
- 单张图像重建 3D 场景:Building Rome 项目可见范围外几何也补全 — jonstephens85 · 2026-10-09
- PredActor 用单一扩散策略统一人形机器人运动生成与控制,G1 端侧跑 50Hz — carlosdponx · 2026-10-09