Differential geometry
The Lean Pool projects whose card's first MSC2020 code is in class 53, Differential geometry: 2 articles, one per card.
TheoremNash's smooth isometric embedding theorem#
A Lean 4 / Mathlib formalization of Nash's C^∞ isometric embedding theorem for closed manifolds: every compact smooth manifold without boundary, equipped with a smooth Riemannian metric, admits a smooth injective map into some Euclidean space ℝ^q whose differential pulls the Euclidean inner product back to the given metric. The proof formalized is Günther's (1989), which replaces the Nash-Moser iteration by an elliptic fixed-point argument, following the presentation in A. J. Wassermann's Cambridge Part III lecture notes as the primary source. The development has two layers. The first proves the theorem for the flat torus: a self-contained Sobolev toolkit on 𝕋ⁿ (weighted ℓ² Sobolev spaces on ℤⁿ, Rellich compactness, the Sobolev sup bound, three multiplication theorems, mollifiers, periodization, Fourier inversion and Parseval), the approximation of smooth metrics by realizable ones, Günther's perturbation theorem proved by a contraction in Hˢ, and their assembly into the statement that every smooth 2π-periodic positive-definite matrix field on ℝⁿ is the pullback metric of a smooth periodic immersion that is injective modulo 2πℤⁿ. The second layer reduces the closed-manifold case to the torus: a Whitney embedding from Mathlib is extended to the ambient space, the metric is extended by a pseudo-inverse construction, cut off, symmetrized and periodized, and the torus theorem is applied. No bound on the embedding dimension is claimed. Concrete instances (round spheres of every dimension, products of spheres, the flat torus 𝕊¹ × 𝕊¹) are derived, and the flat-torus instance is shown to reproduce the torus theorem's conclusion, tying the two layers together. Nothing here is claimed to be new.
Quoted from the card LeanPool/projects/nashembedding.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
NashEmbeddingTheorem.nash_isometric_embedding(theorem; a main declaration), declared in LeanPool/NashEmbedding/Solution.lean, line 38: “Every compact smooth boundaryless manifold with a smooth Riemannian metric admits a smooth isometric embedding in some finite-dimensional Euclidean space.”
Project
- Authors: David Wiygul.
- Project repository: langlerangle/nashembedding, at commit 515a8245.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: Apache-2.0.
- MSC2020: 53C24.
- In Lean Pool: LeanPool/NashEmbedding, from the card LeanPool/projects/nashembedding.yaml.
Sources
TheoremPlanar Euclidean dual-geodesic midpoint rigidity#
Complementary canonical local midpoints for two Euclidean dual torsion-free connections force their symmetric cubic tensor to be constant on a connected open planar domain. The proof constructs the local geodesic germs and derives the fourth-order obstruction, including its exceptional tensors. A differential strengthening needs only differentiability; five fixed direction tests suffice.
Quoted from the card LeanPool/projects/planar-midpoint-rigidity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.
Main results
The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.
PlanarMidpoint.planar_dual_midpoint_rigidity(theorem; a main declaration), declared in LeanPool/PlanarMidpoint/MidpointRigidity.lean, line 44: “On an open preconnected Euclidean planar domain, a smooth symmetric cubic tensor field whose canonical local dual geodesic midpoints sum to the endpoints is constant.”PlanarMidpoint.planar_midpoint_rigidity_C2(theorem), declared in LeanPool/PlanarMidpoint/MidpointRigidity.lean, line 31: “The geometric midpoint rigidity theorem already holds for C2 coefficient fields.”PlanarMidpoint.planar_obstruction_rigidity(theorem), declared in LeanPool/PlanarMidpoint/DifferentialRigidity.lean, line 109: “A differentiable planar cubic coefficient field is constant if its quartic midpoint obstruction vanishes at every point and in every direction.”PlanarMidpoint.planar_five_direction_rigidity(theorem), declared in LeanPool/PlanarMidpoint/FiveDirections.lean, line 28: “The differential obstruction criterion needs only the five directions (j, 1) for j = 0, 1, 2, 3, 4 at every point.”
Project
- Authors: JD Jones.
- Source: arXiv:2609.07551.
- The card's note on its source: “The upstream MIT-licensed original proof settles the dimension-two case of Nielsen–Okamura Conjecture 9.1 (v2, Section 9); the cited paper poses the general-dimensional conjecture and does not contain this planar necessity proof. Public completed source was released on 2026-10-08. Proofs and mathematical arguments were produced by OpenAI Codex agents under JD Jones's supervision.”
- Project repository: JD-Jones-ASES/PlanarMidpoint, at commit f277b89a.
- Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
- License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
- MSC2020: 53B12, 39B22.
- In Lean Pool: LeanPool/PlanarMidpoint, from the card LeanPool/projects/planar-midpoint-rigidity.yaml.
Sources
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.