OpenAI 声称证明杨-米尔斯难题却不公开 Lean 文件，引 community 吐槽

teortaxesTex · x · 2026-11-01

围绕 OpenAI 宣称攻克千禧年难题「杨-米尔斯存在性」但隐藏 Lean 形式化证明文件的争议发酵。数学家 Elliot Glazer 吐槽：我们没有 Yang-Mills 的 Lean 文件，有的只是一家公司声称「这个文件存在」——而且这是唯一一个从外部连他们到底证明了什么都看不出来的高调公开结果。

teortaxesTex 讽刺道：Lean 证明很快就像思维链一样被隐藏了，「你付费买的是服务，证明是 OpenAI 的 IP」——讽刺厂商以商业机密为由不给社区可验证的证明材料。