Constructs α-Hölder continuous solutions with α = exp(-c_n K) for uniformly elliptic equations with ellipticity ratio K in d ≥ 3, proving the sharpness of the Bombieri-Giusti exponent.
Formalization of De Giorgi--Nash--Moser Theory in Lean
6 Pith papers cite this work. Polarity classification is still indexing.
6
Pith papers citing it
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.
years
2026 6representative citing papers
Stable phase retrieval holds for L2-spans of independent centered real random variables iff all but at most one coordinate obeys a uniform two-sided L1 bound.
For every d>1, explicit lattice criteria with D(Λ)>1 are derived under which no continuous-Zak-transform function generates a Gabor frame, negatively resolving existence questions for several classes of smooth windows.
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
STFT with Gaussian window performs L²-local stable phase retrieval at the constant function, with Lean 4 autoformalization for an extension to Hermite windows and finite spans of basis vectors.
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.
citing papers explorer
-
On the sharp H\"older exponent in the De Giorgi--Nash--Moser theory
Constructs α-Hölder continuous solutions with α = exp(-c_n K) for uniformly elliptic equations with ellipticity ratio K in d ≥ 3, proving the sharpness of the Bombieri-Giusti exponent.
-
Stable Phase Retrieval for Spans of Independent Random Variables
Stable phase retrieval holds for L2-spans of independent centered real random variables iff all but at most one coordinate obeys a uniform two-sided L1 bound.
-
On the existence problem of regular Gabor frames
For every d>1, explicit lattice criteria with D(Λ)>1 are derived under which no continuous-Zak-transform function generates a Gabor frame, negatively resolving existence questions for several classes of smooth windows.
-
Formalizing Mathematics at Scale
A multi-agent framework called AutoformBot autoformalized 26 textbooks spanning analysis, algebra, topology, combinatorics and probability into a verified Lean 4 library of 45k declarations, demonstrating scalable formalization of graduate math.
-
$L^2$-Stability for STFT phase retrieval
STFT with Gaussian window performs L²-local stable phase retrieval at the constant function, with Lean 4 autoformalization for an extension to Hermite windows and finite spans of basis vectors.
-
Ablation and the Meno: Tools for Empirical Metamathematics
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.