{"id":"palomar/PALOMAR-2026-09-02-000004","url":"https://github.com/langlerangle/NashEmbedding/tree/515a8245c51c952db59d81ef840a146ed853e4ea","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000004-v1.json","repo":"https://github.com/langlerangle/NashEmbedding","tags":["math.DG","math.AP","msc:53C42","msc:53C21","msc:58J05","msc:46E35","differential-geometry","isometric-embedding","lean","riemannian-geometry"],"score":0,"title":"Nash's isometric embedding theorem for closed manifolds (Günther's proof)","trust":"high","domain":"math.DG","source":"palomar","authors":["David Wiygul"],"reviews":0,"subject":"math.DG","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-02","reactions":{},"formalized":true,"formalizes":[{"title":"On the perturbation problem associated to isometric embeddings of Riemannian manifolds","identifier":"","relationship":"adapts"},{"title":"The Atiyah-Singer Index Theorem, Part III lecture notes (Cambridge, Lent 2010): Sobolev spaces on the torus, Nash's embedding theorem for the N-torus, the reduction of the compact case","identifier":"","relationship":"formalizes"}]}