发生了什么
9 月 18 日,菲尔兹奖得主、加州大学洛杉矶分校教授陶哲轩在其个人博客上代表 SAIR 基金会(科学与人工智能研究基金会)宣布,正式启动「开放数学模型计划」(Open Math Model Initiative)。该计划的目标是联合数学界、科研机构与产业伙伴,为数学及基础科学研究构建开放权重模型与配套开源工具链,使研究者能够按任务调用开源或闭源大语言模型。计划即日起征集在资金、算力、专业经验与社区建设方面的合作伙伴,首批伙伴名单与模型细节尚未公布。
- 首阶段场景:理解艰深论证、核对文献、探索示例与反例、编写代码,以及把自然语言证明形式化为 Lean 4 可检查的代码
- 开放原则:开放许可的权重与代码、公开训练方法、可复现评测,并在发布时同步报告失败与局限
- 数据原则:数学共同体拥有研究数据并决定其使用方式,未经研究者明确同意、未事先约定用途的数据不进入训练集
- 许可与治理:联合成果拟采用 Apache 2.0、MIT 或 CC BY 4.0 等许可;治理规则与决策公开,成员可参与决策并对负责人问责
为什么重要
这项计划的直接背景是学界与商业实验室之间的张力。9 月 11 日,包括陶哲轩、邓煜在内的 25 位菲尔兹奖得主联合发布题为《数学领域中人工智能的严重错位》的声明,指出把「解决著名未解问题」当作模型能力基准的做法,可能把数学研究原本重视的理解、解释、知识积累与学术协作排挤在外。陶哲轩在同期演讲中把这一现象概括为「证明消化不良」:证明的生成与验证正被 AI 以远超「消化」环节的速度自动化,而消化意味着理解证明为何成立、连接已有文献、提取可迁移思想。
对科研机构与企业研究部门更有参考价值的,是评价口径的调整。该计划明确不以榜单正确率作为唯一标准,而重点考察三项指标:辅助科研时是否足够可靠、输出能否留下可重复且可检查的验证过程、长期使用成本能否被普通大学和研究机构承担。这一取向与当前商业模型「以解题数量证明能力」的叙事形成对照,也把「可用、可查、用得起」推回到模型评价的中心位置。
现实约束
- 算力缺口:非营利机构难以长期复制大型实验室的 GPU 规模与推理投入
- 数据成本:高质量数学数据的整理、形式化、版权处理与人工校验需要大量专业工作
- 待公布事项:预算、模型规模、架构、训练时间表与首批合作机构均未确定;可观察指标是半年内能否放出首个可下载的检查点

