DeGiorgi

A large-scale Lean 4 formalization of elliptic De Giorgi-Nash-Moser theory, built on top of Mathlib.

This repository formalizes the De Giorgi/Moser weak-solution theory for uniformly elliptic divergence-form equations with general bounded measurable uniformly elliptic coefficients, proving local boundedness, weak Harnack, Harnack, and Hölder regularity. The development is fully formalized, sorry-free, and axiom-free beyond Lean and Mathlib, and is organized around the namespace DeGiorgi.

Spanning about 56,000 lines of Lean 4, the project brings a major chapter of elliptic regularity into the formal setting in dimension d ≥ 3, with the formal statements presented in the normalized and rescaled forms natural for the proofs.

The code was written in a roughly two-week interval with extensive use of subscription large-language models (LLMs). The authors provided detailed proof blueprints and supervised the code generated by the LLMs, and intervened when they got stuck.

To our knowledge, this development represents the first proof-assistant formalization of Sobolev spaces built from weak derivatives at this level of generality, and the first large-scale formalization of a modern PDE regularity theorem.

Authors:

• Scott Armstrong — CNRS & Laboratoire Jacques-Louis Lions, Sorbonne Université and Courant Institute, School of Mathematics, Computing, and Data Science, New York University. (scottnarmstrong@gmail.com)
• Julia Kempe — Courant Institute, School of Mathematics, Computing, and Data Science, New York University. (kempe@nyu.edu)

Main import

import DeGiorgi

The root module re-exports the main headline results from:

import DeGiorgi.DeGiorgiTheory

Headline theorems

The root import exposes theorem names including:

• linfty_subsolution_DeGiorgi_normalized
• weak_harnack
• weak_harnack_on_ball
• harnack
• harnack_of_homogeneousWeakSolution
• holder_Moser
• holder_Moser_of_homogeneousWeakSolution

Companion document

The repository also includes DeGiorgi_Lean_to_Tex.tex, a machine-generated natural-language rendering of the Lean development. It is intended as a reading companion to the formalized proofs in the Lean source files.

Build

This project uses the Lean compiler and dependency versions pinned in lean-toolchain and lake-manifest.json.

Assuming elan and lake are installed:

lake exe cache get
lake build

To build the root import directly:

lake build DeGiorgi

Repository layout

• DeGiorgi/ contains the Lean source files
• DeGiorgi.lean is the root import
• DeGiorgi_Lean_to_Tex.tex is a machine-generated natural-language companion to the Lean development
• manifest.json records the main extracted theorem targets

License

This project is released under the Apache 2.0 license. See LICENSE for details.

Acknowledgements

S.A. acknowledges support from the European Research Council (ERC) under the European Union's Horizon Europe research and innovation programme, grant agreement number 101200828.

J.K. thanks the Simons Foundation for support through the Collaborative Grant “The Physics of Learning and Neural Computation”.

Citation

If you use this development, please cite the accompanying paper:
Formalization of De Giorgi--Nash--Moser Theory in Lean
Scott Armstrong and Julia Kempe
arXiv:2604.05984

The software repository can be cited using the metadata in CITATION.cff.