九章云极问鼎陶哲轩数学挑战赛，强化学习成AI4S新基建

2026年9月11日，28位菲尔兹奖得主联名发表《人工智能在数学中的严重错位》，指出AI公司把解决数学难题当作能力基准的做法对数学科学和共同体有害，认为数学研究真正追求的是概念性理解与洞察，而非批量生产对错判定。

同月底，陶哲轩联合创立的SAIR Foundation公布数学蒸馏挑战赛第二阶段成绩。294支参赛队伍中，九章云极言表实验室在全部四个赛道均获满分200分，总榜221分，大幅领先，位列唯一头名。陶哲轩反对的是“只追求答对、不关心理解”的路径，而非AI做数学本身。

该赛事聚焦等式理论中的蕴含关系，规则要求：蕴含成立须提交Lean4形式化证明，不成立须提交反例，所有提交由确定性Lean验证器检验，未通过不得分。评判标准从“答对率”改为“可验证性”。赛事设Solo和Marathon两类赛道，分别侧重单题攻坚与资源分配。主榜之外设Research Leaderboard，从约62000条法则的五阶等式中筛选最难题单独评分。仅两支队伍得分大于零，九章云极以17分断崖领先，第二名仅3分。

九章云极将比赛新结果整理成论文《Trace-Tree Magmas: Proof-Producing Infinite Countermodels and 28 New Order-Five Austin Classifications》。Austin法则指所有满足它的有限代数结构都平凡、但存在非平凡无限结构的特殊等式。论文提出“秩递减稀疏迹树magma”新构造，以有限重写规则在无限构造树上定义真正无限的代数结构，绕开有限模型搜索器局限。在ETP锁定的96个五阶候选等式中，为28个此前无公开分类的等式首次构造非平凡无限模型，建立28项新Austin分类，归于14个对偶类，一次搜索生成636份Lean4证书，全部被验证器接受。每个模型均附自包含Lean4证明，搜索与生成程序不被信任，候选结果须通过Lean内核验收才计数。

论文主要贡献者来自九章云极旗下AI4S研究机构言表实验室。九章云极是人工智能基础设施及智算云提供商。其AI首席科学家缪旭博士表示，SAIR开放理念与九章方向一致，挑战赛是切入口。他认为九章做RSI希望模型与人类知识一起进化。自动数学推理需在“搜索证明→形式化验证→反馈调整”循环中迭代，涉及大规模并行搜索、长时运行与高效调度，与强化学习训练工程挑战相似。比赛中部分Lean证明需运行长达一小时，团队对Lean系统大量优化，提升加载速度与并行能力。九章云极围绕智算云与智算操作系统构建全栈能力，持有超29000PFLOPS可控算力，率先提出DCU度量单位，实践入选工信部2025年度新型信息基础设施典型案例。

AI4S正从“加速计算”转向“参与发现”。OpenAI曾宣布产出722个数学发现，但部分结果存在错误或无法独立复核，几项因符号错误被撤回。缪旭指出，AI4S一大瓶颈是科研人员对AI推理结论的“信任赤字”。大语言模型概率性生成带来幻觉风险，科学推理中微小误差可能导致结论无效。2026年3月发布的《人工智能安全治理框架》2.0版将模型输出可靠性与可验证性纳入治理体系，要求高风险决策场景强化可追溯、可审计能力。九章云极的应对路径是神经符号验证与强化学习闭环结合。