AI 中文总结
在 Lean 4 中形式化线性椭圆偏微分方程理论，包括 Dirichlet 问题可解性、Sobolev 空间及相关定理，实现无 sorry 的机器验证。
AI 中文摘要
我们在 Lean 4 中，基于 Mathlib，形式化了散度形式二阶线性椭圆算子的 Dirichlet 问题的可解性。机器验证的结果（开发过程中无 sorry）包括 Poincaré 不等式、通过 Lax-Milgram 定理得到的弱解存在性、Rellich-Kondrachov 紧性、Fredholm 二择一、谱定理、内部正则性估计以及 Sobolev 嵌入定理。从这些结果中，我们获得了对足够正则的系数和数据的经典可解性的形式化。我们的 Lean 库包含一个独立于现有形式化而发展的自包含的 Sobolev 空间理论。在整篇论文中，我们将每个散文陈述与相应的机器检查的 Lean 声明关联起来。
英文摘要
We formalise in Lean 4, on top of Mathlib, the solvability of the Dirichlet problem for second-order linear elliptic operators in divergence form. The machine-verified results, with no sorry in the development, include the Poincaré inequality, the existence of weak solutions by the Lax-Milgram theorem, Rellich-Kondrachov compactness, the Fredholm alternative, the spectral theorem, interior regularity estimates, and the Sobolev embedding theorem. From these results we obtain a formalisation of classical solvability for sufficiently regular coefficients and data. Our Lean library includes a self-contained theory of Sobolev spaces developed independently of existing formalisations. Throughout the paper we associate each prose statement with the named machine-checked Lean declaration that discharges it.
Comments30 pages, 1 figure. Lean library available at https://github.com/alejandro-soto-franco/EllipticPDE
