数学还能学吗？北大董彬与 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 篇论文，2025 年离开弗吉尼亚大学讲席教授席位、以"创始数学家"身份加入的 Ken Ono 已深度参与其中——他与 Bernhard Heim、Markus Neuhauser 合作的 Nekrasov–Okounkov 论文被期刊接收，附录证明由 AxiomProver 在 Lean 里生成并验证；而 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）、与主播甲小姐是"同门师兄"；desc 里有一句以直接引语给出的董彬观点——“越偏向就业、实用性越强的学科，越在 AI 的打击范围之内”；访谈还涉及期刊体系、千位数学家签署宣言反对 AI、数学家会否沦为"鉴赏家"、高考志愿这几个延伸话题，以及一个更开放的追问——当 AI 几乎能承担所有"工具价值"，人类如何重新定义与分配"尊严"。

血肉从国际硬进展里借：DeepMind 的 AlphaProof（IMO 银牌）/ AlphaGeometry（IMO 几何 25/30 题）/ AlphaEvolve（50+ 开放问题）/ FunSearch（首次用 LLM 在开放问题上发现新结果）；Axiom Math 论文页挂出的 12 篇论文（3 项期刊接收，部分条目未能独立核实）/ Ken Ono 离开 UVA 加入工业界 / Lean 4 形式化 20 万级定理。这些 2024–2026 年间发生的真实事件，构成视频"无尽前沿"可独立查阅的参照系。看过视频的读者若发现写偏之处，欢迎指正。

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

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

Axiom 的成绩单按演讲口径是：2026 年 2 月起发布 7 篇论文，其中 5 篇涉及形式化定理证明，3 项成果被《Mathematische Nachrichten》《Indagationes Mathematicae》《Archiv der Mathematik》接收；官网论文页在演讲前后共挂出 12 篇，其中部分条目（如 Aumann 定理形式化）截至本文修订未能独立核实。

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

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

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

先说"安德森猜想"这个名字本身。它（Anderson conjecture）在国际数学界指向好几个不同领域：最有名的是物理学家 P. W. Anderson 在凝聚态物理里关于无序系统的猜想；数学领域也有多位 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 按演讲口径是 2026 年 2 月起 7 篇论文、5 篇涉及形式化、3 项期刊接收，官网论文页在演讲前后共挂出 12 篇（部分条目未能独立核实）；能对回 arXiv 的论文里，参与深度从"形式化一个关键组合恒等式"一直到"主引擎由 AxiomProver 自动生成并形式化"。DeepMind 这边，AlphaGeometry 在 30 题几何里解出 25 题，AlphaProof 与 AlphaGeometry 2 组合在 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 的电脑上逐行复现。按 Carina Hong 在 SAIR 演讲里的口径，AxiomProver 2025 年 12 月解决一个 Erdős 问题时用了约 50 个推理节点，到 2026 年 3 月 31 日提交 arXiv 的 Ramanujan τ 函数论文时涨到约 500——这个 10 倍跃升，测的正是"AI 在一棵不断回溯的搜索树里要展开多少个节点才能让 Lean 全程不报错"。它反映的是问题难度和搜索空间，不能直接换算成"AI 比 5 个月前聪明了 10 倍"。

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

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

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

要读懂这个叙事，只需要盯住 desc 里那组数字：基础班 60 人、排名倒数第二、GPA 2.7/4.0、差点没能顺利毕业——按 desc 的转述，他自己说"在北大数院的四年被’虐得很惨’"。这是一段被筛得很疼的经历——而他最后活下来了，还把数学做成了志业。

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

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

把这段反差叙事和董彬现在的 AI for Math 工作叠在一起读，会看到一个有意思的对照：他在数学训练的"正路"上被训成了"鉴赏家"——能识别好的数学、能做严密的推理、能写形式化的证明；而他下一步的方向，恰恰是让 AI 也具备这些能力。所以他在访谈里面对"数学家会沦为鉴赏家吗"这个话题时，背后是具体的个人经验：一个从 1999 年北大数院走过来的数学家，在反思自己所受的那套训练。这不是外行的预测。

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

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

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

支持这个判断的证据，在工作流里就能直接看到。Axiom 能对回 arXiv 的论文里，Ken Ono 等人类数学家的名字和 AxiomProver 并排出现：τ 函数论文的 24 位作者里，机器承担的是论文摘要里写明的主引擎角色，人负责命题与方向。协作模式下的人类数学家，主要工作已经变成提示、追问、判断 AI 给的方向值不值得追——这就是鉴赏家在做的事。AlphaEvolve 的白皮书致谢了陶哲轩（Terence Tao，2006 年菲尔兹奖得主），他在系统公布前受邀试用、在数学方向上给出反馈，同样是鉴赏家的活。Ken Ono 在 Axiom 的角色也类似：在 AI 给出的几百个推理节点里，挑出最值得追问的方向。这是数学家工作正在长出的新形态。

但"沦为鉴赏家"这个判断要成立，得有个前提：人类数学家真的不再动手做证明了。这个前提目前站不住。Ken Ono 加入 Axiom 后不是退居二线——他深度参与论文写作，用 AI 工具把直觉推成可验证的证明。当最顶尖的数学家下场使用这些工具时，他们的工作方式更像教练或高级用户：仍在动手，只是工具换了。

更关键的是，数学的核心从来不是"证明别人提的猜想"，而是"提出值得追的猜想"。AlphaEvolve 目前能做的是在给定猜想下找更好的解，还没稳定跨过"自己提出猜想"这一步——这才是人类数学家暂时拿不走的位置。再加上 desc 提到的"上千位数学家签署宣言反对 AI"，说明共同体本身对这件事有强烈反弹，远没到接受"数学家退居鉴赏席"的程度。

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

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

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

传统数学期刊的核心功能是同行评审——一篇论文要被接收，得经过匿名审稿人数月到一年多的审稿、修改、再审稿循环。这套机制在 2020 年代被几股力量同时压着：

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

Axiom 的应对策略是把 AI 参与的论文投给正经学术期刊——按演讲口径已有 3 项成果被《Mathematische Nachrichten》《Indagationes Mathematicae》《Archiv der Mathematik》接收，Nekrasov–Okounkov 论文则被《Research in Number Theory》接收，让现有的同行评审给 AI 证明打分——这是把 AI 装进旧体系的尝试。顺着这条逻辑往下推：体系不改革，AI 证明就只能挂在 arXiv 上等共同体的非正式评判；体系要改革，就得立新规矩，比如"AI 证明必须附 Lean 形式化代码才能投稿"。

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

有一个相关的、能核实的事实是：2025 年，ACM SIGPLAN 把编程语言软件奖颁给了 Lean 的四位核心开发者（Gabriel Ebner、Soonho Kong、Leonardo de Moura、Sebastian Ullrich），授奖理由是 Lean 对数学、硬件与软件验证以及 AI 的影响。学术界主流已经接受形式化证明作为数学工作的合法一部分。从"形式化是少数派"到"形式化是主流工具"，这个转变已经在发生。

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

desc 提到的最后一个话题是高考志愿填报。这是访谈里最贴近普通读者的一块，也是 desc 里唯一给出董彬直接引语的地方。

这句话值得原样放在这里——正值高考志愿填报季，无数家长学生在困惑 AI 时代选什么专业才不容易被替代，desc 记下的董彬观点是：

“越偏向就业、实用性越强的学科，越在 AI 的打击范围之内。”

这句话和直觉相反，却和 AI for Math 的现状对得上：AI 最先吃得透的，恰恰是模式清晰、目标明确、以"工具价值"为主的领域——写格式化文书、做标准化题、跑固定流程，这些"实用技能"的边界越清楚，越容易被模型复刻。而数学训练给的东西——面对一个没人知道答案的问题，自己搭结构、自己验证对错——恰恰是模型最难自动化的部分。

以此为准绳，AI for Math 这条赛道在 2026 年夏天的状态大致是这样：

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

至于"你该不该报数学”，desc 没给到那么细。但从这句引语和他个人的路径——1999 年"误入"北大数院，被"虐得很惨"，最后把数学做成了和 AI 交叉的志业——能推出来的是：他劝的不是"都去学数学"，而是别用"好不好就业"当唯一的选专业标尺，因为那个标尺本身正在被 AI 重写。这是基于公开材料的推断，具体建议在访谈原声里，我没有字幕可以引用。

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

desc 里比"AI 证明数学猜想"这类新闻性细节更值得读的，是"这也是一场关乎每个普通人的对话"这一句。董彬的访谈在视频简介里就明确提到，眼下正值高考志愿填报季。

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

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

拆成三个具体的子问题：

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

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

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

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

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

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

在三个子问题之外，desc 还记下了访谈的两个落点：一是董彬分享了他的"登月"野心（具体内容没有字幕可考）；二是整场对话最后的追问——当 AI 几乎能承担所有"工具价值"，人类如何剥离自身的工具属性，重新定义与分配所谓的"尊严"？这两个点决定了这场访谈的分量：前者是国内 AI for Math 的目标刻度，后者比"要不要学数学"更根本——“越实用越容易被打击"的判断，最后收束到的不是专业选择技巧，而是人的位置怎么重新定义。

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

读者判断：这段视频适合谁

建议去看原片：想听董彬本人具体论述和现场发挥的读者——本文无字幕可引，观点基本只能以"desc 提到"转述，唯一直接引语在第六幕；正在填高考志愿、想要"数学还值不值得学"个体化建议的读者——desc 只给了一句话观点，落到"你该不该报数学"的答案在访谈原声里；想弄清"安德森猜想"和"千位数学家宣言"细节的读者——这两处本文明确标了无法核实，访谈里董彬或许给了上下文。

读本文就够：想快速定位"国内 AI for Math 在国际坐标系里的档位”——总览表加第一、二幕就能对上；想把"AI 自主证明 + 形式化验证"范式理解透——第二幕的框架比转述更体系化；想对"数学家会不会沦为鉴赏家"听一个有论证、留余地的判断——第四幕给了前提和反例。

关于时间点：视频在 B 站标注"暂无字幕"，公开渠道也没有章节标记，本文给不出"董彬在哪一分秒说了什么"的时间戳，只能按话题组织。这对理解访谈话题没有损失，回看原片定位具体段落会麻烦些。

常见误读

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

• 「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：2013 年由 Leonardo de Moura 在微软研究院启动的证明辅助语言，mathlib 库已形式化 20 万级定理。2025 年 ACM SIGPLAN 编程语言软件奖授予 Lean 的四位核心开发者（Ebner、Kong、de Moura、Ullrich）。Lean FRO 是其背后的基金会。
• Axiom Math：2025 年成立的 AI for Math 初创公司，总部加州帕罗奥图，创始数学家 Ken Ono（2025 年离开弗吉尼亚大学讲席教授席位加入），CEO Carina Hong。2026 年 6 月上旬 Hong 在 SAIR 基金会 2026 Science x AI Summit 演讲，演讲口径为当年 2 月起 7 篇论文、5 篇涉及形式化、3 项期刊接收；官网论文页前后共挂出 12 篇，部分条目未能独立核实。
• AxiomProver：Axiom Math 内部的 AI 形式化证明器，输出可被 Lean 4 编译验证的代码。按演讲口径，推理节点数从 2025-12 解决一个 Erdős 问题的约 50 个，涨到 2026-03 提交 arXiv 的 τ 函数论文的约 500 个（10 倍跃升，反映搜索空间大小，不能直接换算成"AI 智商"）。
• AlphaProof：DeepMind 2024 年发布的 IMO 数学竞赛 AI 系统，2024 年与 AlphaGeometry 2 组合拿 28/42 分达"银牌标准"（距金牌线 1 分）。2025 年 DeepMind 以 Gemini Deep Think 端到端达到金牌标准（35/42），没有 AlphaProof 参与，但官方说明该成果延续了 AlphaProof 一脉的研究。
• AlphaGeometry：DeepMind 2024-01 发布的 IMO 几何 AI 系统，30 题解出 25 题（金牌选手平均 25.9 题），神经-符号混合架构 + 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（国际数学家大会）：每四年一次的国际数学界最高级别会议，受邀做报告是学术声誉的重要标志。
• 北大数学科学学院基础班：desc 里提到的董彬当年所在班级——60 人中排名倒数第二、GPA 2.7/4.0、差点没能毕业。其制度沿革本文未能独立核实，不作展开。

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

视频本身

• 视频原片：B 站《甲小姐对话北大董彬：AI for Math的无尽前沿，AI时代不被替代的志愿……请相信数学！》（BV1cDTe6QE4p），2026-07-01 19: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；2026-09-23 修订时复抓核实，账号名、发布时间、desc 全文与此一致）。

国际 AI for Math 权威工作

• DeepMind AlphaProof（2024 IMO 银牌）；2025 年 IMO 金牌由 Gemini Deep Think 端到端拿下（35/42），官方说明其延续 AlphaProof 一脉的研究
• 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 ｜ 许晨阳 Chenyang Xu ｜ 朱歆文 Xinwen Zhu
• Carina Hong SAIR Summit 2026 演讲（视频精读）：本仓库 content/posts/video/axiom-ai-mathematician-formal-verification-lean.md

国内相关背景

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

限制与声明

• 本文不对"安德森猜想"的具体数学内容做实质讨论——视频未提供字幕，公开渠道未检索到对应文献。
• 本文不对"上千位数学家签署宣言反对 AI"的具体来源、签署人、诉求做实质讨论。
• 董彬的观点只引用 desc 以直接引语给出的那一句（高考志愿），其余观点均以"视频 desc 提到"的形式陈述，不虚构访谈原声。
• Axiom 的成绩单按 Carina Hong 演讲口径陈述；官网论文页的部分条目（如 Aumann 定理形式化）未能独立核实，本文不展开；总览表中 Collatz 论文的 arXiv 署名（Charton / Narayanan）与 Axiom 的关系未获确认，表中已如实标注。
• 文中 AlphaEvolve 的部分量化指标（如开放问题上的最优解超越比例、训练 kernel 提速）未在本文核查周期内完成一手核实，故正文采用概括表述；如需精确数字请查阅 DeepMind 官方博客与 arXiv 白皮书 abs/2506.13131。
• “黄金一代"人物成就中，许晨阳 ICM 受邀报告（2018）、两人次"新视野"数学奖（许晨阳 2019、朱歆文 2020）已经英文维基条目核实；其余以 IMU 官方名单和 Breakthrough Prize 官方名单为准。
• 如视频发布完整文字稿（“甲小姐对话"账号或甲子光年公众号），核实后会重新修订本文。