剑桥数学家指控 OpenAI 的 Navier–Stokes 证明在转写成 Lean 代码时出现偏差

剑桥大学数学家 Anders Hansen 等人在向《新科学家》陈述中表示，OpenAI 为其 Navier–Stokes 问题证明提供的 Lean 代码与自然语言版本在 Lemma 8.6 处不一致：自然语言版本要求某值小于 m+4，Lean 版本中对应条件放宽为小于 m+5，这在数学上更弱。