Formalization of De Giorgi--Nash--Moser Theory in Lean

TL;DR

This paper formalizes key results of the De Giorgi--Nash--Moser theory for elliptic PDEs in Lean, marking the first machine-checked proof of such a major theorem in modern PDE analysis.

Contribution

It provides the first formal proof of core elliptic PDE regularity results in Lean, including local boundedness, Harnack inequalities, and interior Hölder regularity.

Findings

Formalization includes local boundedness of weak subsolutions

Proves weak Harnack inequality for supersolutions

Establishes interior Hölder regularity for solutions

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\"older 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.