Geometry & Topology

Motivation

The smooth four-dimensional Poincaré conjecture asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of K3 — A New Problem List in Low-Dimensional Topology. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. Baykur–Kirby–Ruberman, Problem 4.1

Historical landmarks

• 1961: Smale proved that a closed smooth manifold homotopy equivalent to a sphere of dimension at least five is homeomorphic to that sphere. This is not a theorem that all such smooth manifolds are diffeomorphic to the standard sphere. Smale, Theorem A
• 1982: Freedman established the topological four-dimensional Poincaré theorem: a topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to it. Freedman, Theorem 1.6
• 2026: The K3 problem list continues to distinguish this established topological result from the open smooth sphere problem. Problem 4.1, pp. 191–192

Setting

Let $S^4$ be the unit sphere in $ℝ^5$, with its standard stereographic smooth structure. A homeomorphism is a continuous bijection with continuous inverse; a diffeomorphism is a smooth bijection with smooth inverse. A smooth atlas is a collection of local Euclidean coordinates whose transition maps are smooth.

The manifold $M$ is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on $ℝ^4$. The given atlas is arbitrary: it is not defined by transporting the standard structure from $S^4$.

For a homeomorphism $e:N\to S^4$, let $\mathcal A_e$ denote the atlas transported from the standard sphere along $e$. A structomorphism for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate $\mathsf{SPC4Pullback}$ requires, for every given smooth atlas $\mathcal A$ on such an $N$ and every such $e$, a structomorphism between $(N,\mathcal A)$ and $(N,\mathcal A_e)$. It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, SPC4.lean, lines 53–81 and 211–221]

Formalization targets

Main open goal

For every manifold $M$ with the preceding hypotheses, the goal is

$$M\cong_{\mathrm{Top}}S^4 \quad\Longrightarrow\quad M\cong_{\mathrm{Diff}}S^4.$$

This is the source predicate $\mathsf{SPC4}$. Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.

Structural and literature milestones

The atlas formulation has the exact equivalence

$$\mathsf{SPC4}\quad\Longleftrightarrow\quad\mathsf{SPC4Pullback}.$$

The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence

$$\operatorname{Structomorph}(\mathcal G^{\infty},M,N) \simeq \operatorname{Diff}^{\infty}(M,N),$$

where $\mathcal G^{\infty}$ is the smooth coordinate-change groupoid for the common model. [Shin, SPC4.lean, lines 334–365; Bridge.lean]

Write $F_4$ for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:

$$M\simeq S^4\quad\Longrightarrow\quad M\cong_{\mathrm{Top}}S^4,$$

where $\simeq$ denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If $\mathsf{SPC4Homotopy}$ denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:

$$F_4\quad\Longrightarrow\quad (\mathsf{SPC4}\Longleftrightarrow\mathsf{SPC4Homotopy}).$$

Explicit standard-disk foundations form another track. For every $m\geq0$, they concern the manifold-with-boundary structure on $\overline B^{m+1}$, its boundary set $S^m$, and the smooth collar

$$c:S^m\times[0,1]\longrightarrow\overline B^{m+1}, \qquad c(u,t)=(1-t/2)u.$$

The collar is a closed embedding, has image

$$\{z\in\overline B^{m+1}:\|z\|\geq1/2\},$$

and satisfies $c(u,0)=u$, using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a $C^k$ map from a $C^k$ manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is $C^k$. These targets concern the actual disk smooth structure. [Shin, Disk.lean, lines 1076–1141 and 1263–1318]

Topological two-disk gluing

For each integer $m\geq0$, let $D^{m+1}=\overline B^{m+1}$ be the closed unit disk in $\mathbb R^{m+1}$ and let $\varphi:S^m\to S^m$ be any homeomorphism of its boundary. The twisted double identifies the boundary point $u$ in a left copy of the disk with $\varphi(u)$ in a right copy. With the quotient topology, the target is

$$X_\varphi:=\bigl(D^{m+1}_L\sqcup D^{m+1}_R\bigr)/(u_L\sim\varphi(u)_R) \quad\cong_{\mathrm{Top}}\quad S^{m+1}.$$

This statement is published as SP4Gluing.twistedSphere_homeomorphic. The theorem and its supporting continuity and injectivity lemmas have accepted Lean proofs contributed by carlok. All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.

Seam–interior smooth compatibility

For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth $\varphi^{-1}$; the reverse requires smooth $\varphi$. The single compatibility target concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, Hemisphere.lean, lines 2439–3577]

Significance

A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.

The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.

The topological two-disk gluing result identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.

Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by wamlart: orbit augmentation, region homology budgets, two-corner homology budgets, the Laurent mass threshold, and mass-two positivity. No theorem currently connects their completion to a proof or disproof of $\mathsf{SPC4}$. They are exploratory tools, not established milestones in a proof of the main goal.

Difficulty

A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.

Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.

Formalization scope

The sphere goal quantifies over Type in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order $\infty$. Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.

The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every $m\geq0$, so their dimensions are $m+1\geq1$. The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.

The separate source assertion SPC4Ball is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.

Selected references

• R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., K3 — A New Problem List in Low-Dimensional Topology, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. Author PDF.

• Michael Hartley Freedman, The topology of four-dimensional manifolds, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. DOI; primary-article scan.

• Stephen Smale, Generalized Poincaré's Conjecture in Dimensions Greater Than Four, Annals of Mathematics 74 (1961), 391–406, Theorem A. DOI; primary-article scan.

• Ryan Shin, SPC4.lean, Bridge.lean and Disk.lean, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc, e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302, 889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e.

• Ryan Shin, Hemisphere.lean, unpublished Lean source file, 2026, declaration twistedSphereHomeoSphere; source SHA-256 c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828. Published topological two-disk gluing target; the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.

Motivation

In 1935 Werner Burau attached to every braid on $n$ strands a matrix over the ring of Laurent polynomials $\mathbb{Z}[t,t^{-1}]$. The resulting homomorphism $\rho_n : B_n \to \mathrm{GL}_n(\mathbb{Z}[t,t^{-1}])$ is the oldest and most studied linear representation of the braid group, and whether it is faithful — whether a nontrivial braid can act as the identity matrix — became one of the best known questions about braid groups.

The history is short and sharp:

• 1969 — Magnus and Peluso prove that $\rho_3$ is faithful, by a direct algebraic computation.
• 1991 — Moody proves $\rho_n$ is not faithful for $n \ge 9$.
• 1993 — Long and Paton improve this to $n \ge 6$.
• 1999 — Bigelow settles $n = 5$: $\rho_5$ is not faithful.
• This left exactly one open case, $n = 4$, which appears as Question 3.1 in Margalit's problem list for mapping class groups.
• 2026 — Bharathram, Birman and Brendle prove that $\rho_4$ is faithful (arXiv:2607.05283), closing the last case.

Setting

Let $n \ge 1$. The braid group $B_n$ is taken here in Artin's presentation: generators $\sigma_1,\dots,\sigma_{n-1}$ subject to

$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1}.$$

Let $R = \mathbb{Z}[t,t^{-1}]$. The unreduced Burau representation is the homomorphism

$$\rho_n : B_n \longrightarrow \mathrm{GL}_n(R), \qquad \sigma_i \longmapsto I_{i-1} \oplus \begin{pmatrix} 1-t & t \\ 1 & 0\end{pmatrix} \oplus I_{n-i-1},$$

i.e. the identity matrix altered only in the two rows and columns $i$, $i+1$. That these matrices satisfy the two families of braid relations — so that $\rho_n$ is well defined — is proved in the mission's definition file, together with the invertibility of each generator matrix (its inverse is the identity altered by the block $\begin{pmatrix} 0 & 1 \\ t^{-1} & 1-t^{-1}\end{pmatrix}$).

Equivalently, $\rho_n$ is the action of the mapping class group of the $n$-punctured disk $D_n$ on the relative homology $H_1(\widetilde{D_n}, \{\tilde p_*\})$ of the infinite cyclic cover determined by total winding number; this is the description used throughout the source paper.

A representation is faithful when it is injective.

Target

The goal of the mission is the Main Theorem of the paper:

$$\rho_4 : B_4 \longrightarrow \mathrm{GL}_4(\mathbb{Z}[t,t^{-1}]) \ \text{ is injective.}$$

The milestones are three supporting results, each of which can be attacked independently:

1. Theorem 4.1 (Magnus–Peluso). $\rho_3$ is injective. The paper gives a new topological proof of this classical statement, and the same argument is the model for the four-strand case.
2. Observation 2.1. If a braid $\Phi \in B_n$ satisfies $\rho_n(\Phi) = I$, then its image under the standard inclusion $B_n \hookrightarrow B_{n+1}$ (add one unbraided strand) satisfies $\rho_{n+1}(\iota(\Phi)) = I$. The paper uses this to move a four-strand braid into $B_5$, where a parity obstruction can be applied.
3. Long's criterion ([Long 1986, Theorem 2.2], quoted in Section 1 of the paper). If $N \trianglelefteq B_n$ is nontrivial and not contained in the centre, and $\rho_n$ is injective on $N$, then $\rho_n$ is injective. This is what reduces the Main Theorem to faithfulness on the Brunnian subgroup $\mathrm{Brun}_4$.

Significance

Faithfulness of $\rho_4$ closes the classification of the faithful Burau representations: $\rho_n$ is faithful exactly for $n \le 4$. It immediately gives faithfulness of the Jones representation of $B_4$ (Corollary 1.1 of the paper), since the Jones representation contains the reduced Burau representation as a summand. Beyond the statement itself, the kernel and the image of $\rho_n$ for $n \ge 5$ remain poorly understood, and the paper's disk-sequence and parity technology is proposed by its authors as a tool for that problem.

For formalization, essentially nothing of this is machine-checked today: Mathlib has neither braid groups nor the Burau representation. This mission puts in place a checked definition of $\rho_n$ over $\mathbb{Z}[t,t^{-1}]$ (including well-definedness and invertibility), and then asks for the mathematics. Even the three-strand case — Magnus–Peluso, known since 1969 — is not formalized anywhere, and it is the natural first target.

Difficulty

The obvious approach fails in both directions. One cannot simply compute: a braid in the kernel would have to be found or excluded among infinitely many words, and no normal form for $B_4$ turns injectivity of $\rho_4$ into a finite check. Nor can one argue by a free-subgroup / ping-pong pattern, which is how non-faithfulness is proved for $n \ge 5$.

The source argument is topological. To a braid $\Phi$ one associates the arc $\beta = (\beta_*^3)\Phi$ and the sequence of punctured disks cut out by its intersections with a fixed arc $\alpha$; the Moody polynomial $M(\alpha,\beta) \in \mathbb{Z}[t,t^{-1}]$ then obstructs membership in the kernel provided no cancellation occurs among its monomials. Three-strand braids always satisfy the relevant parity condition; four-strand braids do not, and the paper repairs this by pushing a point-pushing braid $\Phi \in K_4$ into $B_5$ and applying Moody's theorem there. A complete formalization therefore needs curves on punctured disks, minimal position, and the Birman exact sequence — none of which exist in Mathlib. Contributions that build any of that infrastructure are as welcome as contributions to the statements themselves.

Formalization scope

Conventions fixed by the Lean development:

1. $B_n$ is the abstract group given by Artin's presentation, with generators indexed by $\mathrm{Fin}(n-1)$ using truncated subtraction; the generator of index $i$ is $\sigma_{i+1}$. This is the already-published definition reused by the mission, so results proved here interoperate with other braid-group missions.
2. The representation is the unreduced Burau representation, of size $n \times n$, not the reduced $(n-1)$-dimensional one; the variable is written $t$ and the coefficient ring is $\mathbb{Z}[t,t^{-1}]$.
3. Faithfulness is stated as injectivity of the group homomorphism, not as triviality of the kernel on some subgroup, and it is the genuine homomorphism out of the presented group: the braid relations are verified for the Burau matrices in the definition file, so no statement here is vacuous or conditional on well-definedness.
4. Long's criterion is stated for all $n$; for $n \le 2$ its noncentrality hypothesis cannot be satisfied, so its content is the case $n \ge 3$ that the paper uses.

A complete development will additionally need: point-pushing subgroups and the Brunnian group $\mathrm{Brun}_4$, the Moody polynomial of a pair of arcs, and winding-number sequences. These are not yet formalized and are deliberately not part of the current statements; proposals for faithful formalizations of them are welcome in the mission discussion.

Selected references

• V. Bharathram, J. S. Birman, T. E. Brendle, The Burau representation is faithful for n = 4, 2026, arXiv:2607.05283.
• W. Magnus, A. Peluso, On a theorem of V. I. Arnold, Comm. Pure Appl. Math. 22 (1969), 683–692, DOI:10.1002/cpa.3160220508.
• D. D. Long, A note on the normal subgroups of mapping class groups, Math. Proc. Cambridge Philos. Soc. 99 (1986), 79–87, DOI:10.1017/S0305004100063969.
• J. A. Moody, The Burau representation of the braid group $B_n$ is unfaithful for large $n$, Bull. Amer. Math. Soc. 25 (1991), 379–384, DOI:10.1090/S0273-0979-1991-16080-5.
• D. D. Long, M. Paton, The Burau representation is not faithful for $n \ge 6$, Topology 32 (1993), 439–447, DOI:10.1016/0040-9383(93)90030-Y.
• S. Bigelow, The Burau representation is not faithful for $n = 5$, Geom. Topol. 3 (1999), 397–404, DOI:10.2140/gt.1999.3.397.

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.

Motivation

In the last of the twenty-four questions that closed his 1982 survey Three-dimensional manifolds, Kleinian groups and hyperbolic geometry (Bull. Amer. Math. Soc. 6 (1982), 357–381), Thurston asked to "show that volumes of hyperbolic $3$-manifolds are not all rationally related" (p. 380). Twenty-two of the twenty-four have since been answered — geometrization by Perelman, tameness by Agol and by Calegari–Gabai, the ending lamination conjecture by Brock–Canary–Minsky, virtual fibering by Agol — and this one is among the two that remain open.

Some rational relations are forced, and for a trivial reason: a degree $n$ cover of a hyperbolic $3$-manifold has $n$ times its volume, so any two commensurable manifolds have rationally related volumes. The question, which remains open, is whether every rational relation arises that way — equivalently, whether some two hyperbolic $3$-manifolds have irrational volume ratio. Remarkably, not a single such pair is known.

Setting

The bundle fixes the meaning of every term. Hyperbolic $3$-space is the upper half-space $\{(x,y,z) : z > 0\}$. Its volume is Lebesgue measure with density $z^{-3}$ — the Riemannian volume of the metric $(dx^2+dy^2+dz^2)/z^2$ written out, so that no Riemannian machinery is required. The hyperbolic distance is given by its closed formula

$$\cosh d(p,q) \;=\; 1 + \frac{|p-q|^2}{2\,p_3\,q_3}.$$

A Kleinian action is a free, properly discontinuous action by hyperbolic isometries; the quotient is a complete hyperbolic $3$-manifold, discreteness and torsion freeness being consequences rather than hypotheses. The volume of the quotient is the measure of a fundamental domain, in the sense of Mathlib's MeasureTheory.IsFundamentalDomain, and the set of volumes collects those that are finite and positive.

Two conventions are stated rather than derived, and are worth flagging. Isometries are not required to preserve orientation, so the set of volumes also contains those of non-orientable quotients; this enlarges the set but not its $\mathbb{Q}$-span, so neither goal is affected. And preservation of the hyperbolic volume is a field of the structure rather than a consequence of preserving the distance: it holds for every hyperbolic isometry, but deriving it amounts to classifying $\mathrm{Isom}(\mathbb{H}^3)$, which is not the subject of this mission.

Formalization targets

The goal is that the volumes are not all rationally related: there are two of them, $v$ and $w$, with $v \neq q w$ for every rational $q$.

Two milestones support it. The first is that passing to a subgroup of index $n$ multiplies the volume by $n$, a fundamental domain for the subgroup being the union of $n$ translates of one for the whole group; this is the source of every known rational relation, and it is why the question is phrased as it is. The second is that the set of volumes is nonempty — that some finite-volume hyperbolic $3$-manifold exists at all — without which the goal would be vacuously false rather than open.

A stronger form of the question, that the $\mathbb{Q}$-span of the set of volumes is infinite dimensional, is also stated.

Significance

The question is a geometric statement whose difficulty is arithmetic. For the Bianchi groups of an imaginary quadratic field $F$, Humbert's formula gives the covolume as $|\delta_F|^{3/2}\zeta_F(2)/4\pi^2$, so the ratio of two such volumes is, up to explicit algebraic factors, a ratio of Dedekind zeta values at $2$; and Neumann and Yang showed that the Bloch invariant of a hyperbolic $3$-manifold lies in a subgroup of finite $\mathbb{Q}$-rank determined by its invariant trace field, so that manifolds sharing an invariant trace field with a single complex place, such as an imaginary quadratic one, have rationally related volumes. Producing one irrational ratio therefore means separating two such transcendentals — a statement of the same order of difficulty as the irrationality of $\zeta(5)$. The value of formalizing the question is not that it will be closed, but that its statement, and the elementary relations that make its naive form false, are pinned down exactly.

Motivation

The diffeomorphism group $\mathrm{Diff}(M)$ of a closed smooth manifold $M$, topologized so that two diffeomorphisms are close when they and all their derivatives are uniformly close, is a basic invariant of the smooth structure of $M$. Its set of path components $\pi_0\,\mathrm{Diff}(M)$ is the group of isotopy classes of diffeomorphisms (the smooth mapping class group), and its higher homotopy groups classify smooth fibre bundles with fibre $M$. For spheres, the natural comparison is with the orthogonal group $O(n+1)$ of isometries of the round metric, which sits inside $\mathrm{Diff}(S^n)$.

S. Smale asked how far $\mathrm{Diff}(S^n)$ is from $O(n+1)$. The question was settled positively in dimensions $n \le 3$ and has been studied extensively in dimensions $n \ge 5$, where surgery theory and pseudo-isotopy theory apply. Dimension $4$ is the remaining case, and it is where the least is known. The question is recorded on the Open Problem Garden (problem page) with importance "Outstanding".

Timeline.

• 1959 — S. Smale: $\mathrm{Diff}(S^2) \simeq O(3)$.
• 1963 — M. Kervaire and J. Milnor compute the groups $\Theta_n$ of homotopy spheres; combined with Cerf's pseudo-isotopy theorem this computes $\pi_0\,\mathrm{Diff}(S^n)$ for many $n \ge 5$ (for example $\pi_0\,\mathrm{Diff}^+(S^6) \cong \Theta_7 \cong \mathbb Z/28$).
• 1970s — the Cerf–Morlet comparison theorem $\mathrm{Diff}(D^n) \simeq \Omega^{n+1}(PL_n/O_n)$ (Kirby–Siebenmann, Foundational Essays).
• 1978 — F.T. Farrell and W.C. Hsiang compute $\pi_i\,\mathrm{Diff}(D^n)\otimes\mathbb Q$ in a stable range of degrees for large $n$.
• 1983 — A. Hatcher: $\mathrm{Diff}(S^3) \simeq O(4)$ (the Smale conjecture).
• 2007 — R. Budney: $\mathrm{Diff}(D^4)$ is a $5$-fold loop space, via little cubes acting on spaces of long knots.
• 2018 — T. Watanabe: $\pi_*\,\mathrm{Diff}(D^4)\otimes\mathbb Q \ne 0$; the $4$-dimensional Smale conjecture is false (arXiv:1812.02448).

Whether $\mathrm{Diff}(D^4)$ is connected is still unknown.

Setting

Write $\mathbb R^n$ for Euclidean space with the Euclidean norm, $D^n$ for the closed unit ball and $S^n \subset \mathbb R^{n+1}$ for the round unit sphere.

• $\mathrm{Diff}(D^n)$ is the group of diffeomorphisms of the $n$-ball rel boundary. Concretely it is the group of smooth diffeomorphisms $f\colon \mathbb R^n \to \mathbb R^n$ with $f(x) = x$ whenever $\|x\| \ge 1$. Two such maps are close when their $k$-th derivatives are uniformly close for every $k$ (the $C^\infty$ topology). The base point is the identity.
• $\mathrm{Diff}(S^n)$ is the group of all smooth diffeomorphisms of $S^n$ (orientation-preserving or orientation-reversing), with the $C^\infty$ topology. Derivatives are measured through the degree-one homogeneous extension $x \mapsto \|x\|\, f(x/\|x\|)$, taken on the sphere.
• $O(n)$ is the group of real orthogonal $n\times n$ matrices with the matrix topology.
• $X \simeq Y$ means that $X$ and $Y$ are homotopy equivalent. $\pi_0 X$ is the set of path components, and $\pi_i(X,x)$ is the $i$-th homotopy group. $\Omega^k(Y,y)$ is the $k$-fold loop space, the space of maps $[0,1]^k \to Y$ sending the boundary of the cube to $y$.

The source states that $\mathrm{Diff}(S^4) \simeq O(5) \times \mathrm{Diff}(D^4)$, so the homotopy type of $\mathrm{Diff}(S^4)$ is determined by that of $\mathrm{Diff}(D^4)$.

Formalization targets

Goal: connectivity of $\mathrm{Diff}(D^4)$

$$\pi_0\,\mathrm{Diff}(D^4) = 0, \qquad\text{i.e. } \mathrm{Diff}(D^4) \text{ is path-connected.}$$

The source asks to "determine some (any?) homotopy or homology groups of $\mathrm{Diff}(D^4)$" and singles out connectivity as unknown. The goal is the yes/no question for $\pi_0$. It can be settled either way: a proof shows that every diffeomorphism of $D^4$ rel boundary is isotopic to the identity, and a disproof exhibits one that is not.

Milestones

1. $\mathrm{Diff}(S^4) \simeq O(5)\times\mathrm{Diff}(D^4)$ (problem statement).
2. $\mathrm{Diff}(D^4) \simeq \Omega^5(Y,y)$ for some pointed space $(Y,y)$ (Cerf–Morlet, Budney).
3. $\mathrm{Diff}(D^4)$ is not contractible (Watanabe).
4. $\mathrm{Diff}(S^2) \simeq O(3)$ (Smale).
5. $\mathrm{Diff}(S^3) \simeq O(4)$ (Hatcher).
6. $|\pi_0\,\mathrm{Diff}(S^6)| = 56$ (Kervaire–Milnor and Cerf).
7. For $2 \le i < \min\{\tfrac{n-4}{3}, \tfrac{n-7}{2}\}$: $\pi_i\,\mathrm{Diff}(D^n)\otimes\mathbb Q \cong \mathbb Q$ if $n$ is odd and $4 \mid i+1$, and $0$ otherwise (Farrell–Hsiang).

Significance

The result itself. A positive answer would mean $\pi_0\,\mathrm{Diff}(S^4) \cong \mathbb Z/2$, detected by orientation alone, matching dimensions $1$, $2$ and $3$. A negative answer would give an exotic diffeomorphism of $S^4$: one that is topologically isotopic to the identity (by the Alexander trick) but not smoothly isotopic. By the Cerf–Morlet theorem, $\pi_0\,\mathrm{Diff}(D^4) \cong \pi_5(PL_4/O_4)$, so the question is equivalent to a question about the homotopy of $PL_4/O_4$, the space controlling smoothings of PL $4$-manifolds. The source lists the smooth $4$-dimensional Schoenflies problem as a related problem.

Formalizing it. No part of this theory is currently formalized in Lean or Mathlib: there is no $C^\infty$ topology on diffeomorphism groups and no known homotopy equivalence involving one. The milestones are classical theorems (Smale 1959, Hatcher 1983, Kervaire–Milnor 1963, Farrell–Hsiang 1978, Watanabe 2018). Formalizing any of them is new work, independent of the open goal.

Difficulty

In dimensions $\ge 5$, $\pi_0\,\mathrm{Diff}(D^n)$ is computed by combining Cerf's pseudo-isotopy theorem with the $h$-cobordism theorem. Both rely on the Whitney trick, which fails in dimension $4$. In dimension $4$ one also cannot reduce to a lower-dimensional problem as Smale and Hatcher did. The known invariants that detect non-trivial elements of $\pi_*\,\mathrm{Diff}(D^4)$ (Watanabe's configuration-space integrals) are rational and live in positive degrees, so they say nothing about $\pi_0$. Smale's and Hatcher's arguments for $n = 2, 3$ rely on understanding spaces of embedded spheres in $S^n$ of one lower dimension; the corresponding spaces of $3$-spheres in $S^4$ are not understood, so those arguments do not carry over.

Formalization scope

All statements import the single definition file SmaleDiffS4_Basic and live in the namespace SmaleDiffS4.

• DiffDisk n is the subtype of Mathlib's Diffeomorph 𝓘(ℝ, ℝⁿ) 𝓘(ℝ, ℝⁿ) ℝⁿ ℝⁿ ∞ (smooth = C^∞) of maps fixing every point of norm $\ge 1$. Its topology is induced by the family of iterated derivatives iteratedFDeriv ℝ k f, $k \in \mathbb N$, each with the topology of uniform convergence on $\mathbb R^n$. This "identity outside the open ball" model is the standard model of $\mathrm{Diff}(D^n \text{ rel } \partial)$ and is homotopy equivalent to the "identity on the boundary" and "identity near the boundary" variants.
• DiffSphere n is Mathlib's Diffeomorph (𝓡 n) (𝓡 n) (sphere 0 1) (sphere 0 1) ∞ on the unit sphere of $\mathbb R^{n+1}$. Its topology is induced by the iterated derivatives of the radial extension, restricted to the sphere and uniformly topologized.
• OrthGroup n is Matrix.orthogonalGroup (Fin n) ℝ with the subspace topology.
• Homotopy equivalence is ContinuousMap.HomotopyEquiv. $\Omega^5$ is GenLoop (Fin 5) Y y, $\pi_0$ is ZerothHomotopy, and $\pi_i$ is HomotopyGroup (Fin i). $\pi_i\otimes\mathbb Q$ is TensorProduct ℤ ℚ (Additive π_i), and "$\cong\mathbb Q$" is stated as $\mathbb Q$-rank $1$.
• The Farrell–Hsiang milestone covers only $i \ge 2$, where $\pi_i$ is abelian in Mathlib. It includes the parity hypothesis "$n$ odd" of the original theorem, which is lost in the source page's rendering.

A trivializing formalization is ruled out: the topology is the genuine $C^\infty$ topology rather than the discrete or indiscrete one, and the goal is not vacuous because DiffDisk 4 is nonempty (it contains the identity).

A complete development needs reusable infrastructure: the $C^\infty$ topology and topological-group structure on diffeomorphism groups, isotopy extension and fibration theorems (Cerf–Palais), restriction to a disc, and the Alexander trick. Contributions of this infrastructure as separate theorems are welcome.

Selected references

• Open Problem Garden, What is the homotopy type of the group of diffeomorphisms of the 4-sphere? (posted 2009). http://www.openproblemgarden.org/op/what_is_the_homotopy_type_of_the_group_of_diffeomorphisms_of_the_4_sphere
• S. Smale, Diffeomorphisms of the 2-sphere, Proc. Amer. Math. Soc. 10 (1959), 621–626. https://doi.org/10.1090/S0002-9939-1959-0112149-8
• M. Kervaire, J. Milnor, Groups of homotopy spheres I, Ann. of Math. 77 (1963), 504–537. https://doi.org/10.2307/1970128
• R. Kirby, L. Siebenmann, Foundational Essays on Topological Manifolds, Smoothings, and Triangulations, Princeton University Press, 1977.
• F.T. Farrell, W.C. Hsiang, On the rational homotopy groups of the diffeomorphism groups of discs, spheres and aspherical manifolds, Proc. Sympos. Pure Math. 32 (1978), 403–415.
• A. Hatcher, A proof of a Smale conjecture, $\mathrm{Diff}(S^3)\simeq O(4)$, Ann. of Math. (2) 117 (1983), 553–607. https://doi.org/10.2307/2007035
• R. Budney, Little cubes and long knots, Topology 46 (2007), 1–27. https://arxiv.org/abs/math/0309427
• T. Watanabe, Some exotic nontrivial elements of the rational homotopy groups of $\mathrm{Diff}(S^4)$, 2018. https://arxiv.org/abs/1812.02448

Motivation

Anosov flows are the model of uniformly hyperbolic, chaotic continuous-time dynamics: a nonsingular vector field $X$ on a closed manifold $M$ is Anosov when the tangent bundle splits as $TM=E^s\oplus\mathbb RX\oplus E^u$, with $E^s$ uniformly contracted and $E^u$ uniformly expanded by the derivative of the flow. They are structurally stable, so one can hope to classify them up to topological equivalence. In dimension three this classification is far from complete: it is not known which closed 3-manifolds carry Anosov flows, nor how many inequivalent Anosov flows a given manifold can carry.

The classical examples — suspensions of hyperbolic toral automorphisms and geodesic flows of hyperbolic surfaces — are rigid (Plante; Ghys). Non-algebraic examples were built by Franks–Williams (a nontransitive Anosov flow, 1980), Handel–Thurston, Goodman, Fried, Bonatti–Langevin, Fenley, Barbot and others. Several of these examples glue together neighbourhoods of hyperbolic sets along their boundaries. Béguin, Bonatti and Yu (Geom. Topol. 21 (2017)) turned this into a general theory, and used it to answer questions of Katok and of Barbot–Fenley.

Setting

A plug $(U,X)$ is a compact 3-manifold $U$ with boundary and a nonsingular C¹ vector field $X$ transverse to $\partial U$. The boundary splits into the entrance boundary $\partial^{in}U$ (where $X$ points inwards) and the exit boundary $\partial^{out}U$. The maximal invariant set $\Lambda$ consists of the points whose orbit stays in $U$ for all times. The plug is hyperbolic if $\Lambda$ is a hyperbolic set with one-dimensional strong stable and strong unstable bundles. The entrance lamination $L^s_X=W^s(\Lambda)\cap\partial^{in}U$ and the exit lamination $L^u_X=W^u(\Lambda)\cap\partial^{out}U$ are one-dimensional laminations of the boundary surfaces. The plug has filling MS laminations when every component of $\partial^{in}U\setminus L^s_X$ (and of $\partial^{out}U\setminus L^u_X$) is a strip: a disc whose accessible boundary consists of two leaves asymptotic to each other at both ends.

A diffeomorphism $\varphi:\partial^{out}U\to\partial^{in}U$ is a strongly transverse gluing map if $\varphi_*(L^u_X)$ and $L^s_X$ are transverse and cut $\partial^{in}U$ into squares with sides alternately on leaves of the two laminations. Gluing then gives a closed manifold $U/\varphi$ with an induced vector field $Z$. Two triples $(U,X,\varphi)$ and $(U,Y,\psi)$ are strongly isotopic if they are joined by a continuous path of such data.

Formalization targets

Goal: the gluing theorem (Theorem 1.5)

$$\begin{gathered}(U,X)\ \text{hyperbolic plug with filling MS laminations},\ \Lambda\ \text{without attractors or repellers},\ \varphi\ \text{strongly transverse}\\ \Longrightarrow\ \exists\,(Y,\psi)\ \text{strongly isotopic to}\ (X,\varphi)\ \text{with the field induced by } Y \text{ on } U/\psi\ \text{Anosov}.\end{gathered}$$

Milestones

• Proposition 1.1: gluing two hyperbolic plugs along transverse laminations gives a hyperbolic plug. Proposition 1.3: strongly transverse gluing preserves filling MS laminations.
• Lemma 3.27 (self-gluing case): the glued manifold $U/\varphi$ exists as a closed smooth manifold with an induced vector field.
• Proposition 1.6: if the graph of basic pieces is strongly connected, the Anosov flow of Theorem 1.5 is transitive.
• Theorem 1.8: every transitive Anosov flow on a closed 3-manifold is a factor of a transitive Anosov flow on another closed 3-manifold, restricted to a compact invariant set.
• Theorem 1.9: some closed orientable 3-manifold carries both a transitive and a nontransitive Anosov flow.
• Theorem 1.10 and Corollary 1.11: every MS foliation of a closed orientable surface is the entrance foliation of a transitive attracting hyperbolic plug; in particular incoherent transitive hyperbolic attractors exist.
• Theorem 1.12: every hyperbolic plug with filling MS laminations embeds, up to topological equivalence, in an Anosov flow on a closed orientable 3-manifold, which can be taken transitive when $\Lambda$ has no attractors or repellers.
• Theorem 1.13: for every $n\ge1$ some closed orientable 3-manifold carries $n$ pairwise inequivalent transitive Anosov flows.
• Theorem 1.15: some transitive Anosov flow admits infinitely many pairwise nonisotopic transverse tori.

Significance

Theorem 1.5 lets one build Anosov flows on closed 3-manifolds by gluing hyperbolic plugs. Proposition 1.6 gives a combinatorial criterion for the result to be transitive. Together they answer a question of Katok (Theorem 1.9) and questions of Barbot and Fenley on manifolds with several hyperbolic JSJ pieces supporting transitive Anosov flows (Theorem 1.13). They also show that transitive Anosov flows admit no fully canonical decomposition into finitely many transverse tori (Theorem 1.15). The results are proved in the source paper. None of them is formalized, and Mathlib has no theory of hyperbolic sets for flows, stable manifolds or laminations. A formal proof therefore needs a substantial amount of reusable smooth dynamics.

Difficulty

The glued vector field is generally not hyperbolic: perturbing the gluing map can create solid tori of parallel periodic orbits. The difficulty is to choose the gluing map (and the vector field within its topological equivalence class) so that cone fields on $\partial^{in}U$ are mapped into themselves by the return map. The return map is the composition of the crossing map of the plug with the gluing map. Contraction and expansion must therefore be controlled simultaneously along two transverse invariant foliations. The paper achieves this after reducing to plugs with an affine Markov partition. The naive approach — fixing $\varphi$ and trying to verify hyperbolicity — fails in general (Question 1.4 of the paper remains open).

Formalization scope

• Manifolds are modelled on the half-space EuclideanHalfSpace 3 with a $C^\infty$ structure; closed manifolds are compact, Hausdorff and BoundarylessManifold, and connected where the paper's statements concern a single manifold. Orientability is given by an atlas with positive Jacobians.
• Vector fields are C¹ sections; flows are encoded by integral curves, so that partial flows on manifolds with boundary make sense; flowMap X t x is $x$ when the orbit is undefined.
• Hyperbolicity is quantified over a continuous Riemannian metric, invariant line fields and constants $C,\lambda>0$; continuity of the splitting is not imposed (it is automatic).
• Filling MS laminations are encoded through the strip condition (Lemma 3.21); leaves of $L^s$ are path components of intersections of weak stable manifolds with $\partial^{in}U$.
• The glued manifold $U/\varphi$ is not a quotient type: statements quantify over every closed smooth 3-manifold $N$ with a surjective C¹ immersion $q:U\to N$ realising the identification. Lemma 3.27 (a milestone) guarantees such $N$ exists, so these statements are not vacuous. The induced field is not required to be C¹ and "Anosov" there means hyperbolicity of the whole manifold.
• Useful reusable infrastructure: flows of C¹ vector fields on compact manifolds (with boundary), stable manifold theory, the λ-lemma, laminations and foliations of surfaces, and gluing of manifolds along boundary components.

Selected references

• F. Béguin, C. Bonatti, B. Yu, Building Anosov flows on 3-manifolds, Geom. Topol. 21 (2017) 1837–1930. https://doi.org/10.2140/gt.2017.21.1837

Motivation

The Hodge conjecture predicts that on a non-singular complex projective variety $X$ every rational cohomology class of type $(p,p)$ is a rational linear combination of the classes of algebraic subvarieties of $X$. Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A $2n$-dimensional complex abelian variety $A$ is of Weil type for an imaginary quadratic field $K=\mathbb{Q}(\sqrt{-d})$ if $K$ embeds into $\mathrm{End}_{\mathbb{Q}}(A)$ in such a way that both eigenspaces of $\eta(\sqrt{-d})$ meet $H^{1,0}(A)$ in an $n$-dimensional subspace. Such an $A$ carries a distinguished two-dimensional space of rational $(n,n)$-classes, the Weil classes, which for a generic $A$ of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.

Timeline of the unconditional results on algebraicity of Weil classes:

• A. Weil (1977) constructed the classes and showed that the generic abelian variety of Weil type has a three-dimensional space of rational $(n,n)$-classes, spanned by $h^n$ and the two-dimensional Weil plane.
• C. Schoen (Compositio Math. 65 (1988) and its 1998 Addendum, Compositio Math. 114) proved algebraicity for fourfolds of Weil type with $K=\mathbb{Q}(\sqrt{-3})$ and arbitrary discriminant, for sixfolds with $K=\mathbb{Q}(\sqrt{-3})$ and trivial discriminant, and for fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; a second proof of the last case is in B. van Geemen's survey (1994).
• K. Koike (Canad. Math. Bull. 47 (2004)) proved algebraicity for sixfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$, which yields fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and arbitrary discriminant.
• E. Markman (JEMS 25 (2023)) proved algebraicity for fourfolds, arbitrary $K$, and discriminant $1$.
• E. Markman, arXiv:2502.03415, proves algebraicity for sixfolds of discriminant $-1$ and every imaginary quadratic $K$, and deduces the Hodge conjecture for all abelian fourfolds.

Setting

Fix $g$ and present a $g$-dimensional complex torus by its first homology: a complex structure $J$ on $H_1(A,\mathbb{R})=\mathbb{R}^{2g}$ with $J^2=-1$, the lattice being $\mathbb{Z}^{2g}\subset\mathbb{R}^{2g}$. A polarization is a rational alternating form $E$ on $H_1(A,\mathbb{Q})=\mathbb{Q}^{2g}$ satisfying the Riemann relations $E(Jx,Jy)=E(x,y)$ and $E(x,Jx)>0$ for $x\neq 0$. Cohomology is $H^k(A,\mathbb{C})=\wedge^k H^1(A,\mathbb{C})$, realized as the alternating $\mathbb{C}$-multilinear forms on $H_1(A,\mathbb{C})=\mathbb{C}^{2g}$; a class is rational if its values on rational vectors are rational, and it has type $(p,q)$ if it is multiplied by $z^p\bar z^{q}$ under the scaling action $v\mapsto (\mathrm{Re}\,z)v+(\mathrm{Im}\,z)Jv$ of $z\in\mathbb{C}$. A Hodge class of degree $2p$ is a rational class of type $(p,p)$.

Let $g=2n$ and $K=\mathbb{Q}(\sqrt{-d})$ with $d>0$. A polarized abelian $2n$-fold of Weil type is such an $(A,E)$ together with a rational endomorphism $M=\eta(\sqrt{-d})$ of $H_1(A,\mathbb{Q})$ with

$$M^2=-d,\qquad MJ=JM,\qquad E(Mx,My)=d\,E(x,y),$$

the last condition saying that $\eta(k)$ multiplies the polarization class by the norm $\mathrm{Nm}(k)$, and such that each of the two eigenspaces $W,\overline{W}\subset H_1(A,\mathbb{C})$ of $M$ meets the $i$-eigenspace of $J$ in an $n$-dimensional subspace. The Hodge–Weil classes are the rational classes in

$$\widehat{HW}\;=\;\big(\wedge^{2n}W\;\oplus\;\wedge^{2n}\overline{W}\big)\cap H^{2n}(A,\mathbb{Q}),$$

equivalently the rational degree-$2n$ classes that vanish on every tuple of vectors containing both a vector of $W$ and a vector of $\overline{W}$.

The form $H(x,y)=E(Mx,y)+\sqrt{-d}\,E(x,y)$ is $K$-valued and hermitian on $H_1(A,\mathbb{Q})$, viewed as a $K$-vector space through $\eta$. The determinant of its Gram matrix in a $K$-basis lies in $\mathbb{Q}^{\times}$, and its class in $\mathbb{Q}^{\times}/\mathrm{Nm}(K^{\times})$ is the discriminant $\det H$ of $(A,\eta,h)$. Discriminant $-1$ means that this determinant equals $-(a^2+dc^2)$ for some rationals $a,c$ not both zero.

Algebraicity is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety $X\subseteq\mathbb{P}^N$ by a projective realization: a smooth, $\mathbb{Z}^{2g}$-periodic immersion $u:\mathbb{R}^{2g}\to X$, surjective onto $X$ and injective modulo the lattice, whose differential intertwines $J$ with the complex structure of $\mathbb{P}^N$. A class $w\in H^{2p}(A,\mathbb{C})$ is algebraic when some de Rham class of $X$ whose periods over the $2p$-cycles swept out by rational vectors $\lambda_1,\dots,\lambda_{2p}$ equal $w(\lambda_1,\dots,\lambda_{2p})$ is a rational combination of cycle classes $\mathrm{cl}(Z)$ of irreducible subvarieties $Z\subseteq X$ of dimension $g-p$. Cycle classes, de Rham cohomology of a projective variety, $(p,q)$-types and Hodge classes are taken from the platform's HodgeConjecture bundle, which formalizes §1 of Deligne's Clay problem description.

Formalization targets

Goal — Theorem 1.5.1 of arXiv:2502.03415

$$\text{For every } d>0:\ \text{the Hodge–Weil classes of a polarized abelian sixfold of Weil type with CM by }\mathbb{Q}(\sqrt{-d})\text{ and discriminant }-1\text{ are algebraic.}$$

The statement fixes neither the field $K$ nor the sixfold: it quantifies over every $d>0$, every polarized abelian sixfold of Weil type of discriminant $-1$, and every projective realization of it.

Milestone — Weil's plane of Hodge–Weil classes (§1.1)

$$\widehat{HW}\ \text{is a two-dimensional }\mathbb{Q}\text{-space, and each of its elements has type }(n,n).$$

Milestone — Schoen's degeneration step (§1.6)

$$\text{Goal for all sixfolds of discriminant }-1\ \Longrightarrow\ \text{Hodge–Weil classes of every abelian fourfold of Weil type are algebraic,}$$

for every imaginary quadratic $K$ and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.

Milestone — Corollary 1.6.1

$$\text{The Hodge conjecture holds for abelian fourfolds.}$$

Milestone — Lefschetz $(1,1)$

Divisor classes: every Hodge class in $H^2$ of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.

Significance

Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold $H^{2,2}(A,\mathbb{Q})$ is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.

Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.

Difficulty

The naive attack — write down subvarieties whose classes span $\widehat{HW}$ — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while $H^{n,n}(A,\mathbb{Q})$ is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf $\mathcal{E}$ on $X\times\hat X$, for $X$ the Jacobian of a genus-$3$ curve, whose characteristic class $\kappa(\mathcal{E})$ remains of Hodge type along all deformations of $(X\times\hat X,\eta,h)$ as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.

Formalization scope

Conventions the Lean development commits to:

1. Complex tori are presented by $(J,E)$ on $\mathbb{R}^{2g}$ with the lattice $\mathbb{Z}^{2g}$; the polarization form is rational rather than integral, which is the isogeny-invariant form of the Riemann relations.
2. Cohomology is the space of alternating multilinear forms on $H_1(A,\mathbb{C})$, i.e. invariant forms on the torus; a period over a lattice cube is used to compare it with the de Rham cohomology of a projective realization.
3. The Weil condition is imposed symmetrically on both eigenspaces of $\eta(\sqrt{-d})$, so it does not depend on the choice of convention for $H^{1,0}$ versus $H^{0,1}$.
4. Discriminant $-1$ is stated as the existence of a $K$-basis in which the Gram determinant of $H$ is $-\mathrm{Nm}(k)$; changing the basis multiplies the determinant by a norm, so the condition is basis-independent.
5. Algebraicity always refers to cycle classes of subvarieties of an actual projective variety, in the sense of Deligne's formulation, never to an abstract subspace of "algebraic" classes; in particular the goal cannot be satisfied by exhibiting a formal object, and the hypotheses are satisfiable — abelian varieties of Weil type of discriminant $-1$ exist for every $K$, and abelian varieties admit projective realizations.

A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian $n$-fold, pure spinors and $K$-secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.

Selected references

• E. Markman, Cycles on abelian $2n$-folds of Weil type from secant sheaves on abelian $n$-folds, arXiv:2502.03415. https://arxiv.org/abs/2502.03415
• A. Weil, Abelian varieties and the Hodge ring, Collected Papers III, Springer 1980, 421–429.
• C. Schoen, Hodge classes on self-products of a variety with an automorphism, Compositio Math. 65 (1988), 3–32; Addendum, Compositio Math. 114 (1998), 329–336. https://eudml.org/doc/89880
• B. van Geemen, An introduction to the Hodge conjecture for abelian varieties, Lecture Notes in Math. 1594, Springer 1994, 233–252. https://doi.org/10.1007/BFb0094425
• K. Koike, Algebraicity of some Weil Hodge classes, Canad. Math. Bull. 47 (2004), 566–572. https://doi.org/10.4153/CMB-2004-055-3
• B. Moonen, Y. Zarhin, Hodge classes and Tate classes on simple abelian fourfolds, Duke Math. J. 77 (1995), 553–581. https://doi.org/10.1215/S0012-7094-95-07717-5
• B. Moonen, Y. Zarhin, Hodge classes on abelian varieties of low dimension, Math. Ann. 315 (1999), 711–733. https://doi.org/10.1007/s002080050333
• J. Ramón Marí, On the Hodge conjecture for products of certain surfaces, Collect. Math. 59 (2008), 1–26. https://doi.org/10.1007/BF03191179
• E. Markman, The monodromy of generalized Kummer varieties and algebraic cycles on their intermediate Jacobians, J. Eur. Math. Soc. 25 (2023), 231–321. https://doi.org/10.4171/JEMS/1199
• P. Deligne, The Hodge conjecture, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/hodge.pdf

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

$$\exists\, f \text{ computable},\quad \forall K,\ |K| \text{ is an integral homology 3-sphere} \implies \bigl(f(K) = \mathtt{true} \iff |K| \text{ bounds a smooth integral homology 4-ball}\bigr).$$

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

$$P = \Sigma(2,3,5) \text{ is an integral homology 3-sphere}, \qquad P \text{ does not bound a smooth } \mathbb Z\text{-homology ball (Rokhlin)},$$ $$P \# (-P) \text{ bounds a smooth } \mathbb Z\text{-homology ball},$$ $$\Sigma(2,5,7),\ \Sigma(3,4,5),\ \Sigma(2,3,13) \text{ bound contractible 4-manifolds (Akbulut–Kirby)},$$ $$\Sigma(p, ps-1, ps+1)\ (p \text{ even}, s \text{ odd}),\ \Sigma(p, ps\pm1, ps\pm2)\ (p \text{ odd}) \text{ bound contractible 4-manifolds (Casson–Harer)},$$ $$L(m^2, mk-1)\ (0<k<m,\ \gcd(m,k)=1) \text{ bounds a smooth } \mathbb Q\text{-homology ball (Casson–Harer)},$$ $$\Sigma(2,3,7) \text{ bounds a smooth } \mathbb Q\text{-homology ball (Fintushel–Stern)}.$$

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

$$\forall\,\gamma,\quad \mathrm{IsKnot}(\gamma)\ \wedge\ \mathrm{IsSlice}(\gamma)\ \Longrightarrow\ \mathrm{IsRibbon}(\gamma).$$

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