本期是集智俱乐部发起的 AI for Math（人工智能与数学）读书会第二季第 6 期，由北大朱韬宇博士主讲，核心主线是：AI 正在把数学从 “单人深度案例式探索” 拓展为 “人机协同的实验型研究范式”；不再只是刷竞赛题，而是进入猜想发现、引理搜索、形式化核验、长证明拆解的研究场景，同时也暴露出形式翻译的语义保真、证明价值衡量、学术责任归属等新难题。
一、读书会基础信息
- 发起方：集智俱乐部；联合发起人：同济大学陈小杨、北工大诸葛昌靖
- 主讲：朱韬宇（北大 BIOPIC，方向：代数拓扑、黎曼几何、计算生物学）
- 时间：2026‑11‑08，上午 10:00–12:00，线上腾讯会议
- 本季周期：2026‑09‑22 起，每周二晚，共 8–10 周，含分享、文献研读、回放资源
- 本期大纲：
- 数学 AI 的底层技术栈：大模型、强化学习、数学智能体
- 能力跃迁：从做题走向研究级数学探索，结合陶哲轩 “数学 2.0”、First Proof、AlphaProof
- 核心案例：Navier‑Stokes（N‑S）方程，讨论形式化转换与语义一致性
- 国内外数学 Agent 路线，包含丘成桐团队相关工作
- 新研究流程、人机分工、责任边界与评价陷阱（Goodhart 定律）
二、技术底座：三类核心组件
| 模块 | 作用说明 |
|---|---|
| 数学大模型 | 自然语言猜想、引理生成、草稿证明、文献检索；天然存在长推理幻觉 |
| 强化学习证明搜索 | 在 Lean / Isabelle 等定理证明器里做路径搜索，代表工作 AlphaProof |
| 数学智能体（Math Agent） | 自主规划、拆分目标、调用符号工具、验证子目标、回溯失败分支，把大模型、形式化验证、检索串联起来 |
关键点：单独大模型不可靠；真正适合研究的系统，是「生成 + 形式化翻译 + 机器核验」的闭环，不是直接采信模型输出的证明文本。
三、范式转变：从解题到数学发现
传统数学范式：数学家选定问题，靠直觉、案例推演、手工构造反例，逐步形成猜想与证明，是 “小样本深度钻研”。
AI 带来的新增能力，读书会归纳为三点：
- 批量普查（陶哲轩提出的群体式研究）：一次性扫描上千个同类问题、长尾猜想，快速筛选值得深入的方向；适合把冷门、搁置多年的猜想批量试探。
- 自动引理挖掘与构造辅助对象：寻找人类不容易想到的中间引理、模空间构造、反模型。
- 形式化可信存证：一旦完整转入 Lean，由类型检查器核验，这条证明的逻辑正确性独立可复现，减少审稿中的隐性漏洞。
但读书会强调一个分界：AlphaProof、First Proof 系列证明的是 “研究难度” 的命题，不等于能攻克最顶级的重大猜想；AI 更擅长拓宽搜索面，而不是直接替代深度数学洞察。
四、重点案例：Navier‑Stokes 与语义一致性
N‑S 方程是本期核心讨论样本，用来暴露「自然语言数学」和「形式化代码」之间的鸿沟：
- 把论文里的命题翻译成 Lean，最难不是语法，而是语义保真：定义域、正则性假设、边界条件、弱解 / 强解的区分，稍有偏差，形式化证明就变成证明另一个命题；
- 即使用机器通过检查，也要人工确认：形式版本和原始数学问题是不是同一个东西；
- 引申结论：形式验证 ≠ “自动正确”，它只保证：在形式系统内部，推导链合法；语义对齐是人类责任。
五、两条路线：国内 Agent 与丘成桐团队方向
读书会对比了两条路线：
- 海外路线：OpenAI First Proof、AlphaProof、陶哲轩 SAIR（开放数学模型，社区共建治理），偏向形式化证明搜索、猜想普查；
- 国内路线（丘成桐数学与人工智能联盟）：更强调双向赋能：用数学原理约束 AI，同时用 AI 加速几何、流形、偏微分方程、代数几何的探索；不只做证明，也面向物理、工程交叉问题。
主流共识：数学 Agent 不是单一模型，而是一套研究工作台，包含检索、符号计算、证明器、反模型构造、依赖图追踪。
六、新流程、分工与边界
新的人机协作流程：
数学家提出方向 → Agent 批量试探、生成候选猜想与草稿 → 人工筛选、校准语义 → 自动形式化翻译 + 机器核验 → 人工提炼数学洞察、构建理论框架 → 归档进形式化知识库
读书会重点警示的风险：
- 评价陷阱（Goodhart 定律）：如果只用 “证明数量、通过 Lean 的条数” 衡量数学产出，系统会优先刷容易形式化的问题，回避真正有数学洞见的难题；
- 责任归属：形式错误、翻译偏差、理解错位，最终学术责任仍由人类研究者承担；机器是审计员，不是作者；
- 理解危机：一条证明可以被 Lean 通过，但人类看不懂、无法内化、无法迁移，这种 “无理解证明” 的学术价值存疑，呼应 Thurston 的经典观点：数学进步的核心是理解，不只是证明。
七、适合与不适合的场景
✅ 适合：
- 批量探索同结构猜想、组合问题、参数扫描；
- 把已有的非形式证明转为可核验形式库；
- 辅助构造反例、计算复杂不变量、清理冗长技术性步骤；
- 给青年数学家提供 “草稿助手”，降低繁琐计算成本。
❌ 当前短板：
- 跨领域、需要长期统一构想、创造全新数学语言的重大突破，仍然高度依赖人；
- 高难度偏微分、几何分析中，假设与正则性的微妙语义很难自动对齐；
- 形式库覆盖不足的领域，翻译成本极高，甚至高于从头写证明。
【相关 FAQ】
问题 1：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，这期读书会主讲人是谁，核心议题是什么？
回答 1：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，主讲人为北大朱韬宇博士；核心议题是 AI 如何重塑数学研究范式，讨论数学智能体、形式化证明、N‑S 方程的语义保真、陶哲轩数学 2.0、丘成桐团队路线，以及人机分工与评价陷阱。
问题 2：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，读书会里提到的 “语义一致性 / 语义保真” 是什么意思？
回答 2：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，它指把自然语言的数学命题翻译成 Lean 这类形式语言时，要保证定义域、假设、量词、结论没有悄悄偏移；哪怕机器通过形式校验，如果翻译跑偏，证明的是另一个命题，这个结果在数学上无效。N‑S 方程就是用来展示这个难点的案例。
问题 3：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，陶哲轩在这期被提到的 “数学 2.0” 核心主张是什么？
回答 3：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，核心主张是 AI 用来增强人类理解而非替代理解；从过去一次深耕单个问题，升级为可以做大规模 “普查式” 数学探索，共建开放、社区治理的形式化数学知识库。
问题 4：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，数学智能体和普通数学大模型差别在哪？
回答 4：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，普通大模型侧重生成文本式解题或证明草稿，容易长程幻觉；数学智能体是一套闭环系统，可以自主拆分目标、调用检索、符号工具、定理证明器、构造反例、回溯失败路径，专门面向研究级的证明搜索与核验。
问题 5：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，读书会为什么提醒不能单纯用形式化证明数量评价数学研究？
回答 5：AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期，这是 Goodhart 定律在数学科研里的应用：一旦把 “通过 Lean 的证明条数” 设为优化指标，系统会优先挑简单、好翻译的题目，回避那些真正能带来新概念、新结构、新理解的困难问题，偏离数学研究本来的价值目标。
【参考资料】
[2026-11-07] 智源社区｜AI 时代的数学发展：数学研究的新范式｜AI for Math 读书会第二季第 6 期
[2026] Tao, T. Mathematics in the Age of AI, arXiv:2608.16753
[2026] Klowden & Tao, Mathematical Methods and Human Thought in the Age of AI
[2026] Abouzaid et al., First Proof Second Batch
[2026] Hubert et al., Olympiad-level formal mathematical reasoning with reinforcement learning, Nature
[1994] Thurston, On proof and progress in mathematics, Bulletin of the AMS
【免责声明】
本文是读书会公开分享的要点整理，不等于主讲原文；读书会观点属于学术讨论，不同数学家与研究团队对 “AI 在数学中的定位、证明价值、人机边界” 存在不同看法；形式化数学、数学 Agent 仍处在快速迭代阶段，不存在成熟通用的研究流水线；Lean、AlphaProof、SAIR 等项目各自有独立的开源协议与局限。