arxiv: 2604.05984 · v1 · submitted 2026-04-07 · 🧮 math.AP

Recognition: no theorem link

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

Scott Armstrong , Julia Kempe

Authors on Pith no claims yet

Pith reviewed 2026-05-10 18:30 UTC · model grok-4.3

classification 🧮 math.AP

keywords formalizationLeanDe Giorgi-Nash-Moser theoryelliptic equationsSobolev spacesweak solutionsHolder regularityPDE regularity

0 comments

The pith

The De Giorgi-Nash-Moser theory for elliptic PDEs has been fully formalized in Lean.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper formalizes the core interior results of De Giorgi-Nash-Moser theory for uniformly elliptic divergence-form equations with bounded measurable coefficients. It establishes local boundedness of weak subsolutions, the weak Harnack inequality for positive supersolutions, Moser's Harnack inequality for solutions, and interior Holder regularity. The work supplies new Lean infrastructure for Sobolev spaces on bounded domains and weak solutions of elliptic equations. A sympathetic reader would care because these results underpin much of modern PDE analysis, and their machine-checked verification removes any possibility of overlooked gaps in the classical arguments.

Core claim

The authors present a Lean formalization that includes local boundedness of weak subsolutions, the weak Harnack inequality for positive weak supersolutions, Moser's Harnack inequality for positive weak solutions, and interior Holder regularity for uniformly elliptic divergence-form equations with bounded measurable coefficients. This is the first machine-checked formalization of a major theorem in modern PDE theory.

What carries the argument

The Lean development of Sobolev spaces, weak solutions to elliptic equations, and the De Giorgi-Nash-Moser estimates that deliver quantitative regularity.

If this is right

The classical interior regularity theory for these elliptic equations is now machine-verified and free of hidden gaps.
New infrastructure for Sobolev spaces and weak solutions can be reused for formalizations of other elliptic and parabolic results.
Quantitative estimates in analysis can be checked at the level of explicit constants and dependencies.
Large-scale formalization of hard analytic arguments is shown to be feasible in Lean.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same infrastructure could support formal verification of related results such as boundary regularity or nonlinear equations.
Combining this library with existing formal developments in real analysis might allow certified numerical methods that respect the Holder estimates.
Future extensions could target the dependence on the ellipticity ratio and dimension to produce explicit constants automatically.

Load-bearing premise

The formalized Lean statements accurately capture the classical mathematical definitions of weak solutions, Sobolev spaces, and the De Giorgi-Nash-Moser estimates without introducing encoding errors.

What would settle it

A concrete mismatch between the formalized statement of Moser's Harnack inequality and its classical textbook version, or an executable counterexample that the Lean proof script accepts.

Figures

Figures reproduced from arXiv: 2604.05984 by Julia Kempe, Scott Armstrong.

**Figure 1.** Figure 1: Sobolev infrastructure. All boxes are reusable library components not specific to De Giorgi–Nash–Moser theory. 3.1. Analytic infrastructure. The proof begins with a bounded-domain Sobolev library. Weak derivatives are defined by integration by parts against smooth compactly supported test functions, and Sobolev spaces on an open set Ω ⊆ R d are defined through the existence of weak partial derivatives in … view at source ↗

**Figure 2.** Figure 2: PDE proof chain. Gray boxes are Sobolev infrastructure from [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

This is the first Lean formalization of De Giorgi-Nash-Moser theory plus useful new infrastructure for Sobolev spaces and weak elliptic solutions.

read the letter

The main point is that Armstrong and Kempe have machine-checked the interior regularity results for weak solutions to uniformly elliptic divergence-form equations: local boundedness of subsolutions, weak Harnack for supersolutions, Moser Harnack, and interior Hölder continuity. They also built out supporting Lean code for Sobolev spaces on bounded domains and the weak formulation that did not exist before in the libraries. That infrastructure work is the real addition here, and getting the quantitative estimates through in a proof assistant is a concrete step forward for formal analysis. It shows that large pieces of hard PDE theory are now reachable in Lean without obvious roadblocks. The internal consistency is strong because everything is checked by the system, and the work is grounded in standard logic rather than any circular or fitted constructions. The abstract states the results match the classical statements, which is the right claim to make. The soft spot is that we still need to see the actual code to confirm the encodings line up on the details that matter: the precise integral identity for weak solutions, how null sets and measurability are handled in the Sobolev spaces, the exact ellipticity bounds, and whether the constants in the estimates are the same as in Gilbarg-Trudinger. The paper does not include an explicit side-by-side validation section, so that check is left to the reader or referee. This paper is mainly useful to people building formal libraries in analysis or to PDE researchers who want verified foundations they can trust for downstream work. It is not a new theorem but a verified version of existing ones, so most people will read it for the code rather than the math. I would send it to peer review. The contribution is clear, the formalization is non-trivial, and the potential mismatches are checkable by people who know both the classical theory and Lean.

Referee Report

2 major / 2 minor

Summary. The manuscript presents 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. It claims to be the first machine-checked formalization of a major theorem in modern PDE theory and develops substantial new infrastructure for Sobolev spaces on bounded domains, weak solutions of elliptic equations, and quantitative regularity estimates.

Significance. If the Lean encodings faithfully reproduce the classical statements, this work is a significant milestone in the formalization of analysis. It supplies machine-checked proofs for foundational regularity results in elliptic PDE theory and creates reusable infrastructure for Sobolev spaces and weak solutions. These strengths directly support the claim that large-scale autoformalization of hard analysis is now feasible in Lean, providing a concrete foundation for further developments in the field.

major comments (2)

[Introduction and Preliminaries] The central claim requires that the formalized definitions exactly match the classical ones (integral identity for weak subsolutions against C_c^∞ test functions, W^{1,2} via equivalence classes and distributional derivatives, ellipticity λ|ξ|^2 ≤ A(x)ξ·ξ ≤ Λ|ξ|^2 a.e., and the precise quantitative forms of the estimates). The manuscript provides no explicit side-by-side comparison or validation of these encodings against standard references such as Gilbarg-Trudinger or Evans; this is load-bearing for the assertion that the results correspond to the classical theorems.
[Preliminaries] § on weak solutions and Sobolev spaces: the handling of measurability, null sets, and a.e. conditions in the Lean implementation of the ellipticity condition and the integral identity must be shown to preserve the classical meaning for bounded measurable coefficients; any deviation would undermine applicability of the formalized local boundedness and Harnack results.

minor comments (2)

[Introduction] The abstract and introduction use 'to our knowledge' for the 'first' claim; a short literature survey of prior formalizations in PDE or analysis would strengthen this without altering the main contribution.
[Preliminaries] Notation for the domain, coefficients A, and constants λ, Λ is introduced late; earlier consistent definition would improve readability of the quantitative estimates.

Simulated Author's Rebuttal

2 responses · 0 unresolved

Thank you for your thorough review and positive evaluation of our formalization of the De Giorgi--Nash--Moser theory. We appreciate the emphasis on verifying the fidelity of our Lean encodings to the classical statements. Below we respond to each major comment and indicate the revisions planned for the manuscript.

read point-by-point responses

Referee: [Introduction and Preliminaries] The central claim requires that the formalized definitions exactly match the classical ones (integral identity for weak subsolutions against C_c^∞ test functions, W^{1,2} via equivalence classes and distributional derivatives, ellipticity λ|ξ|^2 ≤ A(x)ξ·ξ ≤ Λ|ξ|^2 a.e., and the precise quantitative forms of the estimates). The manuscript provides no explicit side-by-side comparison or validation of these encodings against standard references such as Gilbarg-Trudinger or Evans; this is load-bearing for the assertion that the results correspond to the classical theorems.

Authors: We agree that an explicit comparison would enhance clarity and strengthen the claim of correspondence to classical theorems. In the revised manuscript, we will add a new subsection in the Preliminaries section providing side-by-side comparisons of our Lean definitions with the statements in Gilbarg-Trudinger (Section 8.1) and Evans (Section 6.2). This will include the weak formulation using compactly supported smooth test functions, the definition of Sobolev spaces via equivalence classes and weak derivatives, the pointwise a.e. ellipticity condition, and the quantitative forms of the estimates. We will also reference the specific Lean declarations to allow readers to verify the encoding. revision: yes
Referee: [Preliminaries] § on weak solutions and Sobolev spaces: the handling of measurability, null sets, and a.e. conditions in the Lean implementation of the ellipticity condition and the integral identity must be shown to preserve the classical meaning for bounded measurable coefficients; any deviation would undermine applicability of the formalized local boundedness and Harnack results.

Authors: Our Lean formalization employs the measure theory library in Mathlib, where the ellipticity condition is asserted to hold Lebesgue-almost everywhere, and the integral identity is formulated using the Lebesgue integral over the domain with test functions in C_c^∞. This mirrors the classical treatment of bounded measurable coefficients, where properties hold up to null sets. To address the concern explicitly, we will include a paragraph in the Preliminaries explaining the correspondence, noting that deviations on null sets do not affect the integral identities or the applicability of the regularity results, consistent with standard PDE theory. We believe no deviation exists in the current encoding, but the added explanation will make this transparent. revision: yes

Circularity Check

0 steps flagged

No circularity: direct formalization of classical PDE theorems

full rationale

The paper encodes the standard De Giorgi-Nash-Moser theory (local boundedness, weak Harnack, Moser Harnack, interior Hölder) for uniformly elliptic divergence-form equations directly from classical sources such as Gilbarg-Trudinger. The Lean statements for weak solutions, Sobolev spaces W^{1,2}, ellipticity, and quantitative estimates follow the integral identities and a.e. conditions of the literature without redefinition, fitted parameters, or self-referential closure. The central claim is simply that these existing results have now been machine-checked; no derivation step reduces to its own input by construction, and the work is self-contained against external mathematical benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the correctness of new Lean definitions for Sobolev spaces and weak solutions together with the standard axioms of the Lean theorem prover; no free parameters or invented entities are introduced.

axioms (1)

standard math Standard axioms and kernel of the Lean theorem prover
All formalizations in Lean rely on the foundational logic and axioms of the system itself.

pith-pipeline@v0.9.0 · 5410 in / 1145 out tokens · 64623 ms · 2026-05-10T18:30:15.435418+00:00 · methodology

discussion (0)

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

Ablation and the Meno: Tools for Empirical Metamathematics
cs.LO 2026-04 unverdicted novelty 6.0

Meno and tactic ablation on Tao's Analysis I generate proof populations that embed on low one- or two-dimensional submanifolds far from human constructions in Goedel Prover space.

Reference graph

Works this paper leans on

10 extracted references · 2 canonical work pages · cited by 1 Pith paper

[1]

Sylvie Boldo, Fran c ois Cl\'ement, Florian Faissole, Vincent Martin, and Micaela Mayero, A C oq formal proof of the L ax-- M ilgram theorem , Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (New York, NY, USA), CPP 2017, ACM, 2017, pp. 79--89

2017
[2]

Enrico Bombieri and Enrico Giusti, Harnack's inequality for elliptic differential equations on minimal surfaces, Invent. Math. 15 (1972), 24--46. 0305715

1972
[3]

Ennio De Giorgi, Sulla differenziabilit\`a e l'analiticit\`a delle estremali degli integrali multipli regolari, Mem. Accad. Sci. Torino. Cl. Sci. Fis. Mat. Nat. (3) 3 (1957), 25--43. 0093649

1957
[4]

12699, Springer, 2021, pp

Leonardo de Moura and Sebastian Ullrich, The lean 4 theorem prover and programming language, Automated Deduction -- CADE 28 (Cham) (Andr\'e Platzer and Geoff Sutcliffe, eds.), Lecture Notes in Computer Science, vol. 12699, Springer, 2021, pp. 625--635

2021
[5]

Moritz Doll, Formalizing S chwartz functions and tempered distributions , arXiv:2510.24060, 2025

work page arXiv 2025
[6]

Pure Appl

J\"urgen Moser, A new proof of D e G iorgi's theorem concerning the regularity problem for elliptic differential equations , Comm. Pure Appl. Math. 13 (1960), 457--468. 0170091

1960
[7]

Pure Appl

, On H arnack's theorem for elliptic differential equations , Comm. Pure Appl. Math. 14 (1961), 577--591. 0159138

1961
[8]

Patrick Massot, Floris van Doorn, and Oliver Nash, Formalising the h -principle and sphere eversion, arXiv:2210.07746, 2022

work page arXiv 2022
[9]

John Nash, Continuity of solutions of parabolic and elliptic equations, Amer. J. Math. 80 (1958), no. 4, 931--954. 0100158

1958
[10]

309, 2024, pp

Floris van Doorn and Heather Macbeth, Integrals within integrals: a formalization of the G agliardo-- N irenberg-- S obolev inequality , 15th International Conference on Interactive Theorem Proving (ITP 2024), LIPIcs, vol. 309, 2024, pp. 37:1--37:18

2024