OpenAI在纳维-斯托克斯方程证明中把数学错误地翻译成了代码

📋总体概括

据New Scientist报道，OpenAI在声称其AI模型完成纳维-斯托克斯方程证明相关形式化工作时，被发现将数学翻译成代码时出现错误，导致所声称的证明结论站不住脚。这一事件揭示了当前AI数学证明能力的边界：形式化验证本应是防错手段，但前提是数学到代码的翻译本身必须准确。该报道引发社区对AI声称攻克重大数学难题时验证流程是否严谨的讨论，也为被炒作的『AI攻克千禧年难题』叙事泼了一盆冷水。