北大董彬谈AI与数学未来,安德森猜想被证伪,数学家应回归提出新问题的初心
北京大学董彬教授指出,AI正深刻改变数学研究范式。其团队研发的Rethlas-Archon系统在无人干预下否定了悬置十余年的安德森猜想,并完成近两万行Lean 4形式化验证。他认为焦虑是暂时的,关键转...
2026年4月,一个由北京大学数学团队主导的AI系统Rethlas-Archon完成了一项令数学界震动的任务:在完全无人类参与的条件下,通过构造反例否定了交换代数中悬置十余年的安德森猜想(Anderson Conjecture),并用近两万行Lean 4代码完成了形式化验证。该成果获《Nature》专题报道,标志着AI在纯数学证明领域已从辅助工具迈向独立探索者角色。
这项工作由北京大学北京国际数学研究中心博雅特聘教授董彬牵头,联合刘若川、肖梁、文再文等学者组建的AI4MATH团队完成。董彬是国内较早系统性探索AI与数学交叉的学者之一——2016年他从计算成像转向深度学习,2023年进一步聚焦大语言模型,提出“数学智能副驾驶”构想。此次成果正是该理念的实践落地。
在近期“2026未来科学·创想季”跨界对话中,董彬坦言,OpenAI一次性公开722篇数学手稿后,全球数学家纷纷自查“受灾程度”:“有些领域可能是‘重灾区’,大家原以为还需数十年才能推进的问题突然有了结果——按照一些同行的说法,基本上被AI‘干没了’。”他同时强调,已有3篇手稿因错误被撤回,说明当前成果仍需严格核验;且多数进展仍基于现有工具向前推进,尚未触及真正颠覆性突破。
但董彬判断,真正的转折点发生在2025年下半年至2026年初:头部模型识别自身推理瑕疵的能力已超过高年级博士生,部分系统甚至能实现“自我迭代”——自行推理、检查、筛选可靠路径,形成闭环增强。这一能力跃升使AI得以处理更复杂的逻辑链条,为解决如准黎曼猜想等高难度问题提供了技术基础。
值得注意的是,数学界对AI的反馈并非全然乐观。多位资深数学家曾公开表达担忧:当长期投入数年乃至数十年的问题被AI快速攻克,研究者的成就感与职业价值将如何安放?董彬承认焦虑真实存在,但他认为这是变革期的必然阵痛。“数学是一个非常开放的体系,重要问题被解决后,会解锁更多新问题,带来更多可能性。”他以微积分诞生类比当前阶段——牛顿与莱布尼茨的突破并未终结数学,反而催生了微分几何、泛函分析等现代分支。
在能力分工上,董彬提出三层认知模型:知识覆盖、推理组织、假设提出。AI在第一层已全面超越人类;第二层推理能力持续提升,但在需要创造新工具时仍有局限;第三层即“提出值得研究的问题”,依赖数学家的直觉与品位——这正是当前AI最薄弱的环节。“优秀数学家的品味,体现在判断哪些问题能打开新空间、哪些方向值得深耕。目前我尚未看到AI展现出这种能力。”
因此,他主张数学家应回归初心:数学本质上是一种语言,而语言的核心价值在于创造新词汇、新表达、新语法。“我们应更重视提出新问题、新概念和构建新理论体系。”这不仅是应对AI挑战的策略,也是数学本源使命的重申。历史上,希尔伯特23个问题、庞加莱猜想等影响深远的贡献,往往源于问题本身的提出而非解答过程。
董彬进一步指出,当前学术生态确实在一定程度上偏离了这一初心。评价体系过度聚焦于“解题”与“证明猜想”,导致年轻学者倾向于选择可预期、易出成果的路径,而非冒险探索边界问题。AI的介入反而可能倒逼反思:当常规证明可被自动化,研究的价值重心自然向更高阶的认知活动迁移。
在产学研协作层面,他建议明确分工:高校负责提供高质量训练数据、设计具有挑战性的评测基准(如开放问题集)、开展基础理论研究;企业则侧重模型训练、工程优化与规模化部署。这种模式类似实验科学中的成果转化路径——高校探索原理,企业推动落地。
此外,董彬强调数学教育亟需调整。一方面要让学生掌握使用AI工具的能力;另一方面必须警惕过度依赖导致认知能力退化。“数学并非‘美而无用’”,他呼吁加强数学与物理、生物、计算机等学科的交叉融合,培养能为千行百业提供高价值训练数据的“硅基智能”支持者。
同期,浙江大学励建书院士与之江实验室王坚院士在第六届智能计算创新论坛上的对话也呼应了这一观点。励建书将当下比作“微积分诞生前夕”,认为AI有望帮助数学家跨越长期瓶颈,进而发现更广阔的数学世界;王坚则补充,数学与AI的结合不仅改变数学研究,也可能反向推动AI推理能力进入新阶段。
值得关注的是,尽管OpenAI等机构成果引发广泛关注,董彬特别提醒:科学进步不能依赖单一公司模型。未来的“科学AI”需开源、可验证、多路径竞争,方能保障数学等基础学科的健康发展。
目前,AI4MATH团队正将Rethlas-Archon扩展至更多代数与数论领域,并探索人机协同的新工作流——数学家设定目标与约束条件,AI生成候选路径,双方共同迭代优化。这种模式已在初步测试中显著缩短问题求解周期。
可以预见,随着形式化验证工具(如Lean、Coq)与大模型推理能力的持续融合,数学研究将进入一个效率与深度并重的新阶段。而人类数学家的角色,或将从“证明执行者”转向“问题策展人”与“理论架构师”。正如董彬所言:“这不是AI取代数学家的时代,而是数学家借助AI抵达新边疆的时代。”
