🔢 mathematics

The continuous functional calculus in Lean

本文记录了在任何证明助手中的连续泛函演算的首次形式化，详细阐述了其在 Lean 的 Mathlib 库中的实现、底层的数学理论，以及确保对数学界易用性的关键设计决策。

原作者： Anatole Dedecker, Jireh Loreaux

发布于 2026-06-08

📖 1 分钟阅读🧠 深度阅读

原作者： Anatole Dedecker, Jireh Loreaux

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下你是一位在极其复杂、高科技厨房里工作的顶级大厨。这个厨房代表了 C*-代数 的世界，这是数学的一个分支，涉及处理算子（就像是转换数据的机器），这些算子极其难以直接理解。

你正在阅读的论文是由两位大厨 Anatole 和 Jireh 撰写的报告，他们刚刚构建了一个全新的、革命性的厨房工具，叫做连续函数演算（Continuous Functional Calculus）。他们还建立了一本数字食谱（使用一种名为 Lean 的编程语言），教计算机如何完美地使用这个工具。

以下是他们所做工作的简单介绍。

1. 问题所在：“黑盒”机器

在这个数学厨房中，你经常会遇到一个特殊的机器（元素 $a$ ），它在做一些复杂的事情。你想对它进行一些新的操作，比如求它的平方根，或者应用一个复杂的曲线。

在过去，要做到这一点，你必须把机器拆解开，理解它的内部齿轮（它的“谱”），然后重新组装它。这就像是为了改变一锅汤的味道，而去拆解整个锅，分析其中每一个分子的化学成分，然后再重新组装起来。这很慢，容易出错，而且需要拥有化学博士学位才能完成一个简单的改变。

2. 解决方案：“魔法标签”

连续函数演算是一个魔法标签。你不需要拆解机器，只需在上面贴一个标签，写上：“对我应用这个函数 $f$ ”。

旧方法： “我需要计算这个机器的平方根。我必须首先证明这个机器是正规的（normal），找到它的内部谱，证明平方根函数在那个谱上是连续的，然后重建这个机器。”
新方法： “我有一个机器 $a$ 。我想应用函数 $f(x) = \sqrt{x}$ 。我只需要写下 $f(a)$ 。”

论文解释了作者如何在 Lean 中构建了这个“魔法标签”系统的数字版本。他们不仅编写了数学逻辑，还设计了接口，使得人类（或计算机）可以轻松使用该工具，而不会被技术细节困住。

3. 设计理念：“先写，后想”

在编写数学程序时，最大的挑战之一是计算机是非常严苛的。如果你要求计算机计算 $1/0$ ，它会崩溃。如果你尝试对一个不是“正规”的机器应用函数，它可能会崩溃。

作者决定使用一种他们称之为**“垃圾值”（Junk Values）**的策略。

类比： 想象一台自动售货机。如果你投入硬币并按下“苏打水”，它会给你一瓶苏打水。如果你按下了“苏打水”但机器坏了，普通的售货机可能会爆炸或报错。
Lean 的方法： 作者编写的机器使得，如果你对着一台坏掉的机器按下“苏打水”，它只会给你一个虚拟的苏打水（一个“垃圾值”，比如 0）。它不会崩溃，它只会说：“这里有一瓶苏打水，但它只是个占位符。”
为什么这有帮助： 这允许数学家编写长而复杂的公式（食谱），而无需在每一步都停下来检查该步骤是否有效。他们可以先写完整个食谱，只在需要证明最终结果是否正确时，才去检查具体步骤的有效性。这使得工作效率更高，也减少了挫败感。

4. “通用适配器”（类）

作者意识到，这个“魔法标签”工具需要在不同的厨房中工作：

复数（标准厨房）。
实数（更简单的厨房）。
非负数（一个不能有负数食材的厨房）。

他们没有构建三个独立的、互不兼容的工具，而是构建了一个通用适配器（在 Lean 中称为“类”/Class）。这个适配器知道如何融入任何一种厨房。如果你在处理实数，它会自动切换到实数模式。如果你在处理矩阵，它会自动切换到矩阵模式。

5. “非单位化”挑战（没有主开关的厨房）

大多数数学工具都假设厨房里有一个“主开关”（单位元/identity element）。但有些数学厨房（非单位代数）是没有这个开关的。

类比： 想象一个控制整个房间的灯光开关。在“单位化”的厨房里，开关是存在的。在“非单位化”的厨房里，开关是不存在的。
解决方案： 作者想出了如何在缺少主开关的情况下依然使用该工具的方法。他们通过暂时假装厨房里有一个开关，完成工作，然后再把开关移除。这使得该工具可以在任何厨房中工作，无论是否有开关。

6. 为什么这很重要

在此论文发表之前，如果数学家想在计算机证明中使用这个工具，他们必须经历重重障碍（证明连续性、证明正规性、处理不同的数字类型），以至于在纸上做数学题并忽略计算机往往更容易。

作者的目标是让计算机接口像在纸上书写一样简单。

之前： 你必须为每一步都随身携带沉重的证明证书背包。
之后： 计算机拥有一个“智能助手”（称为 autoParam），它可以自动为你找到那些证书。如果你写下 sqrt(a)，计算机会自动检查 a 是否是平方根的有效候选对象。如果是，那就太好了；如果不是，它会告诉你。

总结

这篇论文记录了一个用于操纵复杂数学机器的用户友好、通用且鲁棒的数字工具的构建过程。

他们用灵活的定义取代了僵化、易崩溃的定义，利用“垃圾值”来保持流程顺畅。
他们构建了一个通用适配器来处理不同类型的数字（实数、复数、非负数）。
他们确保了即使在“损坏”的厨房（非单位代数）中也能正常工作。
他们加入了自动化功能，使用户不必手动证明每一个微小的细节。

其结果是一个系统，让数学家能够专注于思想（食谱），而不是语法（切菜），使得在证明助手中实现高级算子理论成为可能。

技术总结：Lean 中的连续函数演算

问题陈述
连续函数演算是 $C^*$ 代数理论中的基础工具，它允许将交换 $C^*$ 子代数与紧 Hausdorff 空间上的连续函数代数进行等同。尽管在数学上已得到充分理解，但在像 Lean 这样的证明助手中进行形式化处理却面临着显著挑战。主要的困难在于平衡数学的忠实性与可用性。一个“自然”的数学定义通常依赖于依赖类型（例如，仅定义在元素谱上的函数）和捆绑结构（例如，将连续映射视为一种特定类型）。虽然这些定义是严谨的，但它们会给形式化证明带来摩擦：由于类型依赖于特定的元素，重写等式变得困难；此外，组合函数需要处理复杂的子类型强制转换（coercions）和连续性证明。作者发现，优先考虑严格数学简单性的设计往往无法通过 Mathlib 这类库所要求的实际可用性“试金石”。

方法论与设计决策
作者在 Lean 4 中开发了连续函数演算的形式化，并将其集成到 Mathlib 库中。其方法论涉及一个从数学“纯粹”定义向“实用主义”接口演进的迭代设计过程。关键的设计决策包括：

解捆绑与“垃圾值”（Junk Values）：
作者并没有将函数演算定义为从谱上的连续函数类型 $C(\sigma(a), \mathbb{C})$ 到代数的映射，而是定义了一个接受任意函数 $f: \mathbb{C} \to \mathbb{C}$ 和任意元素 $a$ 的函数 cfc。如果 $a$ 不是正规元素或 $f$ 在谱上不连续，该函数将返回一个“垃圾值”（通常为 0）。
- 基本原理： 这允许用户在首先证明 $a$ 是正规或 $f$ 在谱上连续之前，就能编写类似 $f(a)$ 的表达式。这模仿了非正式数学中“先书写，后思考”的方法，将证明的负担推迟到需要非平凡性质时才处理。这也使得无缝重写（rw）成为可能，因为参数的类型不再依赖于 $a$ 的特定属性。
基于类的抽象：
为了处理不同的标量环（ $\mathbb{C}$ 、 $\mathbb{R}$ 和 $\mathbb{R}_{\ge 0}$ ）以及不同的元素类型（正规、自伴、非负），作者将该演算实现为一个类型类 ContinuousFunctionalCalculus。
- 谓词泛化： 该类由作用于代数元素的谓词 $p$ 参数化（例如，IsStarNormal、IsSelfAdjoint、0 ≤ a）。这使得单一接口可以覆盖各种情况而无需代码重复。
- 属性值 vs 数据： 早期版本包含了作为数据的 $*$ -同态。然而，为了避免定义相等性问题（即两个不同构造的相同映射在定义上可能不相等），最终设计将该类作为一个 Prop（命题）。它断言存在一个具有特定性质的唯一的 $*$ -同态，而不是存储该映射本身。
处理非单位代数：
该形式化扩展到了非单位 $C^*$ 代数。作者没有依赖于对每个定义都使用外部构造（如最小单位化），而是引入了**拟谱（quasispectrum）**的内在定义。非单位函数演算定义在在 0 处消失（或将 0 映射到 0）的函数上，从而避免了在单位与非单位语境之间不断切换的需求。
通过 autoParam 实现自动化：
为了减轻手动传递连续性和正规性证明的繁琐程度，作者利用了 Lean 的 autoParam 特性。诸如“ $f$ 在谱上连续”之类的假设都配备了默认策略。如果用户没有提供证明，Lean 会尝试使用现有的引理（如 aesop、fun_prop）自动合成该证明。
将唯一性作为独立的类：
组合性质（ $g(f(a)) = (g \circ f)(a)$ ）是该理论的核心。作者通过使用唯一性论证而非 Stone–Weierstrass 定理（后者对于 $\mathbb{R}_{\ge 0}$ 失效）来证明这一点。他们将 $*$ -同态的唯一性封装在一个独立的类 ContinuousMap.UniqueHom 中，从而允许在不同的标量环之间通用地导出组合性质。

主要贡献与结果

首次形式化： 本工作构成了任何证明助手中对连续函数演算的首次形式化。
Mathlib 集成： 其实现已合并至 Mathlib，为复数、实数及非负实数函数演算提供了统一接口。
可用性验证： 设计通过了特定的“试金石”测试，包括：
- 使用在全域不连续的函数（如 $x \mapsto x^{-1}$ ）定义逆元（ $f(a^{-1})$ ）。
- 为自伴和非负元素构造正部/负部及平方根。
- 将演算应用于实数上的矩阵（在 Mathlib 中这些矩阵缺乏全局度量结构）。
自动化： 该接口支持高层自动化，允许用户以极少的干预证明诸如 $f(-a) = (x \mapsto f(-x))(a)$ 之类的性质。
应用： 该接口已被用于形式化高级结果，包括：
- 非单位 $C^*$ 代数中近似单位的存在性。
- 函数演算在两个变量上的连续性。
- 关于映射 $a \mapsto |a|$ 、 $a \mapsto a^p$ 以及 $a \mapsto \log(a)$ 的性质。
- 关于幺正元和投影的结论。

意义与局限性
该论文声称其意义主要在于其设计哲学：证明了对于一个大型形式化库而言，若要使其成为有效的工具，必须优先考虑终端用户的易用性（usability），而非定义上的严格数学纯粹性。通过接受“垃圾值”并解开类型捆绑，作者创建了一个行为符合数学家直觉的接口，使得复杂的操纵（如组合和重写）变得可行，而如果采用严格的依赖类型方法，这些操纵将极其困难。

作者对现状保持谦逊，承认存在以下局限性：

Simp 引理： 由于需要显式参数来触发 autoParam，许多引理无法在没有人工干预的情况下直接作为 simp 规则使用，这使得某些证明比预期的更为冗长。
$\mathbb{R}_{\ge 0}$ 的复杂性： 使用非负实数作为标量环引入了特定的技术障碍（例如，截断减法、缺乏环结构），这需要单独的定理陈述。
实 $C^*$ 代数： 虽然该框架旨在支持实 $C^*$ 代数，但针对实代数上的复数函数演算（这需要不同的函数定义域）尚未完全整合，并计划在未来工作中完成。

总之，本文记录了将深奥的算子代数理论成功转化为可用形式系统的过程，强调了在交互式定理证明语境下，数学优雅性与实际效用之间的权衡。