一个22年前的数学猜想，两组人在8天内各自解开了

但"很可能正确"和"正确"之间，隔着的远比你以为的多。

今年的 3 月，陶哲轩在 Dwarkesh Podcast 上聊到 AI 和数学研究的关系。他讲了开普勒的故事，开普勒花了好几年穷举各种关于行星轨道的猜想，大部分是错的，但是他每一步都拿第谷·布拉赫的精密观测数据去核实。陶哲轩说想法可以海量，但是必须配上等量的验证，"Otherwise, it's slop."

四个月后，一件事把这句话从播客金句变成了一道现实问题，先来慢慢细说。

当特征值说谎

1883 年，奥斯本·雷诺在曼彻斯特大学的实验室里往一根玻璃管里注水，他在入水口处加了一缕染料。在低流速时，染料笔直穿过管子。他慢慢的拧动大阀门，直到某个临界点，染料线突然的碎裂，然后弥散成了一团混沌。

层流变成了湍流。

图注：雷诺 1883 年论文中的实验装置和染料形态。

这个实验是流体力学教科书里的经典场景。

但是很少有教科书会把话说到这一步：

圆管中的层流剪切流（Poiseuille flow），在线性稳定性分析的意义上， 对任意雷诺数都是稳定的， 所有特征值的实部永远为负。

按照特征值的判决来说，管道里的水是永远不该失稳的。

现实显然是不遵从这个判决的，那问题出在哪里？

答案就藏在特征向量的正交性里，当矩阵是"正规"的（ ），特征向量正交，谱定理成立：

特征值是系统行为的完整画像。但是线性化剪切流中遇到的算子一般高度非正规，特征向量严重歪斜，甚至近乎平行。

即使是特征值全部稳定，这些非正交的模态之间可以在短时间内相长干涉（constructive interference），把扰动的幅值显著放大，在放大结束后，系统才按特征值指数律慢慢衰减回去。

这叫瞬态增长（Transient Growth）。

Meseguer 和 Trefethen（2003）把线性化圆管流算子的计算推到了雷诺数 的量级。

结果显示，最大瞬态放大因子随雷诺数线性增长（速度范数按 ，能量按 ）。按照论文中的渐近缩放外推， 时速度范数的最大放大约为十几倍。

十几倍看着不多，但是如果初始扰动的幅度和结构恰好落在敏感区间内，这个放大足以把扰动推进非线性效应开始介入的振幅范围。

瞬态增长为管道流在低雷诺数下的转捩提供了一种可能的机制。不过真实的转捩要远比这复杂，低雷诺数下的湍流斑块（turbulent puffs）可以自行衰减，持续湍流有其统计意义上的临界点（Avila 等人，Science 2011）。管道流的转捩不是一条简单的因果链。

只是数学能确切告诉我们的只有一件事：特征值描述的是渐近行为，对有限时间内的瞬态放大"盲"。

图注：示意：非正规系统中的扰动可能先放大，再衰减。

要控制非正规矩阵在有限时间内的行为，需要一个比特征值更精确的工具。2004 年，法国数学家 Michel Crouzeix 提出了一个猜想，这类工具存在一个绝对的、不可改进的上界。

数值域与 Crouzeix 猜想

这个工具叫数值域（Numerical Range）。对任意 阶复矩阵 ，它的数值域定义为：

让单位向量 遍历 中所有方向，把 画在复平面上，所有这些点构成的集合就是数值域。

数值域有两个立刻可用的性质。

第一，Toeplitz-Hausdorff 定理保证 恒为凸集——不管矩阵长什么样，数值域在复平面上永远是一块没有凹角的区域。

第二， 的所有特征值都落在 内部或边界上，数值域是比谱更大的一块地盘。

它和动力系统的联系也是很直接的。

对线性系统 ，取单位状态 时，范数平方的瞬时变化率满足 ，其最大值由 的实部边界给出。数值域直接控制着归一化瞬时增长率的上界。

Crouzeix 猜想说：

对任意 阶复矩阵 （ 不限）和任意在 的某个邻域上全纯的函数 ，

其实说白了不管矩阵多大、非正规性多强，只要算出数值域，看函数在数值域上的最大值，乘以 2，矩阵函数的算子范数一定不超过这个数。

而且 2 不可能更小。 这一点可以用最简单的非正规矩阵动手算出来。值得展开算一遍，因为这是本文唯一展开完整手算的部分。

幂零 Jordan 块：

先看特征值。 的特征多项式是 ，两个特征值都是 0，谱半径为零。只看特征值的话，这个矩阵似乎是"什么都不做"。

但如果算一下算子范数。对任意向量 ， ，所以 ，即 。

反过来，取 ： ，范数恰好是 1，所以 。两边一合， 。特征值说"什么都不做"，算子范数说"它能把一个单位向量完整地搬到另一个方向"，这就是非正规矩阵的欺骗性。

再算数值域。对单位向量 ，Rayleigh 商 。让 和相位差跑遍所有取值，这个值在复平面上扫出以原点为圆心、半径 的闭圆盘：

现在代入猜想。取 ：

• • 左边：

• • 右边：

等号严格取到。常数 不可能比 2 更小，因为这个最简单的 矩阵已经把下界锁死了。

几何直觉是这样的： 的数值域只是半径 的圆盘，但算子范数是 1，数值域画出的地盘远小于矩阵实际的放大能力。

猜想里说的是这种低估最多差一个因子 2。 恰好把这个因子用满了。

但是证明所有矩阵、所有维度、所有函数都不超过 2？

这是一个全称命题，维数不设上限，函数只要求在数值域邻域全纯，矩阵完全任意。一个反例就能推翻，但是要证明永远找不到反例，困难量级完全不是一个level了。

但证明所有矩阵、所有维度、所有函数都不超过 2？这是一个全称命题：维数不设上限，函数只要求在数值域邻域全纯，矩阵完全任意。一个反例就能推翻，但要证明永远找不到反例，困难量级完全不同。

22 年的僵局

猜想提出后数值分析和算子理论这两个圈子的人前前后后攻了 22 年。

2007 年，Crouzeix 本人先给出了第一个通用上界 。

2017 年，他和 Palencia 用复分析中的边界积分技术把常数压到了

然后就卡住了，近十年里，没有人能把维数无关的通用上界再往下压。

看着像估计做得不够紧，实际上已经到头了。

Lorist 和 Schwenninger 在论文中展示了旧框架的代数瓶颈：

Crouzeix-Palencia 的方法只用了 这一个幂次的估计。在归一化 的条件下，令 ，旧论证由此推出的不等式是

解出来恰好是 。估计做得并不粗糙，这就是只用一个幂次的老方法能走到的尽头了。

要突破这个天花板，必须想办法同时利用所有幂次 的信息。

2026 年 7 月，僵局打破了，而且是两组人各自独立做到的。

两条路线

2026 年 7 月 27 日，金山木在 Preprints.org 上发布了预印本。

8 天后，代尔夫特理工大学的 Emiel Lorist 和屯特大学的 Felix Schwenninger 在 arXiv 上发布了 A solution to Crouzeix's conjecture（初版 5 页，修订版 7 页）。

两篇论文用截然不同的工具，独立地给出了同一个结论，常数就是 2。

金山木路线延续了 Crouzeix-Palencia 2017 年的边界积分框架，但是做了一个关键的推广：

把经典框架中的单一对称积分恒等式扩展到完整的 Cayley 变换族，然后在矩阵值 Herglotz 核（matrix-valued Herglotz kernel）的特定几何点上采样。这一步使得旧框架中无法消去的修正项在代数结构中精确抵消，最终把问题归结为两个有序加权 Gram 矩阵的半正定比较，直接锁定常数 2。

Lorist–Schwenninger 路线从算子伸缩理论（dilation theory）切入。他们证明了一个引理：如果算子 的每个幂次 都可以写成"某个压缩算子的 2-伸缩减去一个误差项 "的形式，而且误差项在所有 上一致有界、同时与 交换，那么 。

老的框架只用了 。他们把 Crouzeix-Palencia 的边界积分表示应用到所有幂次 上，验证了误差项满足引理的两个条件，直接拿到 。

两条路线独立收敛到同一个结论，大幅提高了可信度。但独立路线仍可能共同依赖某个已有结论中的隐藏假设，也可能各自存在不同的错误。独立收敛提高可信度，不替代逐篇审计。

Crouzeix 本人、康奈尔大学的 Alex Townsend 和华盛顿大学的 Anne Greenbaum 审阅了金山木的手稿。

Townsend 和 Greenbaum 在署名评述中的措辞是 "thoroughly checked and believe … correct"，认真检查，并相信证明是正确的。这算是强背书了，但不是正式同行评议的结论。

到本文截稿时（2026 年 8 月下旬），两篇预印本均未经过正式的同行评议。

AI 做了什么：公开材料里能读到的

金山木是北京协和医院神经外科的住院医师，同时也是博士后研究员。他本科在北京大学学地质学，后来转入协和医学院读临床医学，获医学博士。他在临床研究中做经颅超声课题时用到了矩阵分析，由此接触到 Crouzeix 猜想。

他用 OpenAI 的 5.6-Sol 模型，在 Work 模式下跑了大概 16 小时的自主推理。

据 Townsend 和 Greenbaum 的评述，他把 OpenAI 此前为 Cycle Double Cover 猜想设计的提示词方法论改造后用在了 Crouzeix 猜想上。

他在 GitHub 上公开了完整的任务提示词（crouzeix_conjecture_prompt.txt）。这是一份统一的 meta-prompt，核心约束包括：

• • 禁止使用公共网络、外部文件、旧对话和项目上下文（但允许模型调用自身的数学知识）

• • 维护多条并行的策略路线（branching portfolio），禁止过早收敛到单一路径

• • 对候选引理尝试寻找反例做对抗审计

• • 输出要求是严格、独立、完整可编译的英文 LaTeX 证明

关于人机分工，金山木论文 v4 的 AI 声明和 Townsend-Greenbaum 的署名评述确认：模型提供了关键的采样思路，并协助了文稿表达、文献整理和排版；关键定理来自金山木未干预的约 16 小时自主运行；作者本人承担全部数学正确性和引文完整性的最终责任。

图注：仓库公开的任务提示词与对话记录页。

仓库近期新增了公开对话记录（conversation-019f7059-public/），包含 13 个线程、170 条模型回复、916 条 agent 间消息和 9173 项形式化推理条目，总计约 5.5 MB。

记录中可以看到模型完成了证明撰写、Lean 4 编译和多轮对抗审计。但是公开的是脱敏后的对话和推理摘要，不含底层隐藏推理和线下人工核验过程。

Lorist 和 Schwenninger 在论文 v2 的 AI 声明中写道，他们用 5.6 Sol Pro 回顾已有的证明思路并寻找对 估计的改进，最终的证明由作者独立完成、验证和撰写。

两组人都用了 AI，但是最终的数学责任都由作者本人来承担。

"找不到错误"不等于"已经正确"

这件事值得我们静下心来想想的，不是两篇预印本本身。

2026 年 2 月，一批数学家发起了 First Proof 项目：选出 10 道横跨不同分支的未公开研究级数学问题，每道题的出题人手里有一份不超过 5 页的解答。

这套基准的目的是测试 AI 系统能不能独立解决研究级的数学问题。

OpenAI 作为参与者，用内部推理模型对全部 10 道题提交了候选解。综合出题人和外部数学家的反馈，OpenAI 判断其中 5 道的候选解很可能正确。

但 Problem 2 的结果反转了。

OpenAI 最初判断 Problem 2 的候选解很可能正确。后来出题人的详细反馈和同行的深入审查揭出了错误，OpenAI 随后公开更正了判定。

OpenAI 写道："Our initial submission for Problem 2 was evaluated as likely correct, but subsequent feedback and detailed examination showed the proof contained errors and is incorrect."

图注：OpenAI 说明 First Proof 第 2 题后来被改判为不正确。

这个案例说得很清楚，"很可能正确"和"正确"之间的距离，远比字面上看起来的要大。

形式化验证：杜绝跳步，但杜绝不了错译

金山木在 GitHub 上开源了 Lean 4 形式化验证模块。

"形式化验证"这个词近年在数学界出现的频率越来越高，但是它到底做了什么、不做什么，很多人并不清楚。

Lean 4 是当前数学界主流的交互式定理证明器之一。

它把数学命题翻译成一套基于依值类型论（Dependent Type Theory）的形式语言，然后由编译器逐步做严格的类型检查（Type Checking）。

每一步推导都必须在类型层面自洽，如果你在某一步隐式假设了一个未声明的条件，编译器会拒绝编译。

在没有 sorry 占位符、没有非预期公理、信任 Lean 内核且定理陈述准确形式化的前提下，编译通过意味着证明在该公理系统内逻辑上没有漏洞。

仓库中公开的公理审计报告（AXIOM_AUDIT.md）显示：

• • 定理 crouzeix_conjecture 依赖的公理仅为 Lean 4 / Mathlib 的标准基础公理（ propext 、 Classical.choice 、 Quot.sound ），没有自定义公理或非标准扩展

• • 0 个 sorry 占位符， sorry 是 Lean 中的"我先跳过这步"标记，编译器会放行但逻辑链在此断开。扫描结果为零，意味着没有被跳过的步骤

这些是仓库的公开可审计声明。

仓库自述的形式化覆盖范围已经不小了，包括有限矩阵的主定理端点和多个特殊情形。

但是他没有独立构建整套 Lean 工程，不对这些声明的完整性和正确性做保证。要从外部确认形式化的可信度，至少还需要知道：

• 1. Lean 代码中的定理陈述是否准确表达了原论文的数学命题？翻译过程中有没有无意中改变了假设条件？

• 2. 形式化覆盖了多少关键引理？是否与论文中的完整证明链条一一对应？

• 3. 第三方能否在标准环境下独立构建整套 Lean 工程并复现审计结果？

形式化验证能杜绝逻辑跳步，但不能判断形式化目标本身是否准确对应原始的数学问题，后者仍然需要领域专家的语义判断。

形式化验证和同行评议，一个负责管逻辑链完整，另一个来管数学内容对不对，谁也替代不了谁。

稀缺品正在转移

回过头来说这件事。

金山木的这个事 AI 做了什么，公开记录里现在已经能看到相当多的细节（前文已有详述）。比"AI 是否在思考"这个定义不清的问题更值得关注的，是一个结构性趋势：

候选证明的生产成本正在大幅下降。一位非数学科班的医生，用设计得当的提示词和大概 16 小时的模型运行时间，获得了一份完整的候选证明，包括证明撰写、Lean 4 编译和多轮自审。两位资深算子理论学者也用了 5.6 Sol 做策略探索。

但是生产候选证明是一回事，确认候选证明正确是另一回事。

同行评议、形式化验证、独立路线核验，这些认证机制的成本并没有同步下降。

Crouzeix 本人、Townsend、Greenbaum 认真检查了金山木的手稿并表示相信证明正确，但这还是非正式的专家判断，不是正式同行评议的结论。

Lean 4 形式化需要专业工程投入，两条独立路线收敛到同一个结论提高了可信度，但独立不等于相互认证。

First Proof 的 Problem 2 也已经告诉我们，初始评估认为正确的候选证明，在深层审查中仍然可能被推翻。

候选证明的生产已经被加速了。

可信结论的认证，还没有。

2026 年 7 月，陶哲轩在国际数学家大会（ICM）做了题为 Mathematics in the age of AI 的公开演讲。

他把当下的局面称为数学的"第二次基础危机"，第一次是一百年前，集合论的悖论逼着数学家把推理的基础显式化；第二次是现在，AI 让证明从稀缺变成了过剩，迫使数学界重新回答一个问题：什么才算知道了一个定理。

Crouzeix 猜想的这个故事可以说是刚好踩在这道缝上了。

本文涉及的两篇预印本均尚未通过正式同行评议。

金山木：The Numerical Range Is a 2-Spectral Set，Preprints.org 202607.1919。

Lorist–Schwenninger：A solution to Crouzeix's conjecture，arXiv:2608.03841（v2，7 页）。

金山木的任务提示词、Lean 4 验证模块和公理审计报告开源于 GitHub：jinshanmu/CrouzeixConjecture。

First Proof 基准项目：1stproof.org。