OpenAI 宣称攻克杨-米尔斯存在性问题却不公开 Lean 文件引发争议

OpenAI 宣称攻克千禧年难题「杨-米尔斯存在性」，但未公开 Lean 形式化证明文件，引发数学界质疑。数学家 Elliot Glazer 指出，社区既无法取得证明文件，也难以从外部判断具体证明了什么；teortaxesTex 则讽刺称，Lean 证明像思维链一样被隐藏，证明属于 OpenAI 的知识产权。