A Formalization of the Laplace Transform and Its Inversion in Lean 4

想象一个这样的世界：事物随时间变化的混乱、杂乱的运动——比如摆动的钟摆、振动的吉他弦，或是穿过导线的信号——可以被瞬间转化为一个干净、静态的代数问题。这就是**拉普拉斯变换（Laplace transform）**的魔力，这种数学工具被工程师和科学家使用了一个多世纪。你可以把它看作是一个通用的翻译器，将用“时间”语言编写的故事（其中事物在移动、加速或减速）转化为用“复数”语言编写的故事（其中同样的运动变成了简单的乘法和除法）。

为什么这很重要？因为求解关于事物如何变化的方程通常极其困难，就像是在试图解开一个正在被拉扯的绳结。但如果你能将这个绳结翻译成另一种语言，让它看起来只是一条直线，你就能轻松解决它，然后再把答案翻译回来。这篇论文是关于为这个翻译器构建一个“证明检查器”。作者们不仅仅是写下了规则；他们使用了一个名为 Lean 4 的计算机程序，逐步地在数学上证明了这个翻译器确实如其所承诺的那样精确工作，甚至包括该过程中最棘手的部分。他们希望确保当我们使用这些强大的工具来设计桥梁、电路或控制系统时，底层的数学是坚不可摧且没有隐藏错误的。

---

数字证明检查器

想象你有一个非常严格、非常死板的机器人朋友，它热爱数学但讨厌猜测。你告诉它：“这是一个将弯曲线条变为平滑曲线的公式，”它会问：“你确定吗？如果这条线抖动得太厉害怎么办？如果它一直延伸到无穷远怎么办？”这篇论文是两位研究员 Daniel 和 Antoine 教导这位机器人朋友掌握拉普拉斯变换所需的一切知识的结果。

他们不仅编写了一本教科书；他们还在 Lean 4 中构建了一个完整的、经过计算机验证的库。这是一种专门用于编写计算机可以检查错误的数学证明的编程语言。他们的目标是将拉普拉斯变换——一种将时间函数转化为复数函数的方法——进行建模，并证明其每一条规则都有效，从基础定义到将答案转回时间的复杂“反演”过程。

翻译器与魔镜

拉普拉斯变换就像一面神奇的镜子。你将一个函数 $f(t)$（描述随时间发生的事情）放入镜中，它会反射回一个新的函数 $(Lf)(s)$（描述同一件事在“频率”世界中的样子）。

• 前行之旅： 论文证明了如果你有一个表现良好的函数（它不会过快地爆炸到无穷大），这面镜子就能奏效。他们证明了如何翻译简单的对象，如常数、时间的幂次，甚至是正弦波。例如，他们展示了镜子如何将导数（变化率）转化为与数字 $s$ 的简单乘法，再减去一个初始值。这就是使求解微分方程变得如此容易的“秘诀”。
• 归途（反演）： 真正的挑战是如何拿回答案。如何通过观察反射出的图像并准确知道原始物体是什么？这被称为拉普拉斯反变换（inverse Laplace transform）。论文证明了一种执行此操作的具体方法，称为 Bromwich 公式。

为什么他们没有选择“简便”路径

通常，数学家使用一种称为**复平面围道积分（complex contour integration）**的技术来证明反演公式。想象在地图上的一个形状周围画一个圈，并使用一个特殊的定理（留数定理）来计算里面的“宝藏”。这是一个强大的工具，但作者发现计算机库中还没有内置足够的这类“绘图”工具。

因此，他们采取了一条不同的、更接地气的路径。他们没有在复平面上画圈，而是将问题视为实数轴上的直线积分。他们将问题分解为更小、更易处理的部分：

1. 截断（Truncation）： 他们假装无限长的直线只是一个从 $-T$ 到 $T$ 的短有限段。
2. Sinc 函数： 随着他们使这个片段变得越来越长，一个涉及 sinc 函数（看起来像是一个逐渐变小的波浪）的特定模式出现了。
3. 狄利克雷积分（Dirichlet Integral）： 他们依靠一个关于这个 sinc 波形下方面积的著名预证事实（狄利克雷积分），来证明当这个片段趋于无穷长时，结果能够完美地重建原始函数。

这种方法在设置上更难，但对于计算机验证来说更安全，因为它依赖于实数微积分，而计算机对这方面已经非常擅长。

摆动钟摆测试

为了证明他们的系统确实有效，他们不仅仅检查抽象数学；他们解决了一个经典的物理问题：谐振子（harmonic oscillator）。这是关于摆动的钟摆或上下弹跳的弹簧背后的数学。

• 设定： 他们定义了一个处于静止状态但受到快速推动的弹簧，由方程 $y''(t) + \omega^2 y(t) = 0$ 描述。
• 翻译： 他们将这个方程输入到他们计算机验证的拉普拉斯翻译器中。
• 结果： 计算机成功地将这个复杂的微分方程转换成了简单的代数方程：$(s^2 + \omega^2)Y(s) = \omega$。
• 求解： 对 $Y(s)$ 进行求解得到了 $\frac{\omega}{s^2 + \omega^2}$。
• 验证： 计算机随后检查了自己的库，并确认这个特定的结果正是 $\sin(\omega t)$ 的拉普拉斯变换。

这是一个巨大的成功。这意味着计算机不仅计算出了答案；它还证明了该答案确实是一个正弦波，这与人类物理学家几个世纪以来所知的一致，但其确定性程度让任何人为错误都无处遁形。

游戏的严格规则

这篇论文也是关于当你停止猜测并开始证明时必须多么谨慎的一课。作者强调了许多在教科书中经常被掩盖掉的“陷阱”：

• 无穷大很棘手： 你不能仅仅假设积分会趋向无穷大。证明必须明确说明函数必须衰减得足够快，以便积分的“尾部”消失。
• 边界情况： 在进行数学运算时，存在一些规则发生变化的特定点（例如时间 $t=0$）。计算机迫使他们必须精确说明函数的定义域和连续性。
• 交换顺序： 在反演证明中，他们必须交换两个积分的顺序。在日常数学中，你可能会直接这样做。但在他们的形式化证明中，他们必须严格证明合并后的曲面下的“面积”是有限的，然后才被允许交换顺序。

核心结论

这篇论文是**形式化验证（formal verification）**领域的一个里程碑。它并没有发现新的物理定律或发明一种新的波。相反，它为一个已经被广泛使用的工具构建了一座确定性的堡垒。通过将拉普拉斯变换及其反变换翻译成计算机可以检查的语言，作者创建了一个参考标准。

他们证明了只要遵循关于函数在无穷远处行为的严格规则，这个“神奇镜子”就是有效的。他们展示了通往答案的路径涉及细致、循序渐进的逻辑，而非捷径。对于任何正在构建依赖这些数学工具的下一代软件的人来说，这项工作确保了其基础不仅稳固，而且不可撼动。谐振子的例子是最后的认可印记：计算机与人类达成了一致，并且第一次，计算机也签署了这份证明。