🔢 mathematics

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case

本文使用 Lean 4 证明助手及其数学库 Mathlib，通过形式化阿道夫·赫维茨（Adolf Hurwitz）的傅里叶分析路径，在二维平面上严格验证了等周不等式 $L^2 \ge 4\pi A$ 。

原作者： Miraj Samarakkody

发布于 2026-03-17

📖 1 分钟阅读🧠 深度阅读

原作者： Miraj Samarakkody

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

这篇论文讲述了一个非常有趣的故事：作者 Miraj Samarakkody 使用一种名为 Lean 4 的“数学超级计算机”（证明助手），把人类历史上一个著名的几何定理——等周不等式——从头到尾用代码“跑”了一遍，确保它100% 正确，没有任何逻辑漏洞。

为了让你轻松理解，我们可以把这个过程想象成**“给数学定理做一次彻底的 CT 扫描”**。

1. 什么是“等周不等式”？（那个古老的谜题）

想象一下，你手里有一根固定长度的绳子（比如 1 米长）。

如果你把它围成一个正方形，里面能装多少东西（面积）？
如果你把它围成一个三角形，能装多少？
如果你把它围成一个圆形，能装多少？

答案很直观： 围成圆形时，里面的面积最大。
这就是“等周不等式”的核心：在周长固定的情况下，圆形的面积最大。 反过来说，如果你围住了一定的面积，圆形的周长是最短的。

这个结论古希腊人就知道（比如狄多女王用牛皮圈地的传说），但直到 19 世纪，数学家们才给出了严格的证明。其中，德国数学家阿道夫·赫维茨（Adolf Hurwitz）在 1902 年想出了一个非常优雅的方法，利用傅里叶级数（一种把复杂波形拆解成简单波形的数学工具）来证明它。

2. 为什么要用电脑来证明？（为什么要“形式化”？）

通常，数学家在纸上写证明时，会省略一些“显而易见”的步骤，比如“显然这里可以交换求和与积分的顺序”。人类读者能脑补出这些细节，但电脑不行。电脑需要每一个字、每一个逻辑跳跃都写得清清楚楚。

这篇论文做的就是这件事：

目标：把赫维茨那个优雅的证明，翻译成电脑能读懂的“代码语言”（Lean 4）。
工具：Lean 4 和它的数学库 Mathlib（就像是一个巨大的、已经验证过的数学公式百科全书）。
意义：一旦电脑通过了验证，我们就绝对确定这个定理是真理，没有任何人类可能犯的错误或疏漏。

3. 作者是怎么做的？（两个阶段的“登山”）

作者把证明过程分成了两个阶段，就像爬一座山：

第一阶段：搭建“脚手架”（傅里叶分析基础）

赫维茨的证明需要用到很多高级数学工具，就像盖房子需要先打地基。作者在电脑里先把这些工具造好：

正交性：就像不同频率的音叉互不干扰，作者证明了正弦波和余弦波在数学上是“正交”的（互不重叠）。
帕塞瓦尔定理（Parseval's Theorem）：这是一个能量守恒的公式。它告诉你，一个复杂波形的总能量，等于它所有组成波形的能量之和。
魏尔斯特拉斯 M 判别法：用来确保这些无穷多个波形加起来时，不会“乱套”，而是稳稳地收敛到一个结果。
维尔廷格不等式（Wirtinger's Inequality）：这是证明的关键“秘密武器”。它建立了一个函数（波形）和它的导数（变化率）之间的面积关系。

比喻：这就像在盖大楼前，先确保水泥、钢筋、砖块的质量都经过严格检测，并且知道怎么把它们完美地粘合在一起。

第二阶段：执行“赫维茨的证明”（真正的登山）

有了地基，作者开始按照赫维茨的思路走：

把曲线“拉直”：把任意形状的封闭曲线，想象成一根有弹性的绳子，重新调整它的参数，让它看起来像是在一个标准的圆圈上运动。
计算面积：用“鞋带公式”（一种计算多边形面积的方法）把面积表示出来。
数学魔术（分部积分）：通过一些微积分技巧，把面积公式变形。
应用“算术 - 几何平均不等式”：这是一个简单的数学常识（两个数的乘积小于等于它们的平方和的一半），用来缩小面积的上限。
终极一击（维尔廷格不等式）：利用第一阶段造好的“秘密武器”，把面积和周长联系起来。
得出结论：最终算出，面积 $A$ 永远小于等于 $L^2 / 4\pi$ 。只有当形状是完美的圆时，等号才成立。

4. 遇到的“坑”与挑战

虽然数学逻辑很清晰，但在电脑里实现却充满了“坑”：

无穷大的麻烦：数学书上写“交换求和与积分顺序”只需一句话，但在电脑里，必须证明这种交换是安全的，否则电脑会报错。
索引的混乱：数学里习惯从 1 开始数数，或者从 0 开始，Lean 4 里也有不同的计数方式。作者花了很多时间处理这些“对不上号”的问题，就像要把不同国家的护照统一成一种格式。
坐标的投影：在电脑里，二维平面上的点不是简单的 $(x, y)$ ，而是更复杂的结构。作者需要仔细地把这些结构拆解，才能算出导数。

5. 总结：这有什么用？

这篇论文不仅仅是在证明“圆最大”这个老生常谈的结论。它的真正价值在于：

信任：它展示了现代计算机如何帮助人类验证最复杂的数学理论，消除了人为错误的疑虑。
桥梁：它证明了 Lean 4 这样的工具已经强大到可以处理大学高年级甚至研究生级别的经典分析学问题。
未来：这为未来证明更宏大、更复杂的数学猜想（比如黎曼猜想或更高维的几何问题）铺平了道路。

一句话总结：
作者用一台“数学显微镜”，把赫维茨 100 年前关于“圆最美、面积最大”的证明，拆解成每一个原子级别的逻辑步骤，并让电脑确认：是的，圆确实是赢家，而且这个结论坚不可摧。

这是一份关于 Miraj Samarakkody 于 2026 年 3 月发表的论文《二维经典等周不等式的形式化》（Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case）的详细技术总结。

1. 问题背景 (Problem)

等周不等式 (The Isoperimetric Inequality) 是几何学中最著名的定理之一。其核心问题是：在所有周长 $L$ 给定的平面简单闭曲线中，哪一种形状围成的面积 $A$ 最大？

定理陈述：对于任意简单闭曲线，满足 $L^2 \ge 4\pi A$ 。
取等条件：当且仅当该曲线为圆时，等号成立（即 $A = L^2 / (4\pi)$ ）。
形式化挑战：虽然该定理在数学上已有多种证明（如变分法、Steiner 对称化等），但在计算机辅助证明（Formal Verification）中，特别是处理涉及傅里叶级数、无穷级数与积分交换、逐项微分以及正则性条件（ $C^1$ 连续性）的解析证明时，存在巨大的技术挑战。

2. 方法论 (Methodology)

本文使用 Lean 4 证明助手及其数学库 Mathlib，严格形式化了 Adolf Hurwitz (1902) 提出的基于傅里叶分析的证明方法。该方法避免了变分法，转而利用傅里叶系数和 Parseval 恒等式将几何问题转化为代数不等式。

形式化过程分为两个主要阶段：

第一阶段：傅里叶分析基础 (Fourier-Analytic Foundations)

为了支持 Hurwitz 的证明，作者首先构建了所需的分析工具：

三角函数正交性：在 $[-\pi, \pi]$ 上形式化了 $\sin(nx)$ 和 $\cos(mx)$ 的正交关系。
一致收敛性：利用 Weierstrass M-判别法 证明了傅里叶部分和的一致收敛性，这是保证极限函数连续性和可积性的关键。
Parseval 定理：形式化了 $L^2$ 范数与傅里叶系数 $\ell^2$ 范数之间的等式关系。
逐项微分：在满足更强收敛条件（ $\sum n(|a_n| + |b_n|) < \infty$ ）下，证明了傅里叶级数可以逐项求导。
Wirtinger 不等式：利用 Parseval 定理证明了该不等式（对于零均值周期函数， $\int f^2 \le \int (f')^2$ ）。

第二阶段：Hurwitz 证明的执行 (Hurwitz's Proof Execution)

针对平面上的简单闭 $C^1$ 曲线 $\gamma$ （弧长参数化，周长 $L$ ）：

重参数化：将曲线从 $[0, L]$ 重参数化到 $[0, 2\pi]$ ，定义坐标函数 $f(\theta)$ 和 $g(\theta)$ 。
面积公式：利用 鞋带公式 (Shoelace Formula) 和格林定理，将面积 $A$ 表示为积分 $A = \int_0^{2\pi} f(\theta)g'(\theta) d\theta$ （经分部积分简化后）。
不等式推导：
- 应用 AM-GM 不等式： $2fg' \le f^2 + (g')^2$ 。
- 应用 Wirtinger 不等式：利用 $f$ 的零均值性质（通过平移曲线实现），得到 $\int f^2 \le \int (f')^2$ 。
- 结合 弧长约束：由于是弧长参数化， $(f')^2 + (g')^2 = (L/2\pi)^2$ 为常数。
最终结论：通过上述步骤推导出 $A \le L^2 / (4\pi)$ 。

3. 关键贡献 (Key Contributions)

首个完整的 Hurwitz 证明形式化：
这是首次使用 Lean 4 完整形式化 Hurwitz 的傅里叶级数证明。之前的形式化尝试多集中在多边形或变分法证明，而本文填补了经典解析证明的空白。
Mathlib 中傅里叶分析的扩展：
- 构建了针对经典实傅里叶级数（系数序列 $a_n, b_n$ ）的专门理论，而非仅依赖抽象的 $L^2$ 空间理论。
- 形式化了从系数序列到函数收敛性的详细逻辑，包括正交性、Parseval 恒等式和 Wirtinger 不等式的严格推导。
处理高阶分析挑战：
论文详细记录了在 Lean 中处理以下复杂数学概念的策略：
- 积分与求和的交换：严格使用控制收敛定理（Dominated Convergence Theorem）的变体来证明 $\int \sum = \sum \int$ 。
- 逐项微分：解决了傅里叶级数索引（ $N^+$ ）与 Lean 标准定理索引（ $N$ ）之间的不匹配问题，并处理了导数级数的一致收敛性。
- 欧几里得空间投影：在 Mathlib 的 EuclideanSpace 和 PiLp 框架下，正确处理了曲线坐标分量与其导数之间的关系。
代码与文档：
提供了完整的 Lean 代码库（GitHub: mirajcs/IsoperimetricInequality），包含两个核心文件：IsoperimetricInequality.Basic（基础理论）和 IsoperimetricInequality.Adolf Hurwitz proof（主证明）。

4. 主要结果 (Results)

论文成功验证了以下核心定理和引理：

三角函数正交性引理：5 个关键的三角积分恒等式。
Parseval 定理：建立了函数平方积分与傅里叶系数平方和之间的精确等式。
Wirtinger 不等式：证明了 $\int f^2 \le \int (f')^2$ （在零均值条件下）。
等周不等式主定理：
```
theorem isoperimetric_inequality (gamma : SimpleClosedC1Curve 2) ... :
  area gamma 0 gamma.length <= gamma.length ^ 2 / (4 * Real.pi)
```
该定理在假设曲线为 $C^1$ $C^{1}$ 且导数连续、弧长参数化的条件下，机器验证了 $A \le L^2 / (4\pi)$ $A \leq L^{2} / (4 π)$ 。

5. 意义与影响 (Significance)

数学正确性的终极验证：
教科书中的 Hurwitz 证明通常省略了关于“无穷级数与积分交换”、“逐项微分合法性”以及“正则性条件”的繁琐细节。形式化过程强制将这些隐含假设显式化，确保了证明在逻辑上的绝对严密性。
Lean 4 分析库能力的展示：
该工作展示了 Mathlib 在处理研究生级别经典分析（Real Analysis）问题时的成熟度。它证明了 Lean 4 不仅能处理代数结构，也能处理涉及极限、积分、微分和无穷级数的复杂分析问题。
未来工作的基石：
- 等号成立条件：目前形式化仅证明了不等式，未来工作将致力于证明“当且仅当曲线为圆时取等号”。
- 正则性推广：当前证明要求曲线是 $C^1$ 的，未来可尝试推广到更弱的正则性条件（如有限变差或 $W^{1,2}$ 空间）。
- 高维推广：为形式化 $n$ 维空间中的等周不等式（涉及 Brunn-Minkowski 不等式或几何测度论）提供了基础组件。

综上所述，这篇论文不仅是对一个经典几何定理的机器验证，更是数学形式化领域在经典分析方向上的一次重要突破，展示了现代证明助手在处理复杂解析证明时的强大能力。