前几天，arXiv 上出现了一篇论文，标题很长：A formalization of the De Giorgi–Nash–Moser theory in Lean 4。如果你不搞定理证明，可能会直接划走。但我建议你停一下——这篇论文或许标志着一个对 PDE 研究者 真正有用的新方向正在成型。

我不是 Lean 用户，代码一行没跑过。但读完这篇论文之后，我意识到：形式化方法（formal methods）正在从“数学家的玩具”变成“PDE 研究的实用工具”。而且，你完全不需要自己会写 Lean，就可以从中受益，甚至参与其中。

传统 PDE 研究有什么痛点？

做 PDE 的人都知道，我们的领域有几样特产：

• 长证明：一个正则性定理动辄十几页，引理套引理。

• 软分析：常数被吸收、极限与函数空间来回切换、“容易验证”三个字频繁出现。

• 易错点：截断函数是否属于正确的 Sobolev 空间？延拓是否保持范数？BMO 估计中的常数是否真的与维度无关？——这些细节在发表时往往被跳过，但学生复现时经常卡住。

这些问题不是谁的错，而是纸质数学的天然局限。形式化恰恰是解决这些痛点的技术——它把证明变成机器可检验的代码，任何模糊之处都会导致编译失败。

这篇论文证明了什么？——给没接触过 Lean 的人

简单说，他们用 Lean 4 完整实现了 De Giorgi–Nash–Moser 理论的核心部分：

• 弱下解的局部有界性

• 正弱上解的弱 Harnack 不等式

• 正解的 Moser Harnack 不等式

• 内部 Hölder 正则性

这些都是现代 PDE 教材的巅峰内容。更重要的是，他们没有使用任何隐藏常数——每个常数都是显式的算术表达式，比如 Harnack 常数是 exp⁡(C(d)Λ1/2)exp(C(d)Λ1/2)，Hölder 指数的下界也是显式给出的。

在此之前，没有任何一个证明助手完成过这么复杂的 PDE 形式化。他们为此还从头搭建了有界区域上的 Sobolev 空间库（约 2 万行 Lean 代码）。

为什么这值得 PDE 研究者关注？——三个理由1. 你的证明可以被“机械化验证”

想象一下：你写了一篇关于某个椭圆方程的正则性论文，审稿人说“Lemma 3.2 的证明似乎跳过了延拓算子的连续性验证”。你可以说：“请参考形式化代码，那里有完整验证。”——这不是科幻，这篇论文就是先例。

未来，顶刊可能会鼓励（甚至要求）核心定理附带形式化附录。Lean 社区已经在推动这件事，而 PDE 是其中最难、也最需要的领域。

2. 形式化暴露了“纸质证明”中隐藏的假设

论文作者反复提到一个现象：教科书上的证明常常说“容易验证 ϕ=η2(u−k)+ϕ=η2(u−k)+​ 是允许的测试函数”。但在 Lean 里，你需要先证明 (u−k)+(u−k)+​ 确实属于 W01,2W01,2​，需要链式法则、截断引理、光滑逼近……整个一套基础设施。

这个过程强迫你把每个“显然”都拆解成原子步骤。许多经典证明在形式化过程中被发现存在微小缺口（比如需要额外的可积性条件）。这对 PDE 理论本身是一种净化和提升。

3. 为 AI 辅助证明铺路

这篇论文最让我惊讶的一点是：他们大量使用了 大语言模型（LLM） 来生成代码，人类只负责提供证明蓝图和最终校验。

也就是说，即使你不懂 Lean，你也可以用自然语言写出证明的结构（“先做 Caccioppoli 估计，再用 Sobolev 嵌入，得到递推”），让 LLM 辅助生成形式化代码。这大大降低了门槛。

未来，PDE 研究者可能只需要写半形式化的证明草稿，然后由 AI 辅助的证明助手自动补全细节并验证。你不需要成为 Lean 专家，就能享受形式化的红利。

那么，作为 PDE 研究者，我现在可以做什么？

1. 关注这个方向：Star 他们的 GitHub 仓库，读一读论文的 Section 4–5（讲基础设施和挑战），你会发现很多证明细节是你平时没想过但确实重要的。

2. 尝试合作：如果你手头有一个相对干净的正则性证明（比如某个抛物方程的 Moser 迭代），可以联系形式化社区的人，看看能否把它变成形式化项目。这比从零开始容易得多。

3. 学习基础 Lean：不一定写到精通，但了解基本语法和思想，就能看懂他们是如何处理弱导数、截断、延拓的。这对你写纸质证明也有好处——你会不自觉地更严谨。

4. 使用他们的库：他们开源的 Sobolev 空间库（有界区域、弱导数、Poincaré、John–Nirenberg）可以直接用于其他 PDE 的形式化。你可以把它当成一个“已验证的分析工具箱”。

一个预测

五年之内，我们会看到：

• 至少 3–5 个经典 PDE 定理在 Lean/Coq 中完成形式化（比如 Schauder 理论、Calderón–Zygmund 估计）。

• 部分期刊开始接受“形式化附录”作为补充材料。

• 出现一批既懂 PDE 又懂形式化的“双栖”研究者，他们将成为连接纯数学与可信计算的关键桥梁。

这篇 De Giorgi–Nash–Moser 的形式化，就是这场浪潮的第一朵浪花。

最后说点实在的

如果你现在觉得“形式化跟我无关”，完全可以理解。毕竟我们 PDE 人已经有太多事要忙：写论文、审稿、带学生、申基金……

但如果你对证明的可靠性有执念，或者对用新工具解决老问题感兴趣，不妨花一个小时读一下这篇论文的 Introduction 和 Section 5。你会看到一群数学家如何用机器把最经典的理论拆解成几千行可验证的逻辑。

这不只是关于 Lean，这是关于我们如何重新审视“证明”这件事。

论文标题：A formalization of the De Giorgi–Nash–Moser theory in Lean 4arXiv: 2604.05984v1代码：github.com/scottnarmstrong/DeGiorgi

欢迎评论区讨论——尤其是那些已经在尝试形式化的 PDE 同行，很想听听你们的经验。

转自 知乎 https://zhuanlan.zhihu.com/p/2025580283496277191?share_code=g6S3KiHzyynv&utm_psn=2026020503081481771&utm_source=wechat_timeline&utm_medium=social&s_r=0&wechatShare=1

转载本文请联系原作者获取授权，同时请注明本文来自王伟华科学网博客。
链接地址：https://wap.sciencenet.cn/blog-81613-1529972.html

上一篇：[转载]数学综合性期刊排名