Ep137 Bv8Ghytff9W
导读：这期为什么是 AI for Math 的入口课
这期访谈主角洪乐潼 Carina Hong，是 Axiom Math 创始人，方向是 AI for Math：让 AI 参与数学问题求解、证明形式化、证明搜索和数学研究协作。视频标题里的关键词很多：Lean、数学天书中的证明、直觉、被创造与被发现、Axiom、Ken Ono、Neo Lab。这些词共同指向一个问题：如果 AI 要进入真正数学研究，它要学会的不只是解题，还要理解数学语言、证明结构、形式系统和数学家的直觉。
本期核心命题
AI for Math 的关键，不是让模型做更多竞赛题，而是把数学直觉、非形式证明、形式化语言、proof assistant 和机器验证接成闭环。Lean 不是装饰，而是把“看起来对”变成“机器可检查”的关键接口。
视觉策略说明
本视频是固定访谈画面，没有教学 slides、白板或产品演示。按本仓库播客标准，正文不重复插入人物帧；封面用于来源识别，正文用概念图、路线图和术语表承载教学内容。
本章小结
这期不是普通创业访谈，而是 AI for Math 的概念入口：它同时讨论数学哲学、形式化证明、Lean、创业路线、研究直觉和 Neo Lab 的资源结构。
讲义式导读：如何判断一个 AI for Math 系统是否靠谱
学习本期时，可以把“AI for Math 系统是否靠谱”拆成六个问题。第一，它能否准确理解数学对象和定理陈述，而不是只做自然语言 paraphrase。第二，它能否把非形式证明转成 Lean/Coq 等 proof assistant 可检查的形式。第三，它能否在证明失败时读取 goal state，并修复而不是重写一段幻觉文本。第四，它能否利用定理库，而不是每次从零开始。第五，它能否给数学家带来研究速度提升，而不只是做已知题。第六，它是否能解释证明为什么有意义。
六问法
一个 AI for Math 系统若只满足前两问，它更像 formalization 工具；若能满足第三、第四问，它开始具备 Agent 能力；若能满足第五、第六问，它才接近数学研究伙伴。
为什么这六问重要
它们把“AI 会不会数学”从模糊问题拆成可检查能力。理解对象对应语义能力；形式化对应语言与类型系统能力；读取 goal state 对应环境反馈；利用定理库对应检索和记忆；提升研究速度对应产品价值；解释意义对应数学审美。高标准 AI for Math 需要这些能力共同出现。
本章小结
这六问会贯穿后文。读者不必先懂 Lean 细节，也能用它判断不同 AI for Math 路线到底是在做题、做证明，还是在尝试进入真正研究。
数学是被发现的，还是被创造的
访谈早段讨论“被创造的与被发现的”。这是 AI for Math 的哲学底色。若数学是被发现的，AI 需要学习客观结构：素数、对称、拓扑、曲率和证明之间的稳定关系。若数学是被创造的，AI 需要学习人类如何选择定义、公理、记号和理论语言。现实中两者交织：数学对象有客观约束，数学语言和证明路径又由人创造。
图片资源缺失
\begin{figure}[H]
\centering
\includegraphics[width=0.92\textwidth]{math-created-discovered.png}
\caption{数学的两种视角：被发现的结构与被创造的语言。}
\end{figure}
读图：为什么 AI for Math 同时面对两层任务
左侧强调数学结构的客观性，右侧强调数学语言和公理系统的创造性。AI for Math 不能只做模式匹配，也不能只生成漂亮文字；它既要捕捉稳定结构，又要把推理写成可验证语言。
bounded attention 与 free attention
访谈中出现 bounded vs free attention 的说法，可以理解为数学思考的两种模式：bounded attention 围绕定义、条件、目标和已有工具局部推进；free attention 则允许联想、审美、类比和跳跃。数学研究需要在二者之间切换：形式化证明偏 bounded，猜想和直觉生成偏 free。
图片资源缺失
\begin{figure}[H]
\centering
\includegraphics[width=0.92\textwidth]{bounded-free-attention.png}
\caption{数学直觉中的 bounded attention 与 free attention。}
\end{figure}
读图：两种注意力分别服务什么
Bounded attention 适合证明检查、局部推理和 Lean 形式化；free attention 适合发现模式、提出猜想和跨领域类比。一个强 AI for Math 系统需要二者协同，而不是只会严格搜索或只会发散联想。
不要把直觉和形式化对立起来
数学直觉不是形式化的敌人。好的形式化系统把直觉变成可检查对象；好的直觉则帮助选择值得形式化的问题和证明路线。
本章小结
AI for Math 的难点来自双重结构：数学既像客观世界，又像人类语言工程。模型必须在自由联想和严格验证之间来回切换。
AI for Math 技术栈：从直觉到可验证证明
很多人把 AI for Math 简化成“模型会不会做数学题”。这只是最浅的一层。真正的目标，是让 AI 从问题、猜想、非形式推理出发，逐步走向形式化陈述、证明搜索、机器验证和人类反馈。
图片资源缺失
\begin{figure}[H]
\centering
\includegraphics[width=0.94\textwidth]{ai-for-math-stack.png}
\caption{AI for Math 技术栈：从问题到验证再到数学家反馈。}
\end{figure}
读图：AI for Math 不是单点模型能力
图中每一层都可能成为瓶颈：问题理解需要语义和背景知识；非形式推理需要直觉；形式化需要 Lean/Coq 语言；证明搜索需要定理库和 tactic；验证需要 proof assistant；最后还需要数学家判断方向和意义。
术语消化：AI for Math 关键词
| 术语 | 解决的问题 | 与本期关系 |
|---|---|---|
| Lean | 形式化数学语言和 proof assistant | 把自然语言证明转成机器可检查证明。 |
| Coq | 另一类 proof assistant | 说明形式化证明不止 Lean 一条路线。 |
| Tactic | 自动或半自动证明步骤 | 让模型能逐步构造可检查证明。 |
| Theorem Proving | 定理证明 | AI for Math 的核心任务之一。 |
| Verifier | 验证器 | 判断证明是否合法，避免“看起来对”的幻觉。 |
| Formalization | 形式化 | 把论文、定义、猜想写进可验证系统。 |
为什么 proof assistant 是关键
数学自然语言证明经常省略步骤，依赖读者背景和直觉。Proof assistant 要求每一步都符合规则。对 AI 来说，这是一种强反馈：生成的证明要么被 kernel 接受，要么失败并给出目标状态。这种反馈比主观评分更硬，也更适合训练和评估。
可验证性是 AI for Math 的护城河
数学是少数能提供强验证信号的高价值领域。Lean/Coq 等系统让模型输出不只是“像证明”，而是必须通过机器检查。这使 AI for Math 同时具备科学价值和工程可训练性。
本章小结
AI for Math 的技术栈包括直觉、形式语言、证明搜索和机器验证。真正困难的是把这些层连起来，而不是只在某一层做题。
把数学变成 Lean：形式化证明闭环
把数学变成 Lean，不是简单翻译。自然语言证明常常省略背景、跳步、依赖图形直觉或引用不明确的定理。Lean 需要明确对象类型、定理陈述、依赖、tactic 和每一步合法性。这让 AI 既有机会，也有约束。
图片资源缺失
\begin{figure}[H]
\centering
\includegraphics[width=0.92\textwidth]{lean-proof-loop.png}
\caption{从自然语言证明到 Lean 验证的闭环。}
\end{figure}
读图：Lean 闭环为什么适合训练
自然语言证明先被转成 formal statement，再生成 tactic 或 proof term，Lean kernel 检查是否合法。如果失败，系统返回 error/goal state，人或模型据此修复。这个闭环提供了比普通文本生成更强的训练反馈。
形式化的三类难点
第一是语义难点：自然语言里的“显然”“由此可得”需要展开。第二是库依赖难点：Lean 里定理、定义、lemma 的名字和使用方式必须准确。第三是搜索难点：证明空间巨大，模型需要决定先证哪个子目标、调用哪个 lemma、何时重写目标。
Lean 不会自动让模型懂数学
Lean 能验证证明是否合法，但不会替模型选择重要问题，也不会自动提供数学审美。AI for Math 还需要人类数学家的直觉、问题选择和理论品味。
数学天书中的证明
访谈标题提到“数学天书中的证明”，可以理解为数学中那些优雅、短小、仿佛来自天书的证明。AI 若只是暴力搜索，可能产出冗长证明；若能学习数学直觉和审美，才可能接近这类证明。形式化验证保证正确性，但优雅性仍需要审美评价。
正确性与优雅性
机器验证解决“对不对”，但不直接解决“好不好”。数学研究还关心证明是否解释了现象、是否揭示结构、是否可推广。AI for Math 的长期目标应同时追求正确性、可读性和洞察力。
本章小结
Lean 让证明变成可执行、可检查对象。AI for Math 的关键，是把自然语言直觉和机器验证闭环连接起来，同时不丢掉数学审美。
从题目求解到数学研究
AI for Math 可以分成不同层级：做题、形式化证明、证明补全、猜想生成、研究协作。越往后，越接近真正数学研究，也越难评估。竞赛题有答案，Lean 证明有 verifier，研究问题则需要判断“值不值得做”。
图片资源缺失
\begin{figure}[H]
\centering
\includegraphics[width=0.96\textwidth]{ai-for-math-roadmap.png}
\caption{从数学题到数学研究的 AI for Math 路线图。}
\end{figure}
读图：为什么越往右越难
题目求解通常有答案；形式化证明有 proof assistant 检查；证明补全有局部目标；猜想生成和研究协作则需要审美、方向判断和长期理论结构。越接近研究，越不能只靠 benchmark。
数学家的直觉
访谈后半段讨论“数学家的直觉”。直觉不是玄学，而是长期训练后对结构、反例、证明路线和审美的压缩判断。AI 可以通过大量数据和反馈学习模式，但是否能形成类似数学家直觉，取决于它是否能把形式化反馈、非形式推理和研究目标整合起来。
直觉可以被训练，但不等于数据拟合
数学直觉来自问题选择、失败经验、结构类比和审美判断。AI 可以从证明库、论文、交互反馈和数学家修正中学习，但需要长期闭环，而不是一次性监督数据。
登月要么成功，要么失败
访谈中“登月要么成功，要么失败”的表达，体现了 AI for Math 创业的高风险性质。数学研究不像普通应用，可以小步验证商业指标；它要么真的推动证明和发现能力，要么只是漂亮 demo。Axiom 这类 Neo Lab 的难度就在于：要同时做科学、产品、团队和融资。
AI for Math 的评估不能只看融资
大额融资和顶级数学家加入是信号，但不是结果。真正结果要看是否能产出可验证证明、加速数学家工作、形成可复用定理库和研究协作模式。
本章小结
AI for Math 的路线从做题走向研究协作。越靠近研究，越需要数学家的直觉、形式化系统和长期反馈，而不是单一 benchmark。
Axiom 与 Neo Lab：AI for Math 创业需要什么
视频描述中提到，Axiom 完成 2 亿美元 A 轮融资，估值 16 亿美元；Ken Ono 离开或暂停传统教授路径加入 Axiom 也引发关注。无论具体媒体叙事如何，这说明 AI for Math 已经从学术问题变成高资本密度 Neo Lab 问题。
图片资源缺失
\begin{figure}[H]
\centering
\includegraphics[width=0.92\textwidth]{ai-math-neolab.png}
\caption{AI for Math Neo Lab 的组成：数学家、形式化系统、模型训练、资金算力和产品目标。}
\end{figure}
读图：Neo Lab 不是普通创业公司
图中五个要素共同指向 Axiom 这类组织：顶级数学家网络提供问题和审美，Lean/Coq 提供形式化基础，模型训练提供自动化能力，资金算力支撑规模实验，产品目标把研究转成可用系统。
为什么数学家网络重要
数学数据不是普通网页数据。真正有价值的问题、证明路线、定理库组织和审美判断，往往掌握在数学家社区中。Ken Ono 这样的数学家加入，不只是背书，更可能带来问题选择、研究网络和验证标准。
AI for Math 的数据飞轮
如果系统能帮助数学家形式化证明、补全 lemma、发现反例，数学家又能反馈修正和评价，这就可能形成数据飞轮。没有数学家参与，模型很容易停留在题库和表面证明。
最不可能创业的创业者
访谈里洪乐潼谈到“最不可能创业的创业者”。这类 Neo Lab 和传统应用创业不同：创始人要理解数学、AI、形式化系统、研究组织和融资。它更像把研究院、模型团队和产品公司压缩成一个高密度组织。
研究导向创业的双重风险
如果太学术，产品和收入路径不清；如果太产品化，可能失去基础研究深度。AI for Math 需要在科学目标和工程落地之间保持张力。
本章小结
Axiom 代表一种新型 AI Lab：研究问题足够基础，资本密度足够高，团队需要同时连接数学家、形式化系统和模型训练。它不是普通 SaaS 创业，也不是传统学术实验室。
术语消化：本期关键词索引
| 术语 | 一句话解释 | 在本期中的作用 |
|---|---|---|
| AI for Math | 用 AI 帮助数学求解、证明、形式化和研究协作 | 全文核心方向。 |
| Lean | 形式化数学语言和 proof assistant | 把证明变成机器可检查对象。 |
| Proof Assistant | 帮助书写和验证形式证明的软件系统 | 提供强 verifier。 |
| Formalization | 把自然语言数学转成形式系统 | AI 与数学库连接的关键步骤。 |
| Tactic | proof assistant 中推进证明的策略命令 | 模型可以生成或搜索的动作。 |
| Verifier | 检查输出是否合法的机制 | 让训练和评估获得硬反馈。 |
| Bounded Attention | 受目标和定义约束的局部注意力 | 支撑严格证明和形式化。 |
| Free Attention | 开放联想和审美判断 | 支撑猜想和新证明路线。 |
| Neo Lab | 高资本密度、研究导向的新型 AI 实验室 | Axiom 的组织类型。 |
本章小结
本期术语围绕一个中心展开：如何把数学从人类直觉和自然语言，转成可验证、可训练、可协作的 AI 系统。
与前两期的连接
EP139 苏煜访谈讲 Agent 技术史，EP138 罗福莉访谈讲 Agent 范式如何改变模型实验室，EP137 洪乐潼访谈则把 AI 的前沿推进到数学研究。三期连起来，是从通用数字代理、模型实验室组织，到科学发现系统的连续图谱。
三期连读的主线
EP139 解释 Agent 为什么成为新范式；EP138 解释模型团队如何为 Agent 重配后训练和算力；EP137 解释 AI 如何进入数学这种高度形式化、可验证但又依赖直觉的领域。
本章小结
AI for Math 是 Agent 时代的一个高价值科学分支。它把工具使用、形式验证、长期推理和人类专家协作放进同一个问题里。
深水区：数学直觉、Lean 生态与研究协作
前面几章把 AI for Math 拆成了技术栈，但洪乐潼访谈真正有趣的地方在于：她并不把数学看成单纯的“题目集合”。数学研究里有审美、有失败、有长期投入，也有共同体认可。AI 如果只会在已知题库里生成答案，距离数学研究仍然很远；如果能帮助数学家发现结构、形式化证明、补全缺失 lemma、检验反例，它才真正进入研究过程。
为什么数学不是普通 NLP 任务
普通 NLP 任务常常允许语义近似：摘要可以有不同措辞，翻译可以有多个等价表达，聊天回答也允许风格差异。数学证明不同：一个关键条件漏掉，整个证明就可能失败。形式系统把这种严格性推到极致，要求每一个对象、类型、依赖和推理步骤都合法。
数学任务的特殊性
数学同时拥有强形式约束和强创造性。强形式约束来自 proof assistant 与定理验证；强创造性来自猜想、审美、定义选择和证明路线设计。AI for Math 必须同时处理这两端。
Lean 生态为什么重要
Lean 的价值不只是验证器，而是生态：mathlib 定理库、社区贡献、形式化风格、tactic 传统、教学材料和数学家参与。模型若要写 Lean 证明，需要理解库里有什么、定理如何命名、哪类 tactic 常用、失败目标如何解读。这和普通代码补全很像，但约束更严格。
Lean 与代码的相似和不同
相似处在于二者都有语法、类型、库、错误信息和可执行反馈；不同处在于 Lean 的目标不是运行程序，而是证明命题。程序可以靠测试覆盖常见情况，证明则必须满足所有情况。
Proof Search 的搜索空间
证明搜索不是线性生成。一个定理可能需要先构造中间 lemma，选择归纳变量，转换目标形式，调用已有定理，或先证明反例不存在。搜索空间巨大，错误路径也很多。AI 的优势在于可以并行尝试和利用语义先验；劣势在于容易生成看似合理但库中不可用的步骤。
证明搜索的常见失败
模型可能知道数学思路，却不知道 Lean 库里对应定理叫什么；也可能知道 tactic，却把目标变成更难的形式；还可能生成自然语言上成立但形式系统缺少前提的证明。失败信息本身就是训练数据。
本章小结
AI for Math 的核心不是“模型更聪明一点”，而是把数学研究拆成可反馈的闭环：直觉提出方向，形式化约束过程，验证器提供硬反馈，数学家判断意义。
Axiom 路线的关键判断：为什么要做研究型公司
Axiom 这样的 Neo Lab 不是普通应用公司。它要面对一个很深的产品悖论：数学研究的最终用户很少，短期商业化不如通用 AI 应用清晰；但一旦系统真正提高数学研究速度，它可能影响科学、工程、密码学、物理、材料和 AI 自身。高风险和高上限同时存在。
Ken Ono 事件的信号
媒体叙事喜欢讲“57 岁终身教授给 24 岁创始人打工”，但更值得关注的是信号本身：顶级数学家愿意把时间放到 AI for Math 上，说明他们认为这不是玩具。数学家加入带来的不是宣传价值，而是问题选择、研究审美、证明质量判断和社区连接。
为什么数学家不可替代
AI 可以生成证明候选，但数学家决定哪些问题重要、哪些证明有解释力、哪些方向值得投入。AI for Math 若脱离数学家共同体，很容易退化成题库自动化。
融资不是结果，而是 runway
Axiom 的大额融资说明资本愿意押注 AI for Math，但融资只是 runway。真正要验证的是：它能否构建可持续的定理库贡献、证明自动化工具、数学家工作流和研究协作产品。否则融资规模只会放大压力。
Neo Lab 的风险
研究型公司容易两头不靠：学术界认为它太商业，商业世界认为它太基础。要穿过这个夹缝，需要一个能被验证的中间产物，例如形式化证明效率提升、定理库增长、数学家协作平台或高价值研究突破。
本章小结
Axiom 的路线不是“做一个数学聊天机器人”，而是试图把数学家、形式化系统和模型训练组织成研究机器。它的风险和价值都来自这个定位。
从数学到更广义的科学发现
AI for Math 之所以重要，还因为数学是科学发现中最形式化、最可验证的一块。如果 AI 能在数学中形成“提出猜想--构造证明--机器验证--人类评价”的闭环，那么类似方法可能迁移到物理、材料、程序验证和算法发现。
为什么数学是试验场
数学有三个优势。第一，正确性可以被形式化系统强验证。第二，历史数据和定理库具有结构化积累。第三，数学家社区对优雅、解释力和重要性有清晰但难以量化的评价传统。这使它既适合机器训练，也能暴露机器训练的不足。
科学发现的三类反馈
数学提供形式验证；代码提供测试和运行反馈；实验科学提供观测和实验反馈。三者都是 AI 从语言生成走向真实发现的关键环境。EP139 的 Agent、EP138 的模型实验室、EP137 的 AI for Math，其实都在寻找可反馈环境。
人机协作的终局
AI for Math 的理想终局未必是“替代数学家”。更现实也更有价值的形态，是 AI 帮数学家形式化繁琐证明、搜索 lemma、发现反例、整理文献、提出候选猜想；数学家则负责问题品味、方向选择、解释和最终判断。这样，AI 成为研究伙伴，而不是单纯自动答题器。
从工具到伙伴
当 AI 只做局部步骤，它是工具；当 AI 能理解上下文、积累经验、提出候选方向并接受验证，它开始像研究伙伴。AI for Math 是这个转变的高难度样板。
本章小结
数学是 AI 进入科学发现的高价值试验场。它的强验证性让训练更清晰，它的审美和直觉又提醒我们：科学发现不能被简化成单一指标。
阅读地图：从 EP137 到后续队列
EP137 在Zhang Xiaojun AI 队列里的位置很特殊。EP140 和 EP138 更偏模型实验室与 Agent 产业范式；EP139 提供 Agent 技术史；EP137 则把问题推向科学研究与形式化证明。它是从“AI 改变生产力”到“AI 改变知识生产”的桥。
读者应该带走的五个问题
第一，AI 能否从题目求解走向真正的数学研究？第二，Lean 是否会成为 AI for Math 的主接口？第三，数学家直觉能否被模型学习，还是必须长期由人类提供？第四，Axiom 这类 Neo Lab 如何在基础研究和商业化之间找到中间产物？第五，AI for Math 的成功是否会反过来推动 AI 自身算法和理论进步？
本期与后续整理的关系
后续如果整理更多 AI for Science、机器人、世界模型或自动驾驶访谈，可以复用本期框架：先找可验证环境，再看人类专家反馈，再看模型是否能形成长期闭环。数学只是这个框架中验证最硬的一类场景。
本章小结
EP137 的价值在于拓展了 AI 队列的边界：从 Agent 产品和模型训练，进入数学和科学发现。它提醒我们，最难的 AI 应用往往同时需要形式验证和人类审美。
转写校正与术语标准化
本期没有平台字幕，正文基于 faster-whisper large-v3 CUDA 转写。数学和 AI 术语密集，自动转写会产生系统性误差，例如把 Lean 写成“令”或“林”，把 AI for Math 写成近似音，把 Carina/Hong/Verve Coffee 等专名误听，把 theorem proving、proof assistant、formalization 等术语拆散。生成讲义时必须做术语校正，否则读者会误解技术主线。
术语消化：常见转写误差修正表
| 标准术语 | 可能的转写误差 | 校正理由 |
|---|---|---|
| Carina Hong / 洪乐潼 | 洪乐同、洪乐童、Carina 音近误写 | 人名与 Axiom 背景相关，必须统一。 |
| Axiom | 公理、A型、Axium | 公司名；中文可解释为“公理”，但正文应保留英文。 |
| Lean | 令、林、line | proof assistant 名称，关系到形式化数学主线。 |
| AI for Math | Al for Math、AI for Mark | 本期核心方向。 |
| Proof Assistant | 证明助手、proof system 混用 | 指 Lean/Coq 这类验证系统。 |
| Formalization | 形式化、格式化混淆 | 指把数学写入形式系统，而不是排版格式化。 |
| Ken Ono | 小野肯、小野 Ken | 数学家专名，关联 Axiom 组织信号。 |
| Bounded / Free Attention | 注意力边界、自由注意力误译 | 这里是数学思考模式隐喻，不是 Transformer attention 机制本身。 |
自动转写不能直接当技术文本
访谈类材料尤其容易在专名、论文名、系统名上误转写。高标准笔记必须基于章节、上下文和外部公开资料做术语校正，不能逐字照搬自动字幕。
本章小结
转写只是原料，不是讲义。AI for Math 这种术语密集内容尤其需要先做术语标准化，再写结构化笔记。
AI for Math 的评估路线：从题库到研究贡献
如果要判断 AI for Math 是否真正进步，不能只看模型做了多少竞赛题。竞赛题有价值，因为答案清晰、反馈硬；但它只是入口。更高层次的评估应该看形式化证明通过率、定理库贡献、lemma 发现、反例构造、数学家协作效率和新研究方向的产生。
评估层级
| 层级 | 可测指标 | 局限 |
|---|---|---|
| 竞赛题求解 | 正确率、pass@k、解题时间 | 容易过拟合题库，不代表研究能力。 |
| 形式化补全 | Lean theorem 通过率、tactic 成功率 | 依赖定理库覆盖和题目选择。 |
| 证明生成 | 完整证明长度、可读性、验证通过率 | 正确不等于优雅，长证明可能没有洞察。 |
| 定理库贡献 | 新 lemma 数量、复用率、维护成本 | 需要社区接受，不只是机器生成。 |
| 研究协作 | 数学家节省时间、发现反例、提出猜想 | 难以标准化，但最接近真实价值。 |
评估路线的核心
AI for Math 的评估应从“答案正确”逐步走向“证明可验证”“证明有解释力”“定理库可复用”“数学家愿意协作”。越往后越难量化，但也越接近真正价值。
为什么这和 Agent 相关
AI for Math 看似是科学问题，实际上也是 Agent 问题：模型要进入 Lean 环境，读取 goal state，调用 tactic，观察错误，修复证明，再继续推进。这和 web agent、coding agent 的闭环非常相似，只是环境更形式化、反馈更硬。EP137 因此可以看作 EP139 Agent 技术史的一种科学版实例。
Lean 环境就是一种高质量 Agent 环境
Lean 提供明确状态、明确动作、明确验证和明确错误反馈。相比开放网页环境，它更严格；相比普通聊天，它更可训练。这使 AI for Math 成为研究 Agent 学习能力的理想试验场。
本章小结
AI for Math 的评估不能停在题库正确率。真正的路线，是从解题、形式化、证明生成，逐步走向定理库贡献和数学家协作。
附录：Lean 与 AI for Math 学习路线
| 阶段 | 学什么 | 为什么学 |
|---|---|---|
| 数学语言 | 命题、定义、lemma、proof、反例 | 理解自然语言证明如何组织。 |
| Lean 基础 | theorem、example、rw、simp、apply、exact、induction | 理解 proof assistant 的交互方式。 |
| Mathlib | 常用定理库、命名、搜索、依赖关系 | AI 证明离不开已有数学库。 |
| Autoformalization | 自然语言到 Lean statement | 连接论文/题目和形式系统。 |
| Proof Search | tactic 组合、goal state、错误修复 | 让模型能在验证器反馈下迭代。 |
| Human Collaboration | 数学家审美、问题选择、解释力 | 判断证明是否有意义，而不只是通过。 |
学习路线的意义
这张表把 AI for Math 的学习顺序从“先学模型”改成“先理解数学和形式系统”。对工程读者来说，Lean 基础和 proof search 是进入这一领域的最低门槛；对数学读者来说，autoformalization 和模型反馈是理解 AI 能力边界的入口。
本章小结
AI for Math 是跨学科路线：数学语言、形式系统、模型训练和人机协作缺一不可。学习路径越清楚，越不容易把它误解成“让模型多刷题”。
总结与延伸
核心结论
- AI for Math 不等于刷数学题，而是从问题、直觉、形式化到验证的完整系统。
- Lean/Coq 等 proof assistant 为 AI 提供硬反馈，使数学成为适合训练和评估的高价值领域。
- 数学直觉和形式验证不是对立关系，强系统需要同时拥有 free attention 和 bounded attention。
- Axiom 这类 Neo Lab 需要数学家网络、形式化系统、模型训练、资金算力和产品目标共同成立。
- AI for Math 的终点不是替代数学家，而是与数学家共建证明、定理库和研究路线。
开放问题
- AI 能否生成真正有审美和解释力的证明，而不只是长而正确的证明？
- Lean 形式化会成为数学研究主流接口，还是只服务部分领域？
- 数学家反馈如何规模化，才能形成 AI for Math 数据飞轮？
- Axiom 这类 Neo Lab 的产品形态会是 proof assistant、研究平台，还是数学家协作系统？
拓展阅读
- Lean theorem prover 与 mathlib：理解形式化数学的基础设施。
- Terence Tao、Kevin Buzzard 等关于 formalization 的公开讨论：理解数学社区为什么重视 Lean。
- AI theorem proving、autoformalization、proof search 相关论文：理解 AI for Math 的技术路线。
- EP139 和 EP138 笔记：把 AI for Math 放回 Agent 与模型实验室的更大图谱中。
最后的判断
AI for Math 的难点在于，它同时要求模型懂数学、会写形式语言、能接受机器验证、也能与数学家直觉协作。它是 AI 从“生产力工具”走向“科学发现伙伴”的关键试验场。