数学还能学吗？北大董彬与 AI 时代的无尽前沿——甲小姐对话反写

阅读目标：在国际 AI for Math 的真实坐标系里（AlphaProof / AlphaGeometry / AlphaEvolve、Axiom、Lean），读懂董彬这段访谈抛出的"无尽前沿"——国内"AI 自主证明"站在哪、数学家会不会沦为"鉴赏家"、以及机器能自证猜想的年代普通人还要不要学数学。

2026 年 7 月 1 日，B 站"甲子光年官方账号"上传了一段 2 小时 16 分钟的访谈。对谈人是北大北京国际数学研究中心的董彬——他另一个身份是北京中关村学院常务副院长，研究方向这两年越来越聚焦在 AI for Math。视频 desc 里有一行很硬的话：他的团队用"自主构建的自动化 AI 框架"证明了"安德森猜想"，并称这是"国内首次实现 AI 自主解决数学开放问题，并实现了大规模形式化验证"。

同一周，地球另一边发生的事更值得放在一起看：加州帕罗奥图的 Axiom Math 刚把第 12 篇论文挂出来，作者是 Bernhard Heim、Ken Ono 和 Axiom 三方；而 DeepMind 的 AlphaEvolve 一年前就宣布在 50 多个开放数学问题上跑了它的编码 agent。一个国内的数学家、一家美国的初创公司、一个英国的研究实验室，三拨人在 2026 年的夏天同时往同一个方向使劲——让机器不靠人类手把手，自己把一个开放数学猜想从"提出"走到"可被独立验证的证明"。

这篇文章要拆的就是这件事：董彬视频抛出的"无尽前沿"到底有多远，国内的工作在国际坐标系里站在哪，以及一个更私人的问题——在一个机器能自主证明数学猜想的夏天，普通人还要不要学数学。

方法论说明（先看这段再读下文）

这段视频在 B 站明确标注"暂无字幕"，字幕 API 返回空轨，搜狗微信 / Google / Bing / arXiv 都没有对应的公开文字稿。所以我没有看过这段访谈的完整内容，这不是逐字反写，而是基于官方 desc（视频简介）的二手重构——董彬的具体观点、金句、案例都不会在文中出现，避免在缺字幕的情况下编造内容。

desc 里能确定的事实只有这些：访谈嘉宾是董彬（北京大学北京国际数学研究中心博雅特聘教授、北京中关村学院常务副院长），研究方向是 AI for Math；团队用"自主构建的自动化 AI 框架"证明了"安德森猜想"，desc 称这是"国内首次实现 AI 自主解决数学开放问题，并实现了大规模形式化验证"；董彬的反差背景是 1999 年入北大数学科学学院（“误入”、基础班 60 人 GPA 倒数第二 2.7/4.0）；访谈还涉及期刊体系、千位数学家签署宣言反对 AI、数学家会否沦为"鉴赏家"、高考志愿这四个延伸话题。

既然只有骨架，血肉从哪里来？我的策略是用国际 AI for Math 的硬进展搭一个对照系——DeepMind 的 AlphaProof（IMO 银牌）/ AlphaGeometry（IMO 几何 25/30 题）/ AlphaEvolve（50+ 开放问题）/ FunSearch（首次 LLM 在开放问题上发现新结果）；Axiom Math 的 12 篇顶刊论文 / Ken Ono 离开 UVA 加入工业界 / Lean 4 形式化 20 万级定理。这些 2024–2026 年间发生的真实事件，为视频里的"无尽前沿"提供了一份能被独立查阅的参考地图。如果你看过视频，欢迎在评论区指正我写偏的地方。

总览：AI for Math 在 2026 年的位置

在展开董彬这条线之前，先用一张表把 2023 年到 2026 年夏天 AI for Math 的关键节点串起来。你可以把它当成全文目录。

这张表里值得盯的不是"AI 又攻克了什么题"，而是判决者是不是独立于生成者。FunSearch 把 LLM 当函数生成器，验证交给外部 evaluator；Axiom 把整家公司压在 Lean 上，每一步推理都要被 Lean 编译器逐行检查。两条路线共享同一个工程哲学：让说"对"的那一方，不是写"答案"的那一方。

董彬视频里提到的"自主构建的自动化 AI 框架"+“大规模形式化验证”，和这张表里的两条主线高度同构——国内的工作在尝试走和 Axiom 类似的"AI 自主证明 + Lean 形式化"路径。下面会把这条路径拆开看。

第一幕：安德森猜想与"国内首次 AI 自主证明"

先说"安德森猜想"这个名字本身。它（Anderson conjecture）在国际数学界指向好几个不同领域：最有名的是 1967 年 P. W. Anderson 在凝聚态物理里关于无序系统电子态局域化的猜想，2010 年代后普遍被认为不成立；数学领域也有多位 Anderson（如 Greg W. Anderson、Michael T. Anderson）各自提出过猜想。我在公开渠道没找到与"董彬团队证明’安德森猜想’“严格对应的英文文献，这里只能尊重 desc 的事实陈述，不对猜想本身的数学内容展开。

把名字搁一边，desc 里那句话真正值得拆的是后半句——“国内首次实现 AI 自主解决数学开放问题，并实现了大规模形式化验证”。这句话至少压着三层判断：

1. “AI 自主”。指证明的生成主体是 AI，不是 AI 辅助人类数学家。这一条把工作划到了 Axiom 那种"100% AI 证明 + 形式化"的强路线，而不是"AI 形式化人类已写好的证明"或"AI + 人类协作"的弱路线。
2. “数学开放问题”。指这是一个此前没被解决的猜想，而不是"AI 在文献检索里找到了已有证明”——这恰好是 Carina Hong 在 SAIR Summit 上批评的"数学宝可梦狩猎"陷阱的反面。
3. “大规模形式化验证”。指证明被 Lean 之类的形式化系统端到端验证，而不是"AI 写了一段人类可读的草稿"。

三层都成立的话，国内就出现了和 Axiom 在同一档工程强度上的 AI for Math 工作。但要把这句话变成一个可被引用的成果，得等董彬团队的论文或预印本公开，或者等甲子光年的完整文字稿发出来——这是反写"基于 desc 而非完整视频"的最大局限，我诚实标在这里。

国际同行这边，Axiom 的 12 篇论文（截至 2026-06-15）已经覆盖 5 篇 100% AI 自主证明 + 形式化、4 篇 AI + 人类协作、3 篇 AI 形式化人类已写证明。DeepMind 这边，AlphaGeometry 在 30 题几何里解出 25 题，AlphaProof 在 IMO 拿到"银牌标准"（28/42，距金牌 1 分），AlphaEvolve 在 50+ 开放数学问题上跑编码 agent。在 Lean 这条路上，国内同行不是孤军——Lean FRO、mathlib 的 20 万级形式化定理、Axiom 公开的 AXLE 工具集，都是可直接拿的开源资源。

第二幕：一个 AI 证明在 Lean 里走一遍

视频 desc 没有详细描述董彬团队的"自动化 AI 框架"具体是什么，只给了两条线索——“自主构建"和"大规模形式化验证”。从这两条出发，我可以基于国际同行的做法搭一个推测框架。要强调这是框架性推测，不是对董彬方法的精确转述。

这些团队的工程范式高度相似。下面用一个"证明某个数论猜想"的任务把它串起来，看抽象机制在一次真实工作里怎么配合——这是理解董彬那套"自动化框架"最直接的入口。

第一步，拆任务。 一个完整的证明任务会被规划 Agent 拆成多个子目标——比如"先证明一个引理"、“再做一次归纳”、“调用 mathlib 里的某个已知结论”。拆完丢给一组执行 Agent，串行或并行跑。

第二步，每一步都调真工具。 执行 Agent 不会空想下一步，它调用 Lean 的 tactic 写出形式化代码、查 mathlib 库找可用定理、必要时调外部计算机代数系统（CAS）做符号计算。Axiom 公开强调用开源大模型做底座，理由很具体——数学证明要可审计、可复现，闭源模型每次版本变化都会让历史证明失效。

第三步，Lean 当裁判。 每写完一段 tactic，Lean 编译器立刻逐行检查。逻辑错了就报错退出，Agent 必须回溯换路。这跟"AI 写一段人类可读草稿、交给审稿人慢慢看"是完全不同的反馈回路——前者是毫秒级的硬判决，后者是月级别的软判断。

第四步，靠测试时计算扩展（test-time compute scaling）提正确率。 一条路走不通就回溯，换一条再试。AlphaEvolve 把这个思路推到极致：它在 Gemini 的训练里用来优化底层 kernel，靠的就是"推理时多跑几轮"而不是"训练一个更大的模型"。

一段被 Lean 4 逐行检查的证明，长得大致是这样（示意）：

theorem add_comm_demo (a b : Nat) : a + b = b + a := by
  induction b with
  | zero => simp
  | succ n ih => rw [Nat.add_succ, ih, Nat.succ_add]
-- 任一步逻辑不成立，Lean 立刻报错，Agent 必须回溯换路

把这四步装进 Lean，结果就是：AI 输出的不是一段人类可读的草稿，而是一段 Lean 可执行的代码。这段代码可以在任何一台装了 Lean 4 的电脑上逐行复现。AxiomProver 在 2025-12 解 Erdős 问题时用了约 50 个推理节点，到 2026-04 证明 Ramanujan τ 函数性质时涨到 500——这个 10 倍跃升，测的正是"AI 在一棵不断回溯的搜索树里要展开多少个节点才能让 Lean 全程不报错"。它反映的是问题难度和搜索空间，不能直接换算成"AI 比 5 个月前聪明了 10 倍"。

视频 desc 说"实现了大规模形式化验证"，意味着董彬团队的路线大概率也是 Lean 或 Coq 之一——否则"形式化验证"这个表述没有技术落点。Lean 在数学社区渗透率更高，mathlib 的定理量级是 Coq 数学标准库的好几倍；Coq 在工业级验证和软件正确性上更强（CompCert 编译器、seL4 微内核都是 Coq 形式化的）。如果董彬的工作偏数论方向，Lean 的概率显著高于 Coq——这是从范式选择推到工具链的合理判断，但仍是推断，要确认得看公开论文。

第三幕：北大数院"黄金一代"——数学的反差叙事

desc 提到董彬 1999 年入北大数学科学学院，“误入"数院、基础班 60 人 GPA 倒数第二 2.7/4.0、差点没能顺利毕业；又说"1999 年那一代"是北大数学的"黄金一代”。这两件事叠在一起，是一个非常中国式的反差叙事。

要读懂这个叙事，先得明白北大数院的"基础班"是什么。北大数院从 1978 年起设基础班（最初叫"数学系基础数学专业"），目标是培养顶尖数学研究者，每年从入学本科生里选拔约 20–30 人组成特殊班级，配最强的师资、更难的课程、更频繁的淘汰。基础班的淘汰机制是出了名的——很多人大二、大三被分流到其他专业，最后坚持到毕业、进入数学研究的只是少数。董彬在 60 人里排倒数第二、差点没毕业，意味着他趟过的是北大数院最残酷的那道筛子——而他最后活下来了。

1999 年那一代后来被叫做"黄金一代"，是因为那几年北大数院集中出了一批在国际数学界站得住的学者。刘若川、许晨阳、肖梁、董彬、朱歆文、张钺、王博潼……这串名字分散在代数几何、数论、表示论的不同分支。许晨阳 2018 年做了 ICM（国际数学家大会）受邀报告；朱歆文是"新视野"数学奖得主；刘若川在 p-进 Hodge 理论上的工作国际知名；董彬把方向转向了 AI for Math。

这一代人之所以被叫"黄金"，不是因为挤在同一个数学分支里，而是因为各自把方向做到了国际前沿。北大数院基础班真正产出的，不是某种"数学天才"，而是一批被严格训练过、有能力在数学共同体里做出原创工作的人。

把这段反差叙事和董彬现在的 AI for Math 工作叠在一起读，会看到一个有意思的对照：他在数学训练的"正路"上被训成了"鉴赏家"——能识别好的数学、能做严密的推理、能写形式化的证明；而他下一步的方向，恰恰是让 AI 也具备这些能力。一个数学家对"什么是真正的数学能力"的反向投射——自己经历过 2.7 GPA 的痛苦筛选，现在想让 AI 跳过这个过程。

也正因为这样，他和视频里那个"数学家沦为鉴赏家"的话题之间，有非常具体的个人经验底子。这不是外行的预测，是一个从 1999 年北大数院基础班走过来的数学家，在反思自己所受的那套训练。

第四幕：数学家会沦为"鉴赏家"吗

desc 里抛出的一个核心问题是：“数学家会沦为’鉴赏家’吗？“这个比喻在国际数学共同体里被反复讨论。

鉴赏家（connoisseur）指的是：在 AI 能自主证明数学猜想之后，人类数学家的角色可能从"做数学的人"变成"判断 AI 做的数学是否正确、是否有价值、是否值得追下去的人”——就像艺术市场上 AI 生成画作之后，人类艺术评论家的工作从"创作"滑向"鉴赏”。

支持这个判断的证据，在工作流里就能直接看到。Axiom 的 12 篇论文是现成的样本：5 篇 100% AI 自主证明 + 形式化、4 篇 AI + 人类协作、3 篇 AI 形式化人类已写好的证明。协作论文里的人类数学家，主要工作已经变成"提示、追问、判断 AI 给的方向值不值得追"——这就是鉴赏家在做的事。AlphaEvolve 的白皮书致谢了 Terence Tao（陶哲轩，2006 年菲尔兹奖得主），他的角色是"作为顾问参与，给 AI 提供数学方向感和战略判断"，同样是鉴赏家的活。Ken Ono 加入 Axiom 之后，工作重心越来越像"在 AI 给出的几百个推理节点里，挑出最值得追问的方向，写下一阶段的提问 prompt"。这是 2025 年的数学家工作正在长出的新形态。

但"沦为鉴赏家"这个判断要成立，得有个前提：人类数学家真的不再动手做证明了。这个前提目前站不住。Axiom 论文 #12 是 Bernhard Heim + Ken Ono + Axiom 三方合作，Ono 亲自动手用 AxiomProver 在 Lean 里写证明——当最顶尖的数学家下场使用 AI 工具时，他们的工作方式更像教练或高级用户，仍在动手，只是工具换了。更关键的是，数学的核心从来不是"证明别人提的猜想"，而是"提出值得追的猜想"。AlphaEvolve 目前能做的是在给定猜想下找更好的解，还没稳定跨过"自己提出猜想"这一步——这才是人类数学家暂时拿不走的位置。再加上 desc 提到的"上千位数学家签署宣言反对 AI"，说明共同体本身对这件事有强烈反弹，远没到接受"数学家退居鉴赏席"的程度。

所以"数学家会沦为鉴赏家吗"这个问题，目前没有一个能一锤定音的答案。它取决于你把数学工作的哪一块看作核心：如果核心是"证明"，鉴赏家化已经在发生；如果核心是"提出猜想、判断方向、跨领域综合"，AI 离取代数学家还有相当距离。董彬作为国内 AI for Math 的先行者，对这个问题应该有更具体的判断——我没有字幕可以引用，只能把问题留开放。

第五幕：期刊体系会崩溃吗

desc 提到的另一个延伸话题是"现有期刊体系会不会崩溃"和"上千位数学家签署宣言反对 AI"。这两个话题其实是同一个过程的两个侧面。

传统数学期刊的核心功能是同行评审——一篇论文要被接收，得有 2–4 位匿名审稿人在 6–18 个月内完成审稿、修改、再审稿的循环。这套机制在 2020 年代被几股力量同时压着：

1. 预印本文化。arXiv 让论文在投期刊之前就已经被共同体读到，期刊的"首发权"被削弱。
2. AI 生成的证明难以审查。一篇论文里如果 AI 给出了关键步骤，审稿人要在短时间内判断"AI 给的证明对不对"非常困难——需要在 Lean 之类的形式化系统里复现，才能真正确认。
3. AI for Math 公司的出现。Axiom 把"AI 写论文"做成了一门生意，期刊编辑发现自己要面对一种新型的"作者"：不是人类数学家，而是一台机器加一个公司。

Axiom 的应对策略是把 12 篇论文投到《Archiv der Mathematik》《Indagationes Mathematicae》《Journal of Combinatorial Theory》等期刊，让现有的同行评审给 AI 证明打分——这是把 AI 装进旧体系的尝试。顺着这条逻辑往下推：体系不改革，AI 证明就只能挂在 arXiv 上等共同体的非正式评判；体系要改革，就得立新规矩，比如"AI 证明必须附 Lean 形式化代码才能投稿"。

至于"上千位数学家签署宣言反对 AI"，我在公开渠道没找到确切来源——可能指的是 2023–2024 年间关于"AI 生成内容是否应进入学术评价体系"的几次公开信或联署事件，但确认不了具体是哪一份宣言、谁签的、诉求是什么。这里我尊重 desc 的事实陈述，不对宣言内容展开。

有一个相关的、能核实的事实是：Lean FRO（Lean 背后的基金会）拿到了 ACM SIGPLAN 软件奖，学术界主流已经接受形式化证明作为数学工作的合法一部分。从"形式化是少数派"到"形式化是主流工具"，这个转变已经在发生。

第六幕：高考志愿——给普通人的答案

desc 提到的最后一个话题是高考志愿填报。这是访谈里最贴近普通读者的一块。

我没有字幕可以引用董彬的具体建议，但可以基于公开材料搭一个推断框架。董彬自己 1999 年是"误入"北大数院的，GPA 2.7 差点没毕业。他不是那种"小学就知道自己要学数学"的天才型选手，是经过北大数院基础班的严格筛选、被"虐得很惨"之后活下来的。他对"什么人不该学数学"和"什么人不学数学也能做数学相关的事"，应该是有具体答案的。

AI for Math 这条赛道在 2026 年夏天的状态大致是这样：

• 数学基础仍然不可替代。Lean 形式化、mathlib 定理库、Lean 编译器，这些是数学家几十年的工作积累。AI 在这个基础上做的是"调用 + 重组 + 加速"，不是从零发明。
• 跨学科能力比纯数学能力更稀缺。Axiom 的 Carina Hong 是商业 + 工程背景，Ken Ono 是数学背景，DeepMind 的 AlphaEvolve 团队里既有 AI 研究员也有数学家。“数学 + AI"是稀缺组合，“纯数学"或"纯 AI"反而没那么稀缺。
• 形式化验证能力是新的硬通货。Lean / Coq 这些工具在 2026 年开始进入主流数学工作流，但会写的人极少。这和 1990 年代"会编程"的稀缺性类似。
• AI 暂时替代不了的是"提出猜想”。desc 里也提到这个担忧。但反过来看，能提出好猜想的人，本来就比能证明猜想的人少。

如果董彬要给一个具体建议（基于他个人经验和行业需求推断），大概率会落在"如果你数学好但不确定要不要走纯数学，考虑数学 + AI / 数学 + CS / 数学 + 形式化验证的复合路径”。这比 1999 年"误入北大数学"时的选择面宽得多——20 年前，数学系学生的出口只有"做数学家"或"转行"；现在有了第三个出口：“用 AI 加速数学”。

这只是基于公开材料的推断。董彬在视频里具体怎么说的，我没有字幕可以引用——这是反写绕不开的局限。

第七幕：把这一代人的位置摆好

写到这儿，desc 里最让我触动的不是"AI 证明数学猜想"这种新闻性细节，而是"这是关乎每个普通人的对话"这一句。董彬的访谈在视频简介里就明确标注，眼下正值高考志愿填报季。

把 desc 里的几个话题串起来读，会发现它们指向同一个核心问题：

在一个 AI 能自主证明数学猜想的世界里，人类的数学能力还值什么价？

拆成三个具体的子问题：

人类数学家的位置是什么？

2026 年年中的答案是：从"做题者"变成"方向判断者 + 战略提示者 + 形式化审查者"。这是鉴赏家化正在发生的真实状态。但"提出新猜想"这个位置还没被 AI 占据，这是一条仍然属于人类的护城河。

普通学生学数学是为了什么？

不是为了"成为能证明猜想的人"，而是为了"具备数学直觉、形式化思维、跨学科迁移能力"。这些能力在 AI 时代的稀缺性不是变低了，而是变高了——AI 让"会算"变得不稀缺，让"会问"变得稀缺。

AI for Math 这条赛道对年轻人意味着什么？

这是一条极度跨学科的赛道——数学 + AI + 工具链 + 形式化验证 + 学术发表体系，每个环节都需要不同背景的人。Axiom 的团队组成证明：纯数学家、AI 研究员、工程师、商业人才，缺一不可。对年轻人来说，这条赛道比"纯数学"或"纯 AI"都更适合那些还没想清楚要走哪条路的人。

这三个答案都不是终极答案，但能给到一个具体的思考起点——这是反写这篇文章的目的。

常见误读

下面几条是最容易搞错的地方——顺带说清“为什么错”，方便你排查自己的理解：

• 「AI 证明了猜想 = AI 比数学家聪明」——不对。判决权在 Lean 编译器，不在 AI；AI 干的是“在搜索树里试出一条能通过编译的路”。推理节点从 50 涨到 500 反映的是搜索空间，不是“智商翻 10 倍”。
• 「形式化验证 = AI 写人类可读证明」——不对。形式化是把每一步写成 Lean/Coq 可机械检查的代码，和“AI 写一段草稿交人审”是两种反馈回路（毫秒级硬判决 vs 月级软判断）。
• 「AI 能自证猜想，学数学就没用了」——恰恰相反。AI 让“会算”不稀缺、让“会问（提出猜想）”更稀缺；数学直觉、形式化思维、跨学科迁移在 AI 时代的价值是升的。

自测清单

读完可以对着几个问题自测——也拿国际同行那几个例子当参照：

• 说得清“AI 自主证明”和“AI 辅助 / AI 形式化人类证明”三条强弱路线的区别吗？
• 讲得出为什么“判决者独立于生成者”（Lean 当裁判）是这套范式的关键？
• 说得出“数学家沦为鉴赏家”这个判断成立与不成立各自的前提吗？
• 列得出 AlphaProof / AlphaGeometry / AlphaEvolve / FunSearch 各自跨过的门槛吗？

下一步：如果你看过这段视频，欢迎指正写偏的地方；想深入可先读附录里 Axiom / Lean 的一手资料。

附录 A：核心术语 5 分钟扫盲

• AI for Math：用人工智能方法解决数学问题、辅助数学发现的交叉学科。代表工作：DeepMind AlphaProof / AlphaGeometry / AlphaEvolve / FunSearch，Axiom Math 的 AxiomProver，国内的董彬团队等。
• 形式化验证（formal verification）：用数学符号和逻辑规则写出证明，让计算机可以机械地验证每一步推理是否正确。代表工具：Lean 4、Coq、Isabelle、HOL Light。
• Lean 4：由 Leonardo de Moura 在微软研究院启动的证明辅助语言，mathlib 库已形式化 20 万级定理。Lean FRO 是其背后的基金会。
• Axiom Math：2024 年成立的 AI for Math 初创公司，总部加州帕罗奥图，创始数学家 Ken Ono（弗吉尼亚大学前讲席教授），CEO Carina Hong。2026-06-05 Hong 在 SAIR Summit 演讲，截至 2026-06-15 已发表 12 篇论文，含 5 篇 100% AI 自主证明 + 形式化。
• AxiomProver：Axiom Math 内部的 AI 形式化证明器，输出可被 Lean 4 编译验证的代码。推理节点数从 2025-12 的约 50 个增长到 2026-04 的约 500 个（10 倍跃升，反映搜索空间大小，不能直接换算成"AI 智商"）。
• AlphaProof：DeepMind 2024 年发布的 IMO 数学竞赛 AI 系统，2024 年 IMO 拿 28/42 分达"银牌标准"（距金牌线 1 分），2025 年与 Gemini Deep Think 组合达到金牌级别。
• AlphaGeometry：DeepMind 2024-01 发布的 IMO 几何 AI 系统，30 题解出 25 题（金牌阈值 26），神经-符号混合架构 + 1 亿合成训练样本。论文发在《Nature》。
• AlphaEvolve：DeepMind 2025-05 发布的 Gemini-powered 编码 agent，在 50+ 开放数学问题上测试，arXiv 白皮书见 abs/2506.13131。
• FunSearch：DeepMind 2023-12 发布的工具，首次用 LLM 在开放数学问题（cap set 问题）上发现新结果，论文次月发《Nature》，奠定了"LLM 生成 + 外部验证"的工作流范式。
• IMO（国际数学奥林匹克）：面向高中生的国际数学竞赛，数学界最受关注的竞赛之一，也是 AI 数学推理能力的标志性测试场。
• ICM（国际数学家大会）：每四年一次的国际数学界最高级别会议，受邀做报告是学术声誉的重要标志。
• 北大数学科学学院基础班：北大数院 1978 年开始的特殊班级，每年选拔约 20–30 名本科生配备最强师资、更难课程、更频繁淘汰。1999 年那一代被称为北大数学的"黄金一代"。

附录 B：参考资料与延伸阅读

视频本身

• 视频原片：B 站《甲小姐对话董彬：AI for Math 的无尽前沿，AI 时代不被替代的志愿……请相信数学！》（BV1cDTe6QE4p），2026-07-01 11:16 由"甲子光年官方账号"发布，时长 2:16:15。该视频在 B 站明确标注"暂无字幕"，本文未观看完整视频，全部内容基于视频 desc + 公开学术资料综合整理。
• 视频 desc 来源：B 站 view API https://api.bilibili.com/x/web-interface/view?bvid=BV1cDTe6QE4p 抓取（fetched 2026-07-02 16:30 CST）。

国际 AI for Math 权威工作

• DeepMind AlphaProof（2024 IMO 银牌）；2025 年与 Gemini Deep Think（金牌标准） 组合达金牌级
• DeepMind AlphaGeometry（《Nature》论文，NYU 合作）
• DeepMind AlphaEvolve（arXiv 白皮书 abs/2506.13131）
• DeepMind FunSearch（《Nature》论文，cap set 问题）
• Axiom Math：官网 ｜ 论文列表 ｜ 开源工具集 AXLE
• Lean 4：官方文档 ｜ GitHub ｜ mathlib 统计 ｜ Lean FRO 基金会
• 维基：Ken Ono ｜ Scott Duke Kominers ｜ Robert Aumann（2005 诺奖）
• Carina Hong SAIR Summit 2026 演讲（视频精读）：本仓库 content/posts/video/axiom-ai-mathematician-formal-verification-lean.md

国内相关背景

• 北京大学北京国际数学研究中心（BICMR）
• 北京中关村学院：董彬任常务副院长（视频 desc 提到）
• 甲子光年：官网 ｜ “甲小姐对话"系列

限制与声明

• 本文不对"安德森猜想"的具体数学内容做实质讨论——视频未提供字幕，公开渠道未检索到对应文献。
• 本文不对"上千位数学家签署宣言反对 AI"的具体来源、签署人、诉求做实质讨论。
• 本文不对董彬在视频中的具体金句做引用——所有董彬的具体观点均以"视频 desc 提到"的形式陈述。
• 文中 AlphaEvolve 的部分量化指标（如开放问题上的最优解超越比例、训练 kernel 提速）未在本文核查周期内完成一手核实，故正文采用概括表述；如需精确数字请查阅 DeepMind 官方博客与 arXiv 白皮书 abs/2506.13131。
• 许晨阳的 ICM 受邀年份、朱歆文的"新视野"奖等"黄金一代"人物的具体奖项，建议以 IMU 官方名单和 Breakthrough Prize 官方名单为准。
• 如视频发布完整文字稿（甲子光年公众号文章），本文将在核实后重新修订。