Motivation: an intrinsic manifold in a fixed Euclidean space

A smooth manifold is a space that can be described locally by real coordinates, even when no single coordinate chart describes the whole space. Differential geometry works with these local descriptions, whereas an embedding realizes the entire space inside one Euclidean space without losing either its topology or its infinitesimal geometry. The strong Whitney embedding theorem supplies a dimension bound depending only on the dimension of the manifold. This mission targets the precise version selected by LeanEval v1, rather than a substitute formulation.

The benchmark attributes the strong result to Hassler Whitney's 1944 paper and distinguishes it from the earlier bound of $2n+1$. The result is a known mathematical theorem; the remaining task here is its formal proof in Lean. The exact benchmark declaration is authoritative for the target and its hypotheses, not a reconstruction from the historical literature (source and attribution).

Setting: topology, smoothness, and the differential

Let $n$ be a natural number satisfying $1\le n$. Let $M$ carry a topology and a smooth atlas modeled on $\mathbb R^n$, with the usual model having no boundary. The topology is Hausdorff: distinct points admit disjoint neighborhoods. It is second countable: there is a countable collection of open sets from which every open set can be assembled as a union. These are explicit hypotheses, alongside the chosen charted-space and smooth-manifold structures, in the Lean statement.

A topological embedding is a map that is a homeomorphism onto its image, where the image has the subspace topology inherited from the codomain. An immersion has an injective differential at every point. For a smooth map $e$, write $d e_x$ for the induced linear map on tangent spaces at $x$. These are separate requirements: the target asks for global topological embedding and pointwise injectivity of the differential together, as well as infinite differentiability. Their precise Lean meanings are the existing Mathlib predicates used directly by the benchmark, not new mission-specific definitions.

Formalization target: the single root theorem

For every $n\ge1$ and every $M$ with the structures and hypotheses just stated, establish

$$\exists e:M\longrightarrow\mathbb R^{2n},\qquad e\in C^\infty(M,\mathbb R^{2n}) \ \land\ e\text{ is a topological embedding} \ \land\ \forall x\in M,\ d e_x\text{ is injective}.$$

The codomain has dimension exactly $2n$. The quantifier ranges over all such manifolds, including noncompact ones. There is exactly one goal theorem and no auxiliary theorem items, definition items, or milestones. The declaration is LeanEval.Geometry.WhitneyEmbeddingProblem.whitney_embedding, with the binders and conclusion preserved from the benchmark source.

Significance: the full theorem rather than an easier restriction

The result realizes the given manifold in a Euclidean space with a uniform dimension bound. Its value in this formulation is the simultaneous control of topology, smoothness, and the differential, without a compactness assumption. Replacing the image-topology condition with mere injectivity would omit part of the requested conclusion; replacing $2n$ with an unspecified dimension would omit the quantitative constraint. Both distinctions are explicit in the benchmark's explanation.

A completed formalization would supply a reusable strong embedding theorem on top of Mathlib's manifold language. This is a long-term infrastructure task, not a claim that a short proof is available. The September 5, 2026 LeanEval v1 snapshot supplied for this task records no accepted benchmark credit for this target. That dated benchmark status is not a claim about all formalization projects, and preparing an open theorem statement does not establish the theorem or earn benchmark credit.

Difficulty: the dimension bound and the noncompact scope

The existing compact embedding result discussed by the benchmark provides an embedding into some finite-dimensional Euclidean space. That does not settle the present goal: it assumes compactness and does not supply the $2n$ bound. Consequently, simply invoking that result cannot discharge the unrestricted benchmark statement. The source identifies substantial differential-topological infrastructure behind the strong theorem; this proposal does not advertise an easy proof or prescribe a decomposition (benchmark discussion).

All positive dimensions remain in scope, including $n=1$ and $n=2$. Noncompactness is not a later extension or optional strengthening. The absence of an assumption must not be replaced by an implicit restriction in a new definition or an easier surrogate theorem.

Formalization scope: unchanged Mathlib predicates

The source model is EuclideanSpace ℝ (Fin n), and the target is EuclideanSpace ℝ (Fin (2 * n)). Smoothness is expressed by ContMDiff (𝓡 n) (𝓡 (2 * n)) ∞ e; the other two conjuncts are IsEmbedding e and pointwise Function.Injective of mfderiv. The type $M$ remains universe-polymorphic. No compactness, connectedness, orientability, or nonemptiness hypothesis is added. The empty manifold is included; dimension zero is excluded. Neither properness nor closedness of the image is demanded by the conclusion (exact declaration).

Mathlib already provides the vocabulary needed to state the goal: Euclidean spaces, charts, manifold smoothness, topological embeddings, and manifold derivatives. No custom definition item is necessary. Future proof work may develop reusable infrastructure, but this draft contains only the root theorem and intentionally imposes no supporting targets. A proof must establish that exact statement, not the compact-only, immersion-only, or weak $2n+1$ alternative.

Selected references

• LeanEval contributors, Whitney embedding theorem (strong form, sharp dimension 2n), LeanEval v1 source declaration and manifest, statement revision 1, pinned source and manifest. These specify the exact formal target.
• H. Whitney, The self-intersections of a smooth n-manifold in 2n-space, Annals of Mathematics (2) 45 (1944), 220–246, DOI. Historical attribution as recorded in the LeanEval manifest; no alternate statement from this reference replaces the benchmark goal.