Topology

Motivation

Many constructions in differential topology and infinite-dimensional Lie theory start from a continuous object and need a smooth one: a continuous section of a smooth bundle, a continuous map into a manifold, a continuous homotopy between smooth maps. Steenrod's approximation theorem (Steenrod 1951, §6.7) says that, for finite-dimensional bundles, a continuous section can be smoothed by a small homotopy through sections, without changing it where it is already smooth. Hirsch's textbook (Hirsch 1976, Ch. 2) gives the relative version for maps between finite-dimensional manifolds.

Gauge theory and the study of principal bundles whose structure group is an infinite-dimensional Lie group (current groups, diffeomorphism groups, gauge groups) need the same statement when the typical fibre is infinite-dimensional. C. Wockel (arXiv:math/0610252, 2006) proves it for a finite-dimensional base with corners and a fibre that is a manifold modelled on a locally convex space, combining Steenrod's argument with Neeb's approximation results for maps into locally convex spaces (Neeb 2002, App. A.3). The consequences in the paper are that smooth and continuous homotopy classes of sections, and of maps from a finite-dimensional manifold into a locally convex manifold, coincide; this is used in bundle theory for infinite-dimensional structure groups (Müller–Wockel 2006, cited as [MW06] in the paper).

Setting

A manifold with corners $M$ is a Hausdorff paracompact space with charts onto open subsets of the quadrant $\mathbb R^d_+ = \{x \in \mathbb R^d : x_i \ge 0\}$ and smooth coordinate changes. A locally convex manifold $N$ is a Hausdorff space with charts onto open subsets of a locally convex space and smooth coordinate changes, where smoothness of $f : U \to Y$ means that all iterated directional derivatives exist and are continuous (Definition 0.1 of the paper).

A map $\pi : E \to M$ is a locally trivial smooth bundle with typical fibre $N$ if every point of $M$ has an open neighbourhood $S$ and a diffeomorphism $\varphi : \pi^{-1}(S) \to S \times N$ with $\mathrm{pr}_1 \circ \varphi = \pi$. A section is a continuous map $\sigma : M \to E$ with $\pi \circ \sigma = \mathrm{id}_M$. A map is smooth on a neighbourhood of a set $s$ if it is smooth on some open set containing $s$.

For spaces $X, Y$, $C(X, Y)_{c.o.}$ is the space of continuous maps with the compact-open topology, generated by the sets $\lfloor C, W\rfloor = \{f : f(C) \subseteq W\}$ with $C$ compact and $W$ open.

Formalization targets

Goal: Theorem 0.11 (Generalised Steenrod Approximation Theorem)

Let $M$ be finite-dimensional and connected, $\pi : E \to M$ a locally trivial smooth bundle with typical fibre $N$, $\sigma$ a continuous section, $L \subseteq M$ closed, $U \subseteq M$ open, and $\sigma$ smooth on a neighbourhood of $L \setminus U$. Then for every open $O \supseteq \sigma(M)$ there are a section $\tau$ and a homotopy $H$ with

Milestones

1. Remark 0.4: a connected paracompact finite-dimensional manifold with corners is σ-compact.
2. Proposition 0.7: $C^\infty(M, Y)$ is dense in $C(M, Y)_{c.o.}$, with support control for compactly supported maps.
3. Corollary 0.8: $C^\infty(M, V)$ is dense in $C(M, V)_{c.o.}$ for $V \subseteq Y$ open.
4. Lemma 0.9: relative smoothing of $f : M \to W$, $W \subseteq Y$ open convex, within any compact-open neighbourhood, keeping $f$ off $U$.
5. Lemma 0.10: the same for maps into a subset $W \subseteq N$ diffeomorphic to an open convex subset of the model space.
6. Sections versus fibre maps (proof of Theorem 0.11, p. 5): over a smooth trivialisation $\varphi$, a section $\sigma'$ is smooth near $x$ if and only if $\mathrm{pr}_2 \circ \varphi \circ \sigma'$ is.

Significance

The result. The theorem turns continuous sections into smooth ones by homotopies that are small (they stay in any prescribed open set $O$ around the section) and relative (fixed where nothing needs changing). It yields that $C^\infty(M, N)$ is dense in $C(M, N)$ for the graph and compact-open topologies (Corollary 0.12), that every continuous section is homotopic to a smooth one and continuously homotopic smooth sections are smoothly homotopic (Proposition 0.13), and that smooth and continuous homotopy classes $[M, N]$ agree (Corollary 0.14). These are the statements needed to compare smooth and topological classification of bundles with infinite-dimensional structure groups.

Formalizing it. The theorem is proved in the paper; no machine-checked version exists. Mathlib has smooth partitions of unity on finite-dimensional manifolds with corners and local-to-global smoothing for maps into convex sets, but no density of $C^\infty(M, Y)$ in $C(M, Y)$ for the compact-open topology, no relative smoothing lemma, and no smoothing of sections of non-vector bundles. A formalization would supply these as reusable statements about Mathlib's ContMDiff, Bundle.Trivialization and C(M, Y).

Difficulty

The obvious argument glues local smoothings with a partition of unity, as for real-valued functions. This fails for sections of a non-linear bundle: convex combinations of points of $E$, or of $N$, are meaningless, so a partition-of-unity average of local smoothings is not a section, and the smoothing cannot be done in one global step. Any stepwise replacement must keep the section inside the prescribed open set $O$, must not destroy smoothness already achieved near earlier parts of $L$, and must avoid convergence arguments, since infinitely many steps are needed on a non-compact $M$. The homotopy has to be continuous at the end where infinitely many steps accumulate. Finally, an infinite-dimensional $N$ is not locally compact, so all compactness must come from $M$; this is why the base is finite-dimensional while the fibre is not.

Formalization scope

• Normed models. Mathlib's manifolds require a normed model space, so $N$ is modelled (without boundary) on a real normed space $F$, not necessarily complete or finite-dimensional, and the total space $E$ is a manifold with corners modelled on a real normed space; in Proposition 0.7, Corollary 0.8 and Lemma 0.9 the target $Y$ is a real normed space. On normed spaces the paper's smoothness coincides with Fréchet $C^\infty$, Mathlib's ContMDiff … ∞ (not the analytic ω). This is the one specialisation of the paper; non-normable locally convex fibres are out of scope.
• The base. $M$ carries any finite-dimensional Mathlib model with corners $I$ (which contains the quadrant $\mathbb R^d_+$), with [T2Space M], and [ParacompactSpace M] (Theorem 0.11, Remark 0.4, milestone 6) or [SigmaCompactSpace M] (Proposition 0.7, Corollary 0.8, Lemmas 0.9, 0.10), as Definition 0.3 and the statements require; Theorem 0.11 adds [ConnectedSpace M]. $N$ is [T2Space N].
• Conventions. "Smooth on a neighbourhood of $s$" is $C^\infty$ on an open set containing $s$ (SmoothNear), not smoothness on $s$ itself. Spaces $C(M, W)$ for $W \subseteq Y$ or $W \subseteq N$ are maps into the subtype with the compact-open topology, so neighbourhoods are taken in $C(M, W)$. A bundle is given by smooth Bundle.Trivializations covering $M$; "$W$ diffeomorphic to an open convex subset of $F$" is a partial diffeomorphism $N \to F$ with source $W$ and convex target. The homotopy is indexed by unitInterval and runs from $\sigma$ at $0$ to $\tau$ at $1$. "Support" is the closed support tsupport.
• No trivial reading. The goal must not be read with smoothness on $L$ only (which is weaker for closed $L$), with $O$ replaced by all of $E$, or with a trivial bundle or finite-dimensional fibre; a sanity file checks that the hypotheses are satisfiable on the product bundle $\mathbb R \times \mathbb R \to \mathbb R$.
• What a development needs. Smooth partitions of unity on $M$ (in Mathlib), local compactness and σ-compactness of $M$, the compact-open topology on $C(M, W)$ and continuity of the operations $\gamma \mapsto \lambda\gamma + (1-\lambda)f$ on it, and the gluing of sections along locally finite covers. Proofs of Proposition 0.7 and Lemma 0.9 are reusable beyond this mission; contributions proving any milestone, or the Mathlib-level density results, are welcome.

Selected references

• C. Wockel, A Generalisation of Steenrod's Approximation Theorem, preprint arXiv:math/0610252v1, 2006. https://arxiv.org/abs/math/0610252
• N. Steenrod, The Topology of Fibre Bundles, Princeton University Press, 1951, §6.7. https://doi.org/10.1515/9781400883875
• M. W. Hirsch, Differential Topology, Graduate Texts in Mathematics 33, Springer, 1976, Ch. 2. https://doi.org/10.1007/978-1-4684-9449-5
• K.-H. Neeb, Central extensions of infinite-dimensional Lie groups, Ann. Inst. Fourier 52 (2002), App. A.3 (cited as [Ne02]).
• C. Müller, C. Wockel, Equivalences of smooth and continuous principal bundles with infinite-dimensional structure group, preprint, 2006 (cited as [MW06]).
• J. Dugundji, Topology, Allyn and Bacon, 1966, Theorems XI.7.2–3.

Motivation

Every closed oriented 3-manifold bounds a compact oriented 4-manifold, but asking for a bounding 4-manifold with the homology of a point turns this into one of the long-standing questions of 3/4-manifold topology. The question, recorded on the Open Problem Garden as an outstanding problem of ancient/folklore origin, is whether there is a complete and computable set of invariants that determines which (rational) homology 3-spheres bound (rational) homology 4-balls (Open Problem Garden).

The question organizes the homology cobordism group $\Theta^3_{\mathbb Z}$ (integral homology spheres modulo homology cobordism): an integral homology sphere represents zero in $\Theta^3_{\mathbb Z}$ exactly when it bounds a smooth integral homology ball. It is also tied to the slice-ribbon problem, listed on the Open Problem Garden as a related problem.

Timeline (as recorded in the source's bibliography).

• 1952 — Rokhlin: the signature of a closed smooth spin 4-manifold is divisible by 16. The resulting Rokhlin invariant $\mu \in \mathbb Z/2$ shows that the Poincaré dodecahedral space $\Sigma(2,3,5)$ does not bound a smooth integral homology ball.
• 1961 — Mazur: contractible 4-manifolds whose boundary is a homology sphere different from $S^3$.
• 1979 — Akbulut–Kirby: the Brieskorn spheres $\Sigma(2,5,7)$, $\Sigma(3,4,5)$, $\Sigma(2,3,13)$ bound contractible (Mazur) 4-manifolds.
• 1981 — Casson–Harer: infinite families of Brieskorn spheres bounding contractible 4-manifolds, and lens spaces $L(m^2, mk-1)$ bounding rational homology balls.
• 1981 — Fintushel–Stern: $\Sigma(2,3,7)$ bounds a rational homology ball.
• 1984 — Fickle: further homology spheres bounding contractible 4-manifolds.
• 2007 — Lisca: complete classification of connected sums of lens spaces that bound rational homology balls.

Setting

A closed topological 3-manifold $M$ is a compact Hausdorff space locally homeomorphic to $\mathbb R^3$. Write $H_n(X;\mathbb Z)$ and $H_n(X;\mathbb Q)$ for singular homology. $M$ is an integral homology 3-sphere if $H_n(M;\mathbb Z) \cong H_n(S^3;\mathbb Z)$ for all $n$, and a rational homology 3-sphere if the same holds with $\mathbb Q$ coefficients.

A smooth integral homology 4-ball is a compact smooth 4-manifold $W$ with boundary such that $H_n(W;\mathbb Z) \cong H_n(\mathrm{pt};\mathbb Z)$ for all $n$; a rational homology 4-ball is defined with $\mathbb Q$ coefficients. $M$ bounds $W$ if the manifold boundary $\partial W$ is homeomorphic to $M$.

The Brieskorn manifold $\Sigma(p,q,r) = \{ z \in \mathbb C^3 : z_0^p + z_1^q + z_2^r = 0,\ |z| = 1 \}$ is an integral homology sphere when $p,q,r$ are pairwise coprime; $\Sigma(2,3,5)$ is the Poincaré homology sphere $P$. The lens space $L(p,q)$ is the quotient of $S^3 \subset \mathbb C^2$ by the $\mathbb Z/p$-action generated by $(z_0,z_1) \mapsto (\zeta z_0, \zeta^q z_1)$, $\zeta = e^{2\pi i/p}$.

To speak of algorithms, a 3-manifold is presented by a finite simplicial complex $K$, a list of simplices each given as a list of vertex labels in $\mathbb N$, with geometric realization $|K| \subseteq \mathbb R^{\mathbb N}$. Every closed 3-manifold is triangulable (Moise).

Formalization targets

Goal: decidability of bounding an integral homology ball

A complete and computable set of invariants is, in particular, a decision procedure; conversely a decision procedure is itself a complete computable invariant. The goal is stated for integral homology spheres and integral homology balls (the title question).

Milestones: what is known

Significance

A decision procedure would settle membership in the zero class of $\Theta^3_{\mathbb Z}$ for every presented homology sphere. Without one, each new example requires an ad hoc construction (to show bounding) or an obstruction (to rule it out). The known obstructions — the Rokhlin invariant, Siebenmann's $\overline{\mu}$-invariant, the Ozsváth–Szabó $d$-invariant and others — are spin or spin$^c$ cobordism invariants and are not known to be complete.

None of the milestone results is formalized in Lean. Formalizing even the milestones requires substantial infrastructure (smooth 4-manifolds with boundary, intersection forms, Rokhlin's theorem, explicit handle constructions), which is reusable well beyond this mission.

Difficulty

The answer to the goal is unknown; a disproof (undecidability) would equally resolve the mission. On the obstruction side, every known invariant is a homology cobordism invariant that is computable for special families but not known to detect bounding in general. On the construction side, homology balls are produced by explicit handle decompositions with no general recipe. The topological category is no substitute: by Freedman's work every integral homology 3-sphere bounds a contractible topological 4-manifold, so the problem lives entirely in the smooth category.

Formalization scope

• Homology is Mathlib's singular homology functor with coefficients in $\mathbb Z$ (resp. $\mathbb Q$), valued in modules; "has the homology of $X$" means an isomorphism of $H_n$ for every $n$.
• 3-manifolds are topological (an atlas modelled on $\mathbb R^3$); since every topological 3-manifold has a unique smooth structure up to diffeomorphism (Moise), "$\partial W$ homeomorphic to $M$" is the standard notion. Bounding 4-manifolds are compact, Hausdorff and $C^\infty$, modelled on the half-space $\{x \in \mathbb R^4 : x_0 \ge 0\}$. Orientations are not tracked: a homology ball bounded by $M$ also, with reversed orientation, bounds $-M$.
• $P \# (-P)$ is modelled as the double of $P$ minus an open chart ball, with the closed ball required to lie inside the chart.
• The goal's input is a list of simplices; the realization lives in $\mathbb R^{\mathbb N}$ with the product topology. The hypothesis "$|K|$ is an integral homology 3-sphere" makes this a promise problem: the algorithm is unconstrained on other inputs, which rules out trivializing via undecidability of recognizing manifolds.
• Natural-number subtraction appears only with hypotheses ensuring it does not truncate.

Selected references

• Open Problem Garden, Which homology 3-spheres bound homology 4-balls?, posted by rybu, 2009. http://www.openproblemgarden.org/op/which_homology_3_spheres_bound_homology_4_balls
• R. Kirby, The topology of 4-manifolds, Lecture Notes in Mathematics 1374, Springer-Verlag, 1989.
• V. A. Rokhlin, New results in the theory of four-dimensional manifolds, Doklady Akad. Nauk SSSR (N.S.) 84 (1952), 221–224.
• B. Mazur, A note on some contractible 4-manifolds, Annals of Mathematics (2) 73 (1961), 221–228.
• S. Akbulut, R. Kirby, Mazur manifolds, Michigan Math. J. 26 (1979), 259–284.
• A. Casson, J. Harer, Some homology lens spaces which bound rational homology balls, Pacific J. Math. 96 (1981), no. 1, 23–36.
• R. Fintushel, R. Stern, An exotic free involution on $S^4$, Ann. of Math. (2) 113 (1981), no. 2, 357–365.
• H. Fickle, Knots, $\mathbb Z$-homology 3-spheres and contractible 4-manifolds, Houston J. Math. 10 (1984), no. 4, 467–493.
• P. Lisca, Sums of lens spaces bounding rational balls, Algebr. Geom. Topol. 7 (2007), 2141–2164.

Motivation

A knot is a smooth simple closed curve $K$ in the $3$-sphere $S^3$. Since $S^3$ is the boundary of the $4$-ball $B^4$, one can ask whether $K$ bounds a smoothly embedded disc in $B^4$; if so, $K$ is called slice. Slice knots are the identity element of the smooth knot concordance group, so deciding which knots are slice is a central question of $4$-dimensional topology. A more restrictive and more combinatorial notion is that of a ribbon knot: a knot bounding an immersed disc in $S^3$ whose only self-intersections are ribbon singularities (arcs of double points whose two preimages are an interior arc and an arc running across the disc from boundary to boundary). Every ribbon knot is slice: pushing the interior of a ribbon disc into $B^4$ removes the double points. In 1962 R. H. Fox asked for the converse ([F]). The Open Problem Garden lists this slice–ribbon problem as Outstanding (source): given a knot in $S^3$ which is slice, is it a ribbon knot?

Timeline

• 1962 — Fox, Some problems in knot theory ([F]): asks whether every slice knot is ribbon.
• 1966 — Fox–Milnor: the Alexander polynomial of a slice knot factors as $f(t)f(t^{-1})$, the first obstruction to sliceness.
• 1982 — Gilmer ([G], Invent. Math. 66): lower bounds on the slice genus from Casson–Gordon invariants.
• 1983 — Hass ([H], Math. Proc. Cambridge Philos. Soc. 94): studies the problem through minimal surfaces in $B^4$; a knot bounding a minimal disc in $B^4$ is ribbon.
• 2007 — Lisca: the slice–ribbon conjecture holds for all $2$-bridge knots.
• 2008–2015 — Owens (arXiv:0802.2109), Greene–Jabuka (odd $3$-strand pretzel knots), Lecuona (families of Montesinos knots, arXiv:0910.4601): further families where slice implies ribbon.
• 2010 — Gompf–Scharlemann–Thompson: candidate counterexamples arising from fibered knots and Property 2R.
• The general question remains open.

Setting

Write $\mathbb R^4$ for Euclidean $4$-space (R4), $S^3=\{x:\|x\|=1\}$, $B^4=\{x:\|x\|\le1\}$, and $D^2=\{z\in\mathbb R^2:\|z\|\le 1\}$ for the closed unit disc in the parameter plane $\mathbb R^2$ (R2).

1. Knot (IsKnot γ). A map $\gamma:\mathbb R\to\mathbb R^4$ which is $C^\infty$, $1$-periodic, takes values in $S^3$, is injective on $[0,1)$, and has nowhere-vanishing velocity. The knot is the image $K=\gamma(\mathbb R)$.
2. Slice disc (IsSliceDisk γ F). A $C^\infty$ map $F:\mathbb R^2\to\mathbb R^4$ that is injective on $D^2$ with injective differential at every point of $D^2$, maps the open disc into the open ball, maps the unit circle onto $K$, and is transverse to $S^3$ along the boundary: $\langle F(z), dF_z(z)\rangle>0$ for $\|z\|=1$. A knot is slice (IsSlice γ) if it has a slice disc.
3. Ribbon disc (IsRibbonImmersedDisk γ f, Fox's definition). A $C^\infty$ map $f:\mathbb R^2\to\mathbb R^4$ that maps $D^2$ into $S^3$ with injective differential on $D^2$, maps the unit circle injectively onto $K$, has no triple points, has transverse double points, and whose double-point set in $D^2$ is a disjoint union of arcs $a_1,b_1,\dots,a_n,b_n$ with $f\circ a_i=f\circ b_i$, each $a_i$ contained in the open disc and each $b_i$ running from the boundary circle through the open disc back to the boundary circle. A knot is ribbon (IsRibbon γ) if it bounds a ribbon disc.
4. Ribbon slice disc (IsRibbonSliceDisk γ F). A slice disc on which the squared radial function $r_F(z)=\|F(z)\|^2$ is Morse in the open disc with no local maxima.
5. Minimal disc (IsMinimalOnDisk F). With $E=\langle\partial_0F,\partial_0F\rangle$, $G'=\langle\partial_0F,\partial_1F\rangle$, $G=\langle\partial_1F,\partial_1F\rangle$, the vector $G\,\partial_0\partial_0F-2G'\,\partial_0\partial_1F+E\,\partial_1\partial_1F$ is tangent to the surface at every interior point, i.e. the mean curvature vector of $F$ vanishes on the open disc.

Formalization targets

Goal: slice implies ribbon

Milestones

1. [F] Ribbon knots are slice — the converse direction, observed by Fox.
2. Ribbon discs in $S^3$ versus ribbon discs in $B^4$ — a knot is ribbon iff it bounds a slice disc on which the radial function is Morse without local maxima.
3. [H] Hass — a knot bounding a minimal slice disc in $B^4$ is ribbon.

A further (non-milestone) sanity item asserts that the round unknot $t\mapsto(\cos 2\pi t,\sin 2\pi t,0,0)$ is a ribbon knot, which shows that the definitions are not vacuous.

A supporting (non-milestone) item isolates the maximum-principle step behind [H]: on a minimal disc, the radial function $\|F\|^2$ has no local maximum in the open disc.

Significance

A positive answer would make sliceness, a $4$-dimensional property defined by the existence of an embedded disc in $B^4$, equivalent to a $3$-dimensional property that can be certified by a finite diagrammatic object (a ribbon presentation). A counterexample would exhibit a slice knot whose slice discs all need local maxima of the radial function; several proposed candidates (Gompf–Scharlemann–Thompson) are tied to the smooth $4$-dimensional Poincaré conjecture and to Property 2R. The problem is closely related to the question of which homology $3$-spheres bound homology $4$-balls.

On the formal side no part of this theory is in Mathlib: there are no knots, no slice or ribbon discs, no Morse functions on surfaces and no minimal surfaces. The milestones (Fox's easy direction, the $3$D/$4$D equivalence, Hass's theorem) are classical theorems that have not been machine-checked; formalizing them builds the infrastructure any later attack needs.

Difficulty

Turning a slice disc into a ribbon disc requires removing the local maxima of the radial function on the disc. Cancelling a maximum against a saddle is possible only when the handles are in suitable position, and there is no known procedure that achieves this in general; the known positive results rely on classifying the rational homology balls bounded by branched double covers, using Donaldson's diagonalization theorem, which applies only to special families of knots.

Formalization scope

Everything is stated in Euclidean coordinates: knots are periodic parametrisations $\mathbb R\to S^3\subset\mathbb R^4$, discs are $C^\infty$ maps $\mathbb R^2\to\mathbb R^4$ whose restriction to $D^2$ is the disc in question. Smoothness is $C^\infty$; slice discs are required to be smooth up to the boundary and transverse to $S^3$ there (the standard notion of a properly embedded disc). The knot enters only through its image, so orientation and parametrization play no role. The problem is the smooth one; topologically locally flat slice discs are not allowed. Definitions under which the conjecture holds trivially (for example, a ribbon condition implied by the slice condition by definition) are excluded: the goal uses Fox's $3$-dimensional ribbon discs, and the $4$-dimensional characterisation is a separate milestone.

Contributions welcome: smooth embedded discs and their collars, Morse theory for functions on $D^2$, the push-in construction, and minimal-surface tools (the maximum principle for $\|x\|^2$ on minimal surfaces).

Selected references

• [F] R. H. Fox, Some problems in knot theory, Topology of 3-manifolds and related topics (Proc. Univ. of Georgia Institute, 1961), Prentice-Hall, 1962, pp. 168–176.
• [G] P. M. Gilmer, On the slice genus of knots, Invent. Math. 66 (1982), 191–197.
• [H] J. Hass, The geometry of the slice-ribbon problem, Math. Proc. Cambridge Philos. Soc. 94 (1983), 101–108.
• A. G. Lecuona, On the slice-ribbon conjecture for Montesinos knots, arXiv:0910.4601.
• B. Owens, On slicing invariants of knots, arXiv:0802.2109.
• P. Lisca, Lens spaces, rational balls and the ribbon conjecture, Geom. Topol. 11 (2007), 429–472. https://doi.org/10.2140/gt.2007.11.429
• R. E. Gompf, M. Scharlemann, A. Thompson, Fibered knots and potential counterexamples to the Property 2R and slice-ribbon conjectures, Geom. Topol. 14 (2010), 2305–2347. https://doi.org/10.2140/gt.2010.14.2305
• Open Problem Garden, Slice-ribbon problem (posted by rybu, 2009). http://www.openproblemgarden.org/op/slice_ribbon_problem

Motivation

The generalized Poincaré conjecture asks whether a closed $n$-manifold with the homotopy type of the sphere $S^n$ must be the sphere. In the topological category (conclusion: homeomorphic) it is now known in every dimension: $n = 1, 2$ classically, $n \ge 5$ by Smale (and Stallings, Newman), $n = 4$ by Freedman (1982), and $n = 3$ by Perelman (2003). In the smooth category (conclusion: diffeomorphic) it fails in general: Milnor (1956) found exotic smooth structures on $S^7$, and Kervaire–Milnor showed that exotic spheres exist in many dimensions. The single case that remains completely open is the smooth one in dimension $4$; the Open Problem Garden rates it Outstanding.

Timeline

• 1904 — Poincaré raises the question for 3-manifolds.
• 1956 — Milnor: exotic smooth 7-spheres.
• 1960–62 — Smale (and Stallings): the topological Poincaré conjecture for $n \ge 5$.
• 1963 — Kervaire–Milnor: classification of homotopy spheres in dimensions $\ge 5$.
• 1982 — Freedman: the topological Poincaré conjecture for $n = 4$.
• 1982–87 — Donaldson, Freedman, Gompf, Taubes: exotic $\mathbb{R}^4$'s, in fact a continuum of them.
• 2002–03 — Perelman: the Poincaré conjecture for $n = 3$ (see Morgan–Tian).

Setting

All manifolds are Hausdorff, compact, without boundary and smooth ($C^\infty$). The model sphere is $S^n = \{x \in \mathbb{R}^{n+1} : \|x\| = 1\}$ with its standard smooth structure. Two spaces have the same homotopy type if there is a homotopy equivalence between them.

Formalization targets

Goal

This is the conjecture exactly as stated in the source.

Significance

By Freedman's theorem a homotopy 4-sphere is already homeomorphic to $S^4$, so the conjecture is equivalent to the statement that $S^4$ has no exotic smooth structure. It would complete the generalized Poincaré conjectures in the smooth category in the one dimension where the answer is unknown. A disproof would give the first exotic smooth structure on a closed simply connected 4-manifold with small homology.

Difficulty

The h-cobordism technology that settles dimensions $\ge 5$ (the Whitney trick) fails in dimension 4. Freedman's topological methods give a homeomorphism but no smoothing, and gauge-theoretic invariants (Donaldson, Seiberg–Witten) give no information on homotopy 4-spheres. Many candidate counterexamples (Gluck twists, Cappell–Shaneson spheres) have since been shown to be standard.

Formalization scope

Manifolds use Mathlib's ChartedSpace (EuclideanSpace ℝ (Fin n)) M together with IsManifold (𝓡 n) ∞ M. The model with corners 𝓡 n has no boundary, and ∞ means $C^\infty$ (not analytic). The sphere is Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1 with Mathlib's standard smooth structure. A homotopy equivalence is ContinuousMap.HomotopyEquiv, and diffeomorphisms are Diffeomorph (≃ₘ^∞⟮𝓡 n, 𝓡 n⟯). Closedness is CompactSpace plus T2Space; second countability follows from compactness. The milestones are the known results the source cites: low dimensions, Perelman, Smale, Milnor's exotic spheres, Freedman, and the continuum of exotic $\mathbb{R}^4$'s. They also include the equivalent reformulation "there is no exotic $S^4$". Formalizing any of them requires substantial new manifold-topology infrastructure in Mathlib, and that work is welcome.

Selected references

• M. Freedman, F. Quinn, Topology of 4-manifolds, Princeton University Press, 1990.
• S. Smale, On the structure of manifolds, Amer. J. Math. 84 (1962), 387–399.
• J. Morgan, G. Tian, Ricci Flow and the Poincaré Conjecture, AMS/CMI, 2007.
• J. Milnor, On manifolds homeomorphic to the 7-sphere, Ann. of Math. 64 (1956), 399–405.
• C. Taubes, Gauge theory on asymptotically periodic 4-manifolds, J. Differential Geom. 25 (1987), 363–430.
• Open Problem Garden, Smooth 4-dimensional Poincaré conjecture.

Motivation

The Schoenflies problem asks whether a codimension-one sphere sitting smoothly inside a sphere can be knotted. In every dimension except one the answer is known to be "no"; the remaining case, a smooth $3$-sphere in $S^4$, is listed as an outstanding problem in the Open Problem Garden (source). It is one of the central open questions of smooth $4$-manifold topology, closely tied to the existence of exotic smooth structures on the $4$-ball and to the smooth $4$-dimensional Poincaré conjecture.

Timeline.

• Early 1900s — Schoenflies: every Jordan curve in the plane bounds a disc (the case $n = 1$ below).
• 1924 — Alexander: every (polyhedral, hence smooth) $2$-sphere in $S^3$ bounds a $3$-ball on each side (PNAS); a modern exposition is in Hatcher's notes on $3$-manifolds.
• 1959–1960 — Mazur (Bull. AMS) and Brown (Bull. AMS): the generalized Schoenflies theorem. A (locally flat) embedded $S^n \subset S^{n+1}$ bounds a topological $(n+1)$-ball on each side, in every dimension.
• 1960s — The $h$-cobordism theorem implies that $D^{n+1}$ has no exotic smooth structure restricting to the standard one on the boundary when $n \ge 4$. Combined with Mazur–Brown, this settles the smooth problem for $n \ge 4$.
• 1984–2008 — Scharlemann proves the smooth $4$-dimensional statement for restricted classes of embeddings: genus-two embeddings (Topology 23, 1984), spheres with four critical points (Invent. Math. 79, 1985), and further cases via Generalized Property R (Comment. Math. Helv. 83, 2008).
• The case $n = 3$ remains open.

Setting

For $n \ge 0$ let $S^n = \{x \in \mathbb{R}^{n+1} : \|x\| = 1\}$ be the unit sphere with its standard smooth structure, and let $D^{n+1} = \{x \in \mathbb{R}^{n+1} : \|x\| \le 1\}$ be the closed unit ball. In the Lean development $S^n$ is Sph n.

A smooth embedding $f : S^n \to S^{n+1}$ is a $C^\infty$ map that is injective and whose differential $df_x$ is injective at every point (an injective immersion; since $S^n$ is compact this is an embedding). Its image $M = f(S^n)$ is a smooth $n$-dimensional submanifold of $S^{n+1}$ diffeomorphic to $S^n$ (Lean predicate IsSmoothEmbeddingSph n f).

By the Jordan–Brouwer separation theorem, $S^{n+1} \setminus M$ has exactly two connected components, and $M$ is the frontier of each. Their closures are compact connected $(n+1)$-manifolds with common boundary $M$.

A subset $K \subseteq S^{n+1}$ is a smoothly embedded closed ball if it is diffeomorphic to $D^{n+1}$ (with the smooth structure inherited from $S^{n+1}$). Concretely, $K = e(D^{n+1})$ for a $C^\infty$ map $e : \mathbb{R}^{n+1} \to S^{n+1}$ that is injective on $D^{n+1}$ and has injective differential at every point of $D^{n+1}$, boundary points included (Lean predicate IsSmoothClosedBallIn n K). The topological counterpart, $K$ homeomorphic to $D^{n+1}$, is IsTopClosedBallIn n K.

Formalization targets

Goal: the smooth Schoenflies problem in dimension 4

For every smooth embedding $f : S^3 \to S^4$ and every point $x \in S^4 \setminus f(S^3)$, writing $C_x$ for the connected component of $S^4 \setminus f(S^3)$ containing $x$,

Equivalently: $f(S^3)$ is unknotted.

Milestones (known results)

1. Jordan–Brouwer separation, all $n$: $S^{n+1} \setminus f(S^n)$ has exactly two components, each with frontier $f(S^n)$.
2. Generalized Schoenflies theorem (Mazur, Brown), all $n$: each $\overline{C_x}$ is homeomorphic to $D^{n+1}$.
3. Schoenflies, $n = 1$: each $\overline{C_x}$ is diffeomorphic to $D^2$.
4. Alexander, $n = 2$: each $\overline{C_x}$ is diffeomorphic to $D^3$.
5. High dimensions, $n \ge 4$: each $\overline{C_x}$ is diffeomorphic to $D^{n+1}$.

Significance

The result itself. By milestone 2, $M$ always bounds two topological $4$-balls. So a counterexample to the goal would produce an exotic smooth structure on $D^4$ that embeds in $S^4$; a proof would show that no exotic $D^4$, if one exists, embeds in $S^4$. The problem is related to, but independent of, the smooth $4$-dimensional Poincaré conjecture. For example, the Poincaré conjecture could hold while $D^4$ carries an exotic smooth structure. The goal also completes the uniform statement "every smooth $S^n \subset S^{n+1}$ is unknotted" across all dimensions.

Formalizing it. The goal is open. Milestones 1–5 are classical theorems, and no existing machine-checked proof of them for smooth spheres is relied on here. Formalizing them is substantial independent work and would add basic infrastructure to Mathlib's manifold library: separation theorems, collars, and smoothing of balls.

Difficulty

The topological statement is known in every dimension (milestone 2), so the difficulty is purely smooth. In dimensions $\ge 5$ the passage from "homeomorphic to a ball" to "diffeomorphic to a ball" goes through the $h$-cobordism theorem. That theorem fails in the smooth category in dimension $4$, because the Whitney trick is unavailable. Freedman's topological methods do not control smooth structures. The naive approach is to apply the high-dimensional argument verbatim, and this breaks at exactly this step. Known partial results (Scharlemann) need strong restrictions on the embedding, such as genus bounds or few critical points of a height function.

Formalization scope

• Spheres are the unit spheres in EuclideanSpace ℝ (Fin (n+1)), with Mathlib's standard smooth manifold structure modelled on EuclideanSpace ℝ (Fin n). Smoothness means $C^\infty$ (ContMDiff … ∞), not analytic.
• A smooth embedding of $S^n$ is encoded as a $C^\infty$ injective immersion (injective mfderiv everywhere). This is equivalent because $S^n$ is compact.
• "Diffeomorphic to $D^{n+1}$" is encoded as the image of the closed unit ball under a globally $C^\infty$ map $\mathbb{R}^{n+1} \to S^{n+1}$ that is injective with injective differential on the closed ball. Requiring smoothness on all of $\mathbb{R}^{n+1}$ loses no generality: a map smooth on a neighbourhood of the ball can be precomposed with a smooth radial retraction.
• The components of the complement are connectedComponentIn (Set.range f)ᶜ x for $x \notin f(S^n)$. The conclusion is required for every such $x$, so for both sides of $M$.
• The statement does not hold vacuously: the hypotheses are satisfied by the standard equator, and the immersion condition rules out degenerate maps, since a non-differentiable map has zero mfderiv, which is not injective.
• A complete development needs collar neighbourhoods, separation theorems for smooth hypersurfaces, and tools for comparing smooth structures on balls. Contributions to any milestone are welcome.

Selected references

• Open Problem Garden, Smooth 4-dimensional Schoenflies problem (posted by rybu, 2009). https://www.openproblemgarden.org/op/smooth_4_dimensional_schoenflies_problem
• J. W. Alexander, On the subdivision of 3-space by a polyhedron, Proc. Nat. Acad. Sci. USA 10 (1924), 6–8. https://doi.org/10.1073/pnas.10.1.6
• B. Mazur, On embeddings of spheres, Bull. Amer. Math. Soc. 65 (1959), 59–65. https://doi.org/10.1090/S0002-9904-1959-10274-3
• M. Brown, A proof of the generalized Schoenflies theorem, Bull. Amer. Math. Soc. 66 (1960), 74–76. https://doi.org/10.1090/S0002-9904-1960-10400-4
• M. Morse, E. Baiada, Homotopy and homology related to the Schoenflies problem, Ann. of Math. 58 (1953), 142–165.
• M. Freedman, F. Quinn, Topology of 4-manifolds, Princeton University Press, 1990.
• M. Scharlemann, The four-dimensional Schoenflies conjecture is true for genus two imbeddings, Topology 23 (1984), 211–217.
• M. Scharlemann, Smooth spheres in $\mathbb{R}^4$ with four critical points are standard, Invent. Math. 79 (1985), 125–141.
• M. Scharlemann, Generalized Property R and the Schoenflies conjecture, Comment. Math. Helv. 83 (2008), 421–449.
• A. Hatcher, Notes on basic 3-manifold topology. http://www.math.cornell.edu/~hatcher/3M/3Mdownloads.html