\documentclass[a4paper]{article}
\usepackage[fontset=fandol]{ctex}
\usepackage{amsmath, amssymb}
\usepackage{graphicx}
\usepackage[margin=2.35cm]{geometry}
\usepackage[most]{tcolorbox}
\usepackage{booktabs}
\usepackage{tabularx}
\usepackage{longtable}
\usepackage{array}
\usepackage{float}
\usepackage{xcolor}
\usepackage{hyperref}
\usepackage{fancyhdr}

\hypersetup{colorlinks=true, linkcolor=blue!55!black, urlcolor=blue!60!black}
\graphicspath{{./}{figures/}}
\setlength{\parskip}{0.55em}
\setlength{\parindent}{2em}
\setlength{\emergencystretch}{3em}
\renewcommand{\arraystretch}{1.18}

\newtcolorbox{knowledgebox}[1]{enhanced, colback=blue!5!white, colframe=blue!70!black, colbacktitle=blue!70!black, coltitle=white, fonttitle=\bfseries, title={#1}, sharp corners, breakable}
\newtcolorbox{importantbox}[1]{enhanced, colback=yellow!10!white, colframe=yellow!75!black, colbacktitle=yellow!75!black, coltitle=black, fonttitle=\bfseries, title={#1}, sharp corners, breakable}
\newtcolorbox{warningbox}[1]{enhanced, colback=red!5!white, colframe=red!70!black, colbacktitle=red!70!black, coltitle=white, fonttitle=\bfseries, title={#1}, sharp corners, breakable}

\pagestyle{fancy}
\fancyhf{}
\fancyfoot[C]{\thepage}
\fancyfoot[R]{\footnotesize\color{gray}\href{https://github.com/hqhq1025/ai-course-notes}{AI Course Notes}}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}

\newcommand{\videourl}{https://www.youtube.com/watch?v=bv8ghyTFF9w}
\newcommand{\repourl}{https://github.com/hqhq1025/ai-course-notes}

\begin{document}

\begin{titlepage}
\centering
{\Large 技术访谈笔记\par}
\vspace{1.0cm}
{\huge\bfseries 洪乐潼访谈：AI for Math、Lean 与数学直觉\par}
\vspace{0.6cm}
{\Large Zhang Xiaojun 对话洪乐潼 Carina Hong\par}
\vspace{0.4cm}
{\large 基于 Zhang Xiaojun Podcast 公开视频、GPU 转写稿与自制概念图整理\par}
\vspace{0.3cm}
{\large 2026-04-20\par}
\vspace{0.9cm}
\includegraphics[width=0.88\textwidth,height=0.42\textheight,keepaspectratio]{cover.jpg}\par
\vfill
\begin{tcolorbox}[width=0.92\textwidth, colback=black!2!white, colframe=black!55, sharp corners]
\textbf{视频标题}：137. 对洪乐潼的4小时访谈：AI for Math、把数学变成Lean、数学天书中的证明、直觉、被创造与被发现的\par
\textbf{视频频道}：Zhang Xiaojun Podcast\par
\textbf{视频时长}：04:24:17\par
\textbf{视频链接}：\href{\videourl}{\nolinkurl{\videourl}}\par
\textbf{素材说明}：YouTube 无可用字幕；正文基于 faster-whisper large-v3 CUDA 转写、视频章节、封面和自制教学图整理。固定访谈画面不在正文重复使用。\par
\textbf{项目主页}：\href{\repourl}{\nolinkurl{\repourl}}\par
\end{tcolorbox}
\end{titlepage}

\tableofcontents
\newpage

\section{导读：这期为什么是 AI for Math 的入口课}

这期访谈主角洪乐潼 Carina Hong，是 Axiom Math 创始人，方向是 AI for Math：让 AI 参与数学问题求解、证明形式化、证明搜索和数学研究协作。视频标题里的关键词很多：Lean、数学天书中的证明、直觉、被创造与被发现、Axiom、Ken Ono、Neo Lab。这些词共同指向一个问题：如果 AI 要进入真正数学研究，它要学会的不只是解题，还要理解数学语言、证明结构、形式系统和数学家的直觉。

\begin{importantbox}{本期核心命题}
AI for Math 的关键，不是让模型做更多竞赛题，而是把数学直觉、非形式证明、形式化语言、proof assistant 和机器验证接成闭环。Lean 不是装饰，而是把“看起来对”变成“机器可检查”的关键接口。
\end{importantbox}

\begin{knowledgebox}{视觉策略说明}
本视频是固定访谈画面，没有教学 slides、白板或产品演示。按本仓库播客标准，正文不重复插入人物帧；封面用于来源识别，正文用概念图、路线图和术语表承载教学内容。
\end{knowledgebox}

\subsection{本章小结}

这期不是普通创业访谈，而是 AI for Math 的概念入口：它同时讨论数学哲学、形式化证明、Lean、创业路线、研究直觉和 Neo Lab 的资源结构。


\section{讲义式导读：如何判断一个 AI for Math 系统是否靠谱}

学习本期时，可以把“AI for Math 系统是否靠谱”拆成六个问题。第一，它能否准确理解数学对象和定理陈述，而不是只做自然语言 paraphrase。第二，它能否把非形式证明转成 Lean/Coq 等 proof assistant 可检查的形式。第三，它能否在证明失败时读取 goal state，并修复而不是重写一段幻觉文本。第四，它能否利用定理库，而不是每次从零开始。第五，它能否给数学家带来研究速度提升，而不只是做已知题。第六，它是否能解释证明为什么有意义。

\begin{importantbox}{六问法}
一个 AI for Math 系统若只满足前两问，它更像 formalization 工具；若能满足第三、第四问，它开始具备 Agent 能力；若能满足第五、第六问，它才接近数学研究伙伴。
\end{importantbox}

\subsection{为什么这六问重要}

它们把“AI 会不会数学”从模糊问题拆成可检查能力。理解对象对应语义能力；形式化对应语言与类型系统能力；读取 goal state 对应环境反馈；利用定理库对应检索和记忆；提升研究速度对应产品价值；解释意义对应数学审美。高标准 AI for Math 需要这些能力共同出现。

\subsection{本章小结}

这六问会贯穿后文。读者不必先懂 Lean 细节，也能用它判断不同 AI for Math 路线到底是在做题、做证明，还是在尝试进入真正研究。

\section{数学是被发现的，还是被创造的}

访谈早段讨论“被创造的与被发现的”。这是 AI for Math 的哲学底色。若数学是被发现的，AI 需要学习客观结构：素数、对称、拓扑、曲率和证明之间的稳定关系。若数学是被创造的，AI 需要学习人类如何选择定义、公理、记号和理论语言。现实中两者交织：数学对象有客观约束，数学语言和证明路径又由人创造。

\begin{figure}[H]
\centering
\includegraphics[width=0.92\textwidth]{math-created-discovered.png}
\caption{数学的两种视角：被发现的结构与被创造的语言。}
\end{figure}

\begin{knowledgebox}{读图：为什么 AI for Math 同时面对两层任务}
左侧强调数学结构的客观性，右侧强调数学语言和公理系统的创造性。AI for Math 不能只做模式匹配，也不能只生成漂亮文字；它既要捕捉稳定结构，又要把推理写成可验证语言。
\end{knowledgebox}

\subsection{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}

\begin{knowledgebox}{读图：两种注意力分别服务什么}
Bounded attention 适合证明检查、局部推理和 Lean 形式化；free attention 适合发现模式、提出猜想和跨领域类比。一个强 AI for Math 系统需要二者协同，而不是只会严格搜索或只会发散联想。
\end{knowledgebox}

\begin{warningbox}{不要把直觉和形式化对立起来}
数学直觉不是形式化的敌人。好的形式化系统把直觉变成可检查对象；好的直觉则帮助选择值得形式化的问题和证明路线。
\end{warningbox}

\subsection{本章小结}

AI for Math 的难点来自双重结构：数学既像客观世界，又像人类语言工程。模型必须在自由联想和严格验证之间来回切换。

\section{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}

\begin{knowledgebox}{读图：AI for Math 不是单点模型能力}
图中每一层都可能成为瓶颈：问题理解需要语义和背景知识；非形式推理需要直觉；形式化需要 Lean/Coq 语言；证明搜索需要定理库和 tactic；验证需要 proof assistant；最后还需要数学家判断方向和意义。
\end{knowledgebox}

\subsection{术语消化：AI for Math 关键词}

\noindent\begin{tabularx}{\textwidth}{p{0.22\textwidth}p{0.32\textwidth}X}
\toprule
术语 & 解决的问题 & 与本期关系 \\
\midrule
Lean & 形式化数学语言和 proof assistant & 把自然语言证明转成机器可检查证明。 \\
Coq & 另一类 proof assistant & 说明形式化证明不止 Lean 一条路线。 \\
Tactic & 自动或半自动证明步骤 & 让模型能逐步构造可检查证明。 \\
Theorem Proving & 定理证明 & AI for Math 的核心任务之一。 \\
Verifier & 验证器 & 判断证明是否合法，避免“看起来对”的幻觉。 \\
Formalization & 形式化 & 把论文、定义、猜想写进可验证系统。 \\
\bottomrule
\end{tabularx}

\subsection{为什么 proof assistant 是关键}

数学自然语言证明经常省略步骤，依赖读者背景和直觉。Proof assistant 要求每一步都符合规则。对 AI 来说，这是一种强反馈：生成的证明要么被 kernel 接受，要么失败并给出目标状态。这种反馈比主观评分更硬，也更适合训练和评估。

\begin{importantbox}{可验证性是 AI for Math 的护城河}
数学是少数能提供强验证信号的高价值领域。Lean/Coq 等系统让模型输出不只是“像证明”，而是必须通过机器检查。这使 AI for Math 同时具备科学价值和工程可训练性。
\end{importantbox}

\subsection{本章小结}

AI for Math 的技术栈包括直觉、形式语言、证明搜索和机器验证。真正困难的是把这些层连起来，而不是只在某一层做题。

\section{把数学变成 Lean：形式化证明闭环}

把数学变成 Lean，不是简单翻译。自然语言证明常常省略背景、跳步、依赖图形直觉或引用不明确的定理。Lean 需要明确对象类型、定理陈述、依赖、tactic 和每一步合法性。这让 AI 既有机会，也有约束。

\begin{figure}[H]
\centering
\includegraphics[width=0.92\textwidth]{lean-proof-loop.png}
\caption{从自然语言证明到 Lean 验证的闭环。}
\end{figure}

\begin{knowledgebox}{读图：Lean 闭环为什么适合训练}
自然语言证明先被转成 formal statement，再生成 tactic 或 proof term，Lean kernel 检查是否合法。如果失败，系统返回 error/goal state，人或模型据此修复。这个闭环提供了比普通文本生成更强的训练反馈。
\end{knowledgebox}

\subsection{形式化的三类难点}

第一是语义难点：自然语言里的“显然”“由此可得”需要展开。第二是库依赖难点：Lean 里定理、定义、lemma 的名字和使用方式必须准确。第三是搜索难点：证明空间巨大，模型需要决定先证哪个子目标、调用哪个 lemma、何时重写目标。

\begin{warningbox}{Lean 不会自动让模型懂数学}
Lean 能验证证明是否合法，但不会替模型选择重要问题，也不会自动提供数学审美。AI for Math 还需要人类数学家的直觉、问题选择和理论品味。
\end{warningbox}

\subsection{数学天书中的证明}

访谈标题提到“数学天书中的证明”，可以理解为数学中那些优雅、短小、仿佛来自天书的证明。AI 若只是暴力搜索，可能产出冗长证明；若能学习数学直觉和审美，才可能接近这类证明。形式化验证保证正确性，但优雅性仍需要审美评价。

\begin{importantbox}{正确性与优雅性}
机器验证解决“对不对”，但不直接解决“好不好”。数学研究还关心证明是否解释了现象、是否揭示结构、是否可推广。AI for Math 的长期目标应同时追求正确性、可读性和洞察力。
\end{importantbox}

\subsection{本章小结}

Lean 让证明变成可执行、可检查对象。AI for Math 的关键，是把自然语言直觉和机器验证闭环连接起来，同时不丢掉数学审美。

\section{从题目求解到数学研究}

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}

\begin{knowledgebox}{读图：为什么越往右越难}
题目求解通常有答案；形式化证明有 proof assistant 检查；证明补全有局部目标；猜想生成和研究协作则需要审美、方向判断和长期理论结构。越接近研究，越不能只靠 benchmark。
\end{knowledgebox}

\subsection{数学家的直觉}

访谈后半段讨论“数学家的直觉”。直觉不是玄学，而是长期训练后对结构、反例、证明路线和审美的压缩判断。AI 可以通过大量数据和反馈学习模式，但是否能形成类似数学家直觉，取决于它是否能把形式化反馈、非形式推理和研究目标整合起来。

\begin{knowledgebox}{直觉可以被训练，但不等于数据拟合}
数学直觉来自问题选择、失败经验、结构类比和审美判断。AI 可以从证明库、论文、交互反馈和数学家修正中学习，但需要长期闭环，而不是一次性监督数据。
\end{knowledgebox}

\subsection{登月要么成功，要么失败}

访谈中“登月要么成功，要么失败”的表达，体现了 AI for Math 创业的高风险性质。数学研究不像普通应用，可以小步验证商业指标；它要么真的推动证明和发现能力，要么只是漂亮 demo。Axiom 这类 Neo Lab 的难度就在于：要同时做科学、产品、团队和融资。

\begin{warningbox}{AI for Math 的评估不能只看融资}
大额融资和顶级数学家加入是信号，但不是结果。真正结果要看是否能产出可验证证明、加速数学家工作、形成可复用定理库和研究协作模式。
\end{warningbox}

\subsection{本章小结}

AI for Math 的路线从做题走向研究协作。越靠近研究，越需要数学家的直觉、形式化系统和长期反馈，而不是单一 benchmark。

\section{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}

\begin{knowledgebox}{读图：Neo Lab 不是普通创业公司}
图中五个要素共同指向 Axiom 这类组织：顶级数学家网络提供问题和审美，Lean/Coq 提供形式化基础，模型训练提供自动化能力，资金算力支撑规模实验，产品目标把研究转成可用系统。
\end{knowledgebox}

\subsection{为什么数学家网络重要}

数学数据不是普通网页数据。真正有价值的问题、证明路线、定理库组织和审美判断，往往掌握在数学家社区中。Ken Ono 这样的数学家加入，不只是背书，更可能带来问题选择、研究网络和验证标准。

\begin{importantbox}{AI for Math 的数据飞轮}
如果系统能帮助数学家形式化证明、补全 lemma、发现反例，数学家又能反馈修正和评价，这就可能形成数据飞轮。没有数学家参与，模型很容易停留在题库和表面证明。
\end{importantbox}

\subsection{最不可能创业的创业者}

访谈里洪乐潼谈到“最不可能创业的创业者”。这类 Neo Lab 和传统应用创业不同：创始人要理解数学、AI、形式化系统、研究组织和融资。它更像把研究院、模型团队和产品公司压缩成一个高密度组织。

\begin{warningbox}{研究导向创业的双重风险}
如果太学术，产品和收入路径不清；如果太产品化，可能失去基础研究深度。AI for Math 需要在科学目标和工程落地之间保持张力。
\end{warningbox}

\subsection{本章小结}

Axiom 代表一种新型 AI Lab：研究问题足够基础，资本密度足够高，团队需要同时连接数学家、形式化系统和模型训练。它不是普通 SaaS 创业，也不是传统学术实验室。

\section{术语消化：本期关键词索引}

\begin{longtable}{p{0.23\textwidth}p{0.32\textwidth}p{0.36\textwidth}}
\toprule
术语 & 一句话解释 & 在本期中的作用 \\
\midrule
AI for Math & 用 AI 帮助数学求解、证明、形式化和研究协作 & 全文核心方向。 \\
Lean & 形式化数学语言和 proof assistant & 把证明变成机器可检查对象。 \\
Proof Assistant & 帮助书写和验证形式证明的软件系统 & 提供强 verifier。 \\
Formalization & 把自然语言数学转成形式系统 & AI 与数学库连接的关键步骤。 \\
Tactic & proof assistant 中推进证明的策略命令 & 模型可以生成或搜索的动作。 \\
Verifier & 检查输出是否合法的机制 & 让训练和评估获得硬反馈。 \\
Bounded Attention & 受目标和定义约束的局部注意力 & 支撑严格证明和形式化。 \\
Free Attention & 开放联想和审美判断 & 支撑猜想和新证明路线。 \\
Neo Lab & 高资本密度、研究导向的新型 AI 实验室 & Axiom 的组织类型。 \\
\bottomrule
\end{longtable}

\subsection{本章小结}

本期术语围绕一个中心展开：如何把数学从人类直觉和自然语言，转成可验证、可训练、可协作的 AI 系统。

\section{与前两期的连接}

EP139 苏煜访谈讲 Agent 技术史，EP138 罗福莉访谈讲 Agent 范式如何改变模型实验室，EP137 洪乐潼访谈则把 AI 的前沿推进到数学研究。三期连起来，是从通用数字代理、模型实验室组织，到科学发现系统的连续图谱。

\begin{importantbox}{三期连读的主线}
EP139 解释 Agent 为什么成为新范式；EP138 解释模型团队如何为 Agent 重配后训练和算力；EP137 解释 AI 如何进入数学这种高度形式化、可验证但又依赖直觉的领域。
\end{importantbox}

\subsection{本章小结}

AI for Math 是 Agent 时代的一个高价值科学分支。它把工具使用、形式验证、长期推理和人类专家协作放进同一个问题里。


\section{深水区：数学直觉、Lean 生态与研究协作}

前面几章把 AI for Math 拆成了技术栈，但洪乐潼访谈真正有趣的地方在于：她并不把数学看成单纯的“题目集合”。数学研究里有审美、有失败、有长期投入，也有共同体认可。AI 如果只会在已知题库里生成答案，距离数学研究仍然很远；如果能帮助数学家发现结构、形式化证明、补全缺失 lemma、检验反例，它才真正进入研究过程。

\subsection{为什么数学不是普通 NLP 任务}

普通 NLP 任务常常允许语义近似：摘要可以有不同措辞，翻译可以有多个等价表达，聊天回答也允许风格差异。数学证明不同：一个关键条件漏掉，整个证明就可能失败。形式系统把这种严格性推到极致，要求每一个对象、类型、依赖和推理步骤都合法。

\begin{importantbox}{数学任务的特殊性}
数学同时拥有强形式约束和强创造性。强形式约束来自 proof assistant 与定理验证；强创造性来自猜想、审美、定义选择和证明路线设计。AI for Math 必须同时处理这两端。
\end{importantbox}

\subsection{Lean 生态为什么重要}

Lean 的价值不只是验证器，而是生态：mathlib 定理库、社区贡献、形式化风格、tactic 传统、教学材料和数学家参与。模型若要写 Lean 证明，需要理解库里有什么、定理如何命名、哪类 tactic 常用、失败目标如何解读。这和普通代码补全很像，但约束更严格。

\begin{knowledgebox}{Lean 与代码的相似和不同}
相似处在于二者都有语法、类型、库、错误信息和可执行反馈；不同处在于 Lean 的目标不是运行程序，而是证明命题。程序可以靠测试覆盖常见情况，证明则必须满足所有情况。
\end{knowledgebox}

\subsection{Proof Search 的搜索空间}

证明搜索不是线性生成。一个定理可能需要先构造中间 lemma，选择归纳变量，转换目标形式，调用已有定理，或先证明反例不存在。搜索空间巨大，错误路径也很多。AI 的优势在于可以并行尝试和利用语义先验；劣势在于容易生成看似合理但库中不可用的步骤。

\begin{warningbox}{证明搜索的常见失败}
模型可能知道数学思路，却不知道 Lean 库里对应定理叫什么；也可能知道 tactic，却把目标变成更难的形式；还可能生成自然语言上成立但形式系统缺少前提的证明。失败信息本身就是训练数据。
\end{warningbox}

\subsection{本章小结}

AI for Math 的核心不是“模型更聪明一点”，而是把数学研究拆成可反馈的闭环：直觉提出方向，形式化约束过程，验证器提供硬反馈，数学家判断意义。

\section{Axiom 路线的关键判断：为什么要做研究型公司}

Axiom 这样的 Neo Lab 不是普通应用公司。它要面对一个很深的产品悖论：数学研究的最终用户很少，短期商业化不如通用 AI 应用清晰；但一旦系统真正提高数学研究速度，它可能影响科学、工程、密码学、物理、材料和 AI 自身。高风险和高上限同时存在。

\subsection{Ken Ono 事件的信号}

媒体叙事喜欢讲“57 岁终身教授给 24 岁创始人打工”，但更值得关注的是信号本身：顶级数学家愿意把时间放到 AI for Math 上，说明他们认为这不是玩具。数学家加入带来的不是宣传价值，而是问题选择、研究审美、证明质量判断和社区连接。

\begin{importantbox}{为什么数学家不可替代}
AI 可以生成证明候选，但数学家决定哪些问题重要、哪些证明有解释力、哪些方向值得投入。AI for Math 若脱离数学家共同体，很容易退化成题库自动化。
\end{importantbox}

\subsection{融资不是结果，而是 runway}

Axiom 的大额融资说明资本愿意押注 AI for Math，但融资只是 runway。真正要验证的是：它能否构建可持续的定理库贡献、证明自动化工具、数学家工作流和研究协作产品。否则融资规模只会放大压力。

\begin{warningbox}{Neo Lab 的风险}
研究型公司容易两头不靠：学术界认为它太商业，商业世界认为它太基础。要穿过这个夹缝，需要一个能被验证的中间产物，例如形式化证明效率提升、定理库增长、数学家协作平台或高价值研究突破。
\end{warningbox}

\subsection{本章小结}

Axiom 的路线不是“做一个数学聊天机器人”，而是试图把数学家、形式化系统和模型训练组织成研究机器。它的风险和价值都来自这个定位。

\section{从数学到更广义的科学发现}

AI for Math 之所以重要，还因为数学是科学发现中最形式化、最可验证的一块。如果 AI 能在数学中形成“提出猜想--构造证明--机器验证--人类评价”的闭环，那么类似方法可能迁移到物理、材料、程序验证和算法发现。

\subsection{为什么数学是试验场}

数学有三个优势。第一，正确性可以被形式化系统强验证。第二，历史数据和定理库具有结构化积累。第三，数学家社区对优雅、解释力和重要性有清晰但难以量化的评价传统。这使它既适合机器训练，也能暴露机器训练的不足。

\begin{knowledgebox}{科学发现的三类反馈}
数学提供形式验证；代码提供测试和运行反馈；实验科学提供观测和实验反馈。三者都是 AI 从语言生成走向真实发现的关键环境。EP139 的 Agent、EP138 的模型实验室、EP137 的 AI for Math，其实都在寻找可反馈环境。
\end{knowledgebox}

\subsection{人机协作的终局}

AI for Math 的理想终局未必是“替代数学家”。更现实也更有价值的形态，是 AI 帮数学家形式化繁琐证明、搜索 lemma、发现反例、整理文献、提出候选猜想；数学家则负责问题品味、方向选择、解释和最终判断。这样，AI 成为研究伙伴，而不是单纯自动答题器。

\begin{importantbox}{从工具到伙伴}
当 AI 只做局部步骤，它是工具；当 AI 能理解上下文、积累经验、提出候选方向并接受验证，它开始像研究伙伴。AI for Math 是这个转变的高难度样板。
\end{importantbox}

\subsection{本章小结}

数学是 AI 进入科学发现的高价值试验场。它的强验证性让训练更清晰，它的审美和直觉又提醒我们：科学发现不能被简化成单一指标。

\section{阅读地图：从 EP137 到后续队列}

EP137 在Zhang Xiaojun AI 队列里的位置很特殊。EP140 和 EP138 更偏模型实验室与 Agent 产业范式；EP139 提供 Agent 技术史；EP137 则把问题推向科学研究与形式化证明。它是从“AI 改变生产力”到“AI 改变知识生产”的桥。

\subsection{读者应该带走的五个问题}

第一，AI 能否从题目求解走向真正的数学研究？第二，Lean 是否会成为 AI for Math 的主接口？第三，数学家直觉能否被模型学习，还是必须长期由人类提供？第四，Axiom 这类 Neo Lab 如何在基础研究和商业化之间找到中间产物？第五，AI for Math 的成功是否会反过来推动 AI 自身算法和理论进步？

\begin{knowledgebox}{本期与后续整理的关系}
后续如果整理更多 AI for Science、机器人、世界模型或自动驾驶访谈，可以复用本期框架：先找可验证环境，再看人类专家反馈，再看模型是否能形成长期闭环。数学只是这个框架中验证最硬的一类场景。
\end{knowledgebox}

\subsection{本章小结}

EP137 的价值在于拓展了 AI 队列的边界：从 Agent 产品和模型训练，进入数学和科学发现。它提醒我们，最难的 AI 应用往往同时需要形式验证和人类审美。


\section{转写校正与术语标准化}

本期没有平台字幕，正文基于 faster-whisper large-v3 CUDA 转写。数学和 AI 术语密集，自动转写会产生系统性误差，例如把 Lean 写成“令”或“林”，把 AI for Math 写成近似音，把 Carina/Hong/Verve Coffee 等专名误听，把 theorem proving、proof assistant、formalization 等术语拆散。生成讲义时必须做术语校正，否则读者会误解技术主线。

\subsection{术语消化：常见转写误差修正表}

\noindent\begin{longtable}{p{0.24\textwidth}p{0.32\textwidth}p{0.35\textwidth}}
\toprule
标准术语 & 可能的转写误差 & 校正理由 \\
\midrule
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 机制本身。 \\
\bottomrule
\end{longtable}

\begin{warningbox}{自动转写不能直接当技术文本}
访谈类材料尤其容易在专名、论文名、系统名上误转写。高标准笔记必须基于章节、上下文和外部公开资料做术语校正，不能逐字照搬自动字幕。
\end{warningbox}

\subsection{本章小结}

转写只是原料，不是讲义。AI for Math 这种术语密集内容尤其需要先做术语标准化，再写结构化笔记。

\section{AI for Math 的评估路线：从题库到研究贡献}

如果要判断 AI for Math 是否真正进步，不能只看模型做了多少竞赛题。竞赛题有价值，因为答案清晰、反馈硬；但它只是入口。更高层次的评估应该看形式化证明通过率、定理库贡献、lemma 发现、反例构造、数学家协作效率和新研究方向的产生。

\subsection{评估层级}

\noindent\begin{longtable}{p{0.22\textwidth}p{0.35\textwidth}p{0.34\textwidth}}
\toprule
层级 & 可测指标 & 局限 \\
\midrule
竞赛题求解 & 正确率、pass@k、解题时间 & 容易过拟合题库，不代表研究能力。 \\
形式化补全 & Lean theorem 通过率、tactic 成功率 & 依赖定理库覆盖和题目选择。 \\
证明生成 & 完整证明长度、可读性、验证通过率 & 正确不等于优雅，长证明可能没有洞察。 \\
定理库贡献 & 新 lemma 数量、复用率、维护成本 & 需要社区接受，不只是机器生成。 \\
研究协作 & 数学家节省时间、发现反例、提出猜想 & 难以标准化，但最接近真实价值。 \\
\bottomrule
\end{longtable}

\begin{importantbox}{评估路线的核心}
AI for Math 的评估应从“答案正确”逐步走向“证明可验证”“证明有解释力”“定理库可复用”“数学家愿意协作”。越往后越难量化，但也越接近真正价值。
\end{importantbox}

\subsection{为什么这和 Agent 相关}

AI for Math 看似是科学问题，实际上也是 Agent 问题：模型要进入 Lean 环境，读取 goal state，调用 tactic，观察错误，修复证明，再继续推进。这和 web agent、coding agent 的闭环非常相似，只是环境更形式化、反馈更硬。EP137 因此可以看作 EP139 Agent 技术史的一种科学版实例。

\begin{knowledgebox}{Lean 环境就是一种高质量 Agent 环境}
Lean 提供明确状态、明确动作、明确验证和明确错误反馈。相比开放网页环境，它更严格；相比普通聊天，它更可训练。这使 AI for Math 成为研究 Agent 学习能力的理想试验场。
\end{knowledgebox}

\subsection{本章小结}

AI for Math 的评估不能停在题库正确率。真正的路线，是从解题、形式化、证明生成，逐步走向定理库贡献和数学家协作。


\section{附录：Lean 与 AI for Math 学习路线}

\noindent\begin{longtable}{p{0.20\textwidth}p{0.35\textwidth}p{0.36\textwidth}}
\toprule
阶段 & 学什么 & 为什么学 \\
\midrule
数学语言 & 命题、定义、lemma、proof、反例 & 理解自然语言证明如何组织。 \\
Lean 基础 & theorem、example、rw、simp、apply、exact、induction & 理解 proof assistant 的交互方式。 \\
Mathlib & 常用定理库、命名、搜索、依赖关系 & AI 证明离不开已有数学库。 \\
Autoformalization & 自然语言到 Lean statement & 连接论文/题目和形式系统。 \\
Proof Search & tactic 组合、goal state、错误修复 & 让模型能在验证器反馈下迭代。 \\
Human Collaboration & 数学家审美、问题选择、解释力 & 判断证明是否有意义，而不只是通过。 \\
\bottomrule
\end{longtable}

\begin{knowledgebox}{学习路线的意义}
这张表把 AI for Math 的学习顺序从“先学模型”改成“先理解数学和形式系统”。对工程读者来说，Lean 基础和 proof search 是进入这一领域的最低门槛；对数学读者来说，autoformalization 和模型反馈是理解 AI 能力边界的入口。
\end{knowledgebox}

\subsection{本章小结}

AI for Math 是跨学科路线：数学语言、形式系统、模型训练和人机协作缺一不可。学习路径越清楚，越不容易把它误解成“让模型多刷题”。

\section{总结与延伸}

\subsection{核心结论}

\begin{enumerate}
\item AI for Math 不等于刷数学题，而是从问题、直觉、形式化到验证的完整系统。
\item Lean/Coq 等 proof assistant 为 AI 提供硬反馈，使数学成为适合训练和评估的高价值领域。
\item 数学直觉和形式验证不是对立关系，强系统需要同时拥有 free attention 和 bounded attention。
\item Axiom 这类 Neo Lab 需要数学家网络、形式化系统、模型训练、资金算力和产品目标共同成立。
\item AI for Math 的终点不是替代数学家，而是与数学家共建证明、定理库和研究路线。
\end{enumerate}

\subsection{开放问题}

\begin{itemize}
\item AI 能否生成真正有审美和解释力的证明，而不只是长而正确的证明？
\item Lean 形式化会成为数学研究主流接口，还是只服务部分领域？
\item 数学家反馈如何规模化，才能形成 AI for Math 数据飞轮？
\item Axiom 这类 Neo Lab 的产品形态会是 proof assistant、研究平台，还是数学家协作系统？
\end{itemize}

\subsection{拓展阅读}

\begin{itemize}
\item Lean theorem prover 与 mathlib：理解形式化数学的基础设施。
\item Terence Tao、Kevin Buzzard 等关于 formalization 的公开讨论：理解数学社区为什么重视 Lean。
\item AI theorem proving、autoformalization、proof search 相关论文：理解 AI for Math 的技术路线。
\item EP139 和 EP138 笔记：把 AI for Math 放回 Agent 与模型实验室的更大图谱中。
\end{itemize}

\begin{importantbox}{最后的判断}
AI for Math 的难点在于，它同时要求模型懂数学、会写形式语言、能接受机器验证、也能与数学家直觉协作。它是 AI 从“生产力工具”走向“科学发现伙伴”的关键试验场。
\end{importantbox}

\end{document}
