新论文称 Lean 验证不能为 OpenAI 的 Navier-Stokes 自然语言证明背书
论文分析指出 Lean 编译成功不保证自然语言数学证明无误,证明消除歧义具有无穷大 SCI,并揭示 OpenAI 纳维-斯托克斯形式化存在导数阶数不符。
- Σ0_2-complete希尔伯特第十问题在多项式未知数个数 k>=9 时,存在性预设消解判定问题所属的算术层级
- l对任意层级 l>=2,多项式预设消解判定问题对应的可解性复杂度指数 SCIA(Ξ_dl)
- ∞通用消除自然语言数学歧义、实现语义忠实自动形式化所需的可解性复杂度指数 SCI
形式语言编译通过不等于自然语言证明正确,语义忠实消歧在理论上比停机问题更难。
梳理了语义哲学、SCI 复杂度与丢番图方程理论,并评述了近期工业界的大规模形式化实践。
建立两类形式化任务区分,证明语义忠实消歧为 SCI=∞ 难题,揭示编译反馈循环导致的语义漂移。
通过 OpenAI 纳维-斯托克斯证明、ChatGPT-6 交互及 Meta 实践,揭示了阶数不符与证明替换等实际脱节。
作者指出未详审欧拉方程且设计可信系统超范围;实验仅深入剖析少数案例且未提供统计基准。
论文论证了形式化编译不保证原证明正确,确立了消歧不可计算性理论,并揭示了 OpenAI 爆破证明中的具体脱节。