书生大模型数学证明

围绕书生大模型被传攻克三十年数学难题，文章梳理AI数学证明的真实进展：数学因可自动验证成为推理试金石，AlphaGeometry、AlphaProof、Lean等推动形式化与奥赛突破，中国团队在书生、DeepSeek-Math、Qwen-Math等模型上持续投入。但数学界对“解决”有严格判定，大模型更多承担提出路径、组合结论与辅助验证，陶哲轩称其约等于不称职但不算无能的研究生。真正变化在科研流程：AlphaEvolve改进开放问题上界，模型降低试错成本，教育转向提问与Lean证明。文章提醒别急着宣布革命，累积效率提升或许比单次突破更有分量。