Nash's isometric embedding theorem for closed manifolds (Günther's proof)
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-02-000004
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-02-000004/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-02-000004/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'