结论先行**数学能力特别是前沿问题的解决能力不是解应用题而是形式化验证。**国产模型数学能力不足核心原因不是代码能力差而是没有在Lean形式化证明方向上进行足够的特化训练。这个判断有数据支撑而且能解释一个看似矛盾的现象——国产模型在竞赛数学和代码生成上表现不错却在研究级数学证明上乏善可陈。先界定“数学能力”指什么如果“数学能力”指的是K-12竞赛题的求解国产模型并没有那么不堪。Qwen3-Max-Thinking在AIME 25和HMMT 25上拿到了国内首个双满分Qwen3-VL-235B-A22B-T在涵盖JMC、AMC8、JMO、IMO等竞赛的1230道题目上取得了68.81%的最高分并在六个竞赛中拿到最佳成绩。但前沿数学问题——那些尚未被证明的猜想、需要构造全新证明路径的定理——完全是另一回事。2026年陶哲轩公开表示自己“已经放弃实时跟进所有新证明”AI生成证明的速度已经远超人类消化能力数学正在从“证明稀缺时代”进入“证明过剩时代”。真正的瓶颈已经从“如何生成证明”转移到“如何验证与理解证明”。而目前唯一成熟到可以在研究级别使用的自动验证工具就是Lean及其数学库Mathlib。ArXivLean基准测试的41道研究级题目全部来自2026年3月的最新arXiv论文结果所有模型——包括最强的闭源模型和专门的Lean agent——得分都低于20%。这个数字说明的不是“AI数学不行”而是“AI在形式化框架下解决前沿数学的能力刚刚起步”。代码能力不是瓶颈2026年5月全球权威三方编程榜单Code Arena放榜阿里Qwen3.7-Max以1541分超越GPT-5.5、Gemini-3.5-Flash仅次于Claude系列在大模型厂商中排名全球第二成为唯一突破1540分大关的国产大模型。这个榜单的特点是不考孤立的算法题而是由开发者出题、模型从零生成完整的可交互Web应用再由全球开发者盲测投票。这比传统benchmark更接近真实工程场景。DeepSeek在代码领域同样是第一梯队。SuperCLUE的代码生成项目中国产头部模型与海外头部模型的差距不到2分。代码能力不是国产模型的短板。代码能力确实能转化为实际任务能力两个案例可以说明这一点。网络安全。2026年9月底至10月初一名被CrowdStrike认定为中文使用者的攻击者使用中国开发的开源AI渗透测试工具ARTEX配合DeepSeek v4.1-flash主力模型和GLM-5.3攻破了韩国多家金融机构的系统包括Hana Bank、KB Kookmin Bank和Shinhan Bank被攻入的系统涉及银行的贷款查询服务和员工移动办公支持系统。CrowdStrike在报告中明确指出攻击者“主要使用了DeepSeek v4.1-flash辅以GLM-5.3”。这个案例的关键不在于“模型被用于非法用途”而在于它证明了国产模型的代码生成能力足以支撑复杂的多步骤攻击链从漏洞识别到工具编排到命令生成整个流程需要模型具备可靠的代码理解和生成能力并且能够在迭代反馈中修正错误。这本质上就是“代码生成搜索反馈循环”在攻击场景下的应用。量化。广发证券的研报使用DeepSeek-v4-pro和Qwen3-VL-235B构建了全自动因子挖掘系统框架是一个“生成-评估-进化”的迭代循环模型生成因子代码后自动评估IC、RankIC等指标并将反馈注入下一轮生成全流程无需人工介入。实证结果在沪深全市场以10个交易日为换仓周期DeepSeek-v4-pro生成的因子IC均值为2.15%Qwen3-VL-235B为2.95%。对于A股市场的多因子选股策略2%-3%的IC均值是有实际价值的水平。这直接说明代码生成和搜索反馈循环在国产模型上是有效的。问题出在Lean特化的缺失既然代码能力不弱代码能力也能转化为实际任务能力为什么数学证明不行Lean形式化证明和普通代码生成之间的差异比看起来要大得多。自然语言推理允许启发式跳跃和隐含假设而Lean证明要求每一步都被编译器验证不允许任何省略。一个微小的语法错误或逻辑缺口就会导致整段证明被拒绝。这种刚性反馈机制对训练数据的质量和格式提出了远比普通代码训练更严格的要求。国内在Lean训练数据上的积累确实薄弱。Lean-zh社区虽然存在但规模有限。北大、人大、中科院等机构有研究者在使用Lean国家天元数学中心和上海交大也举办了Lean4的暑期学校和培训班但这些活动的定位是“推广”和“入门”目标是让更多人知道Lean是什么而不是产出大规模的Lean训练数据。有一个值得注意的反面证据DeepSeek其实已经发布过专门的形式化证明模型DeepSeek-Prover-V2-671B在MiniF2F-test上达到了88.9%的通过率Pass8192解决PutnamBench 49/658题性能在神经定理证明领域属于state-of-the-art。这说明技术路径是通的能力是存在的。但Prover-V2的定位是一个专门的定理证明模型而不是将形式化证明能力集成到通用旗舰模型中的系统性特化。MiniF2F上的高分并不直接转化为ArXivLean所测量的研究级证明能力——前者是竞赛级别的形式化后者需要从论文摘要中提取并形式化从未被形式化过的深层数学陈述一道题可能需要数千行Lean代码。国内学术圈已经在有意识地推动定理证明的人才培养。CCF形式化方法专委会主办了定理证明竞赛浙江大学和上海交通大学联合承办深圳河套学院的博士生赵雨扬自2021年起为mathlib贡献了数百个Pull Request。但这些努力仍处于“点状突破”阶段远未形成足以支撑大模型系统性微调的数据规模和工程化能力。参考链接[1] 陶哲轩千年数学规则被AI按下重启键陶哲轩千年数学规则被AI按下重启键_澎湃号·湃客_澎湃新闻-The Paper[2] ArXivLean: How Well Can LLMs Formally Prove Research Math?MathArena.ai[3] 刚刚中国AI闯入全球编程前二仅次Claude刚刚中国AI闯入全球编程前二仅次Claude[4] Chinese-speaking hacker possibly linked to AI-driven attacks on S. Korean banks: report (Yonhap News Agency)Chinese-speaking hacker possibly linked to AI-driven attacks on S. Korean banks: report | Yonhap News Agency[5] 量化投资专题大语言模型投研应用构建全自动的因子挖掘AI智能体广发证券A股-研报详情[6] DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositionhttps://ar5iv.labs.arxiv.org/html/2504.21801[7] 上海交通大学“AI4MathLean4与数学形式化 大模型智能体辅助数学”暑期学校回顾上海交通大学数学科学学院[8] 学子风采 | SLAI博士生赵雨扬斩获CCF首届定理证明竞赛亚军https://www.slai.edu.cn/article/301[9] 阿里千问模型Qwen3-Max-Thinking正式发布https://www.chinaz.com/2026/0127/1735327.shtml[10] 中外AI对决 国产三强只能争夺全球第五SuperCLUE评测https://post.smzdm.com/p/av7z0kzp/[11] Can AI Win Gold? Assessing AI Math LLMs in K-12 International Competitions (ACM)https://dl.acm.org/doi/10.1145/3705016.3705052[12] TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertshttps://ar5iv.labs.arxiv.org/html/2407.03203[13] 陶哲轩在害怕什么深度解析顶尖数学家陶哲轩的内心世界与担忧36氪_让一部分人先看到未来