Differential Geometry in Lean 4

An ongoing Lean 4 library for differential geometry and geometric analysis, currently focused on Ricci flow.

How to use

Use DifferentialGeometry as an upstream dependency and build on its geometric-analysis infrastructure:

[[require]]
name = "DifferentialGeometry"
git = "https://github.com/qinz1yang/differential-geometry.git"
rev = "v0.1.3"

Release v0.1.3 is pinned to Lean and Mathlib v4.33.1.

Import the full library with

import DifferentialGeometry

or a specific module, for example the scalar strong maximum principle:

import DifferentialGeometry.Analysis.Parabolic.MaximumPrinciple.Scalar.Strong

We aim to keep pace with Mathlib releases and update the pinned Mathlib version accordingly.

Formalized theorems

Each is sorry-free (axioms: propext, Classical.choice, Quot.sound).

These three are the standard axioms of Lean's core library — propositional extensionality, the axiom of choice, and quotient soundness — on which all of classical mathematics in Mathlib rests. #print axioms lists everything a theorem transitively assumes: a sorry would surface as sorryAx, and any ad-hoc axiom would be named. An output of exactly these three therefore certifies that the proof is fully kernel-checked, with no sorry and no assumptions beyond the classical foundations.

• Poincaré conjecture — every compact, Hausdorff, simply connected topological three-manifold without boundary is homeomorphic to the unit sphere $S^3 \subset \mathbb{R}^4$. The final statement uses only Lean/Mathlib concepts. The smooth version gives a diffeomorphism for smooth three-manifolds.
• Finite-time extinction with surgery, simply connected case — every simply connected closed oriented smooth three-manifold, with any initial smooth Riemannian metric, admits a controlled finite surgery history ending in the empty manifold at a positive finite time. The extinction structure records the initial metric identification and the empty terminal stage.
• Moise's theorem: compatible smooth structures in dimension three — every compact Hausdorff topological three-manifold admits a smooth atlas compatible with its given topology. The development supplies PL approximation and compact PL smoothing, providing the bridge from smooth to topological Poincaré.
• Perelman's canonical neighborhood theorem — in a Ricci flow on a closed connected oriented three-manifold over a finite time interval, every point of sufficiently large scalar curvature lies in a controlled neck, cap, positively curved compact component, or nearly round component. The development also gives curvature-scale bounds for all mixed space-time curvature derivatives.
• Compactness of ancient κ-solutions — three-dimensional ancient κ-solutions with fixed κ and basepoint scalar curvature normalized to one admit smoothly convergent pointed subsequences with an ancient κ-solution limit, together with universal mixed curvature-derivative estimates.
• Hamilton's compactness theorem — complete connected pointed Ricci flows on a common open time interval, with uniform curvature bounds on compact time intervals and a uniform positive basepoint injectivity-radius bound at time zero, admit a smooth pointed Cheeger–Gromov–Hamilton convergent subsequence with a complete limit.
• Hamilton's theorem (1982) — a closed three-manifold admitting a positive-Ricci metric admits a constant-positive-sectional-curvature metric and is a spherical space form.
• Ricci flow short-time existence — on every closed Riemannian manifold $(M, g_0)$ the Ricci flow $\partial_t g = -2,\mathrm{Ric}_{g(t)}$ has a solution on some $[0, T)$ with $g(0) = g_0$, jointly smooth in $(t, x)$ up to and including the initial time. Proved via the DeTurck's trick and a conjugating flow of the DeTurck vector field.
• Perelman's reduced-volume monotonicity — along a Ricci flow on a closed connected manifold, the reduced volume is nonincreasing in backward time, built on the L-length minimizer, L-cut-locus, and reduced-Jacobian theory.
• Perelman's no local collapsing theorem — every smooth Ricci flow on a closed connected manifold over a finite time interval is uniformly κ-noncollapsed below any prescribed scale on curvature-controlled spacetime balls.
• Perelman's W-entropy monotonicity — along Ricci flow on a closed manifold, a positive conjugate-heat solution determines a W-entropy that is nonincreasing in backward time, with the exact integral-square derivative formula.
• Ricci–DeTurck flow short-time existence — the gauge-fixed, strictly parabolic flow behind the reduction: a solution whose chart-Gram entries are jointly smooth on the closed time slab, together with joint smoothness of the DeTurck vector field.
• Ricci-tensor naturality under diffeomorphisms — $\mathrm{Ric}_{\Phi^* g}(v, w) = \mathrm{Ric}_g(d\Phi, v, d\Phi, w)$, the equivariance that transports the DeTurck solution back to a Ricci flow.
• Scalar-curvature evolution under Ricci flow.
• Hamilton–Ivey pinching estimate — the scalar-curvature lower bound and logarithmic pinching estimate for closed three-dimensional Ricci flows with an initial curvature-operator lower bound, together with an asymptotic pinching estimate.
• Shi's derivative estimates — uniform curvature bounds and completeness of the initial metric give time-weighted bounds for every covariant derivative of curvature along Ricci flow.
• Hamilton's matrix Harnack inequality for Ricci flow — the matrix Harnack quadratic is nonnegative on closed Ricci flows with nonnegative curvature operator. In dimension three, nonnegative initial curvature operator suffices.
• Bonnet–Myers diameter bound — a positive Ricci lower bound forces a bounded diameter.
• Bochner formula — the polarised, pointwise form.
• Weitzenböck identity — the integrated $L^2$ form.
• Lichnerowicz eigenvalue bound on closed manifolds.
• Voss–Weyl divergence formula — the chart-invariant divergence.
• de Rham cohomology — intrinsic differential forms with nilpotent exterior derivative, graded Leibniz rule, and functorial pullback maps.
• Morse lemma, the no-critical-values theorem, and single-critical-point cell attachment, with smooth handle-adjunction diffeomorphisms.
• Elliptic variable-coefficient Schauder estimates and parabolic nondivergence Schauder estimates.
• Strong parabolic maximum principles — scalar equations on fixed and moving metrics, parallel proper cones, and symmetric tensors, with a Hopf boundary point theorem.
• Li–Yau Harnack inequality and Hamilton differential Harnack inequality for positive heat solutions.
• Quasilinear parabolic local existence for locally Lipschitz Sobolev nonlinearities.

Verification

git clone https://github.com/qinz1yang/differential-geometry.git
cd differential-geometry
lake build DifferentialGeometry.Topology.ThreeManifold.Poincare

To inspect the Poincaré theorem's transitive axioms, temporarily add

#print axioms DifferentialGeometry.Topology.poincare_conjecture

to Poincare.lean, then run

lake build DifferentialGeometry.Topology.ThreeManifold.Poincare

PDE infrastructure

Underlying these results is a substantial geometric-analysis backbone:

• Integration & the divergence theorem — Riemannian measures, integration by parts and surface measures, with and without boundary.
• Elliptic regularity — the connection (rough) Laplacian, Green identities, Gårding / Caccioppoli estimates, Hölder–Schauder spaces, variable-coefficient estimates, and interior bootstrap.
• Spectral theory — the scalar theory on closed manifolds (discrete Laplacian spectrum, compact resolvent, eigenbasis); an iterated covariant-gradient jet calculus for tensor fields with fibre-norm towers and Sobolev-scale spectral estimates; and the intrinsic heat-semigroup / Galerkin machinery driving the DeTurck flow.
• Sobolev spaces — chart-based and intrinsic $H^k$ / $W^{k,p}$ spaces with completeness, embedding and compactness results; tensor-valued Hilbert–Sobolev towers; Moser-type tame product estimates; and Gagliardo–Nirenberg interpolation down to fibre-norm level.
• Parabolic & heat equations — heat semigroups, Duhamel solutions, Schauder and maximal regularity, quasilinear local existence, strong maximum and Hopf principles, Harnack inequalities, and joint space-time smoothing.
• ODE flows — $C^\infty$ dependence of flows on their initial data, and time-dependent flows on closed manifolds jointly smooth up to the initial time (via Seeley-type time extension of the vector field).

The classical De Giorgi–Nash–Moser regularity machinery is vendored under External/ from scottnarmstrong/DeGiorgi (Scott Armstrong and Julia Kempe, Apache-2.0).

Topology Infrastructure

The topology library supplies the constructions used by Moise smoothing, surgery, and the Poincaré endpoint:

• PL topology, triangulation & smoothing — simplicial complexes, links and stars, subdivisions, PL balls and spheres, local charts, finite gluing, approximation and isotopy. Compact PL triangulations and smooth structures on compact topological three-manifolds connect the combinatorial and smooth developments.
• Fundamental groups, homotopy & coverings — path and homotopy lifting, covering transformations, deck groups, and based/free sphere-map constructions. The van Kampen development includes fundamental groups of finite connected sums.
• Homology, cohomology & orientation — singular chains, relative and local homology, excision, Mayer–Vietoris exactness, compactly supported cohomology, cap products, low-degree Hurewicz maps, local orientation classes and fundamental classes. These developments build on the vendored canonical-topology core.
• Morse theory & handles — Morse normal forms, regular-level transport, critical-point attachment, sublevel topology and smooth handle attachment, supported by handle and collar constructions.
• Three-manifold topology & surgery — sphere separation, connected sums, cutting and capping, reconstruction and orientation transport. Cut-and-cap reconstruction identifies the original manifold as a connected sum of capped components and sphere-product factors; simple connectivity is preserved by capping.
• Separation, embeddings & gluing — planar Jordan and Schoenflies tools, sphere separation, smooth embedding and extension APIs, collars, and adjunction spaces, with homeomorphism and diffeomorphism transport and gluing.

Third-party foundations are preserved under CanonicalTopology, ClassificationOfSurfaces, Schoenflies, and selected Tau Ceti modules, together with their source, license and modification records. Native extensions and theorem assembly remain in the mathematical topic directories.

AI Disclaimer

Generative AI (ChatGPT, Claude, Deepseek, Gemini, GLM, etc.) was used in the development of this codebase. The high-level architecture is human-designed; AI agents assisted with formalizing individual proofs and writing boilerplate. All definitions and core theorem statements were human-verified for correctness. Since all proofs are verified by Lean's type checker, AI-generated and human-written code are held to the same standard of correctness.

Note: This library is under active development. Breaking changes to public APIs and file paths should be expected.