Formalization of De Giorgi--Nash--Moser Theory in Lean
Scott Armstrong, Julia Kempe
math.AP
Apr 7, 2026 · v1
TL;DR
Formalizes the interior De Giorgi-Nash-Moser theory for uniformly elliptic divergence-form equations, building new Sobolev-space and weak-solution infrastructure in Lean.
Abstract
We present a formalization in Lean of the core interior De Giorgi--Nash--Moser theory for uniformly elliptic divergence-form equations with bounded measurable coefficients. The formalized results include local boundedness of weak subsolutions, the weak Harnack inequality for positive weak supersolutions, Moser's Harnack inequality for positive weak solutions, and interior Hölder regularity. This is, to our knowledge, the first machine-checked formalization of a major theorem in modern PDE theory. The development also required substantial new infrastructure for Sobolev spaces on bounded domains, weak solutions of elliptic equations, and quantitative regularity estimates. More broadly, it suggests that large-scale autoformalization of hard analysis in Lean is now within reach.
Problem
Major theorems in modern PDE theory, specifically the De Giorgi-Nash-Moser interior regularity theory for uniformly elliptic divergence-form equations, had never been machine-checked in any proof assistant.
Approach
The authors formalize in Lean 4 the core De Giorgi-Nash-Moser theory: local boundedness of weak subsolutions, the weak Harnack inequality, Moser's Harnack inequality, and interior Holder regularity. The project required building substantial new infrastructure for Sobolev spaces on bounded domains, weak solutions, and quantitative regularity estimates. LLMs were used extensively under close supervision.
Results
This is the first machine-checked formalization of a major theorem in modern PDE theory. The Sobolev library alone comprises roughly 20,000 lines of Lean. The project demonstrates that large-scale autoformalization of hard analysis in Lean is now within reach.
