数学家 Gerard Sans 驳斥 AI 解题成果：核心在专家与 Lean，AI 什么都没懂

数学家 Gerard Sans 质疑 AI 攻克数学问题的报道，指出核心成果来自专家撰写形式化证明并全程引导，以及 Lean 形式化验证。去掉专家护航或 Lean 后，AI 就会失败；即使证明通过 Lean 验证，AI 仍无法解释其为何成立。