De Giorgi--Nash--Moser 理论在 Lean 中的形式化
偏微分方程分析
2026-04-08 v1
摘要
我们给出了 De Giorgi--Nash--Moser 核心内部理论在 Lean 中的形式化，该理论针对具有有界可测系数的一致椭圆散度形式方程。形式化的结果包括弱下解的局部有界性、正弱上解的弱 Harnack 不等式、正弱解的 Moser Harnack 不等式，以及内部 Hölder 正则性。据我们所知，这是现代偏微分方程理论中一个主要定理的首次机器检查形式化。该发展还需要关于有界域上 Sobolev 空间、椭圆方程弱解和定量正则性估计的大量新基础设施。更广泛地说，它表明在 Lean 中大规模自动形式化困难分析现已触手可及。
引用
@article{arxiv.2604.05984,
title = {Formalization of De Giorgi--Nash--Moser Theory in Lean},
author = {Scott Armstrong and Julia Kempe},
journal= {arXiv preprint arXiv:2604.05984},
year = {2026}
}
备注
11 pages; Lean code available at https://github.com/scottnarmstrong/DeGiorgi