Geometry & Topology

Algebraic Topology·Captain: ryanshin

Smooth 4-dimensional Poincaré conjecture: foundations and reductionsOpen Problem

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.

60 thms5 active usersReviewed

Completed

Differential Geometry·Captain: Lucas

Differential Geometry of Curves and Surfaces III: Global Properties of Plane CurvesTextbook

Motivation

The local theory of curves describes what happens near one point; the global theory asks what a curve must satisfy because it closes up. Two classical statements make the difference visible. The isoperimetric inequality says that among all simple closed plane curves of a given length, the circle encloses the largest area — a question already settled in intent by the Greeks, but given a satisfactory proof only in the nineteenth century, and the short proof reproduced by do Carmo is E. Schmidt's from 1939. The four-vertex theorem says that the curvature of a simple closed convex curve has at least four critical points, so no convex oval has the curvature profile of a curve that just rises and falls once.

The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §1-7, "Global Properties of Plane Curves" (pp. 31–46): the area formula, equation (1) on p. 33; the isoperimetric inequality, Theorem 1 on p. 34; the theorem of turning tangents on p. 37; the lemma, equation (5) on p. 38; and the four-vertex theorem, Theorem 2 on p. 37.

This is the third mission of a series formalizing do Carmo's book, and shares the namespace DoCarmoDG with the earlier ones.

Setting

A closed plane curve of length $l$ is a regular map $\alpha : [0,l] \to \mathbb{R}^2$ whose derivatives of all orders agree at the two endpoints; equivalently, and as used here, a smooth $l$ -periodic map $\alpha : \mathbb{R} \to \mathbb{R}^2$ . It is parametrized by arc length when $|\alpha'(s)| = 1$ for all $s$ , in which case $l$ is its length. It is simple when it has no self-intersection: $\alpha(t_1) \neq \alpha(t_2)$ for distinct $t_1, t_2 \in [0,l)$ .

Write $J$ for rotation by $+\pi/2$ , $J(a,b) = (-b,a)$ . For a curve parametrized by arc length the signed curvature is

k(s) = \bigl\langle \alpha''(s),\, J\alpha'(s) \bigr\rangle,

which is do Carmo's convention of §1-5, Remark 1: the normal is chosen so that $\{\alpha', J\alpha'\}$ has the orientation of the natural basis, and then $\alpha'' = k\,J\alpha'$ . A vertex is a parameter $t$ with $k'(t) = 0$ . The curve is convex when, for every parameter $t$ , the whole trace lies in one of the two closed half-planes bounded by the tangent line at $t$ .

An angle function for $\alpha$ is a smooth $\theta$ with $\alpha'(s) = (\cos\theta(s), \sin\theta(s))$ ; the rotation index is $(\theta(l) - \theta(0))/2\pi$ . The area bounded by a positively oriented simple closed curve is given by do Carmo's equation (1),

A = \frac{1}{2}\int_0^l \bigl(x\,y' - y\,x'\bigr)\,dt, \qquad \alpha = (x,y).

Formalization targets

Goal — Four-vertex theorem (do Carmo, Theorem 2, p. 37)

\alpha \ \text{simple closed convex} \quad \Longrightarrow \quad \#\{\,t \in [0,l) : k'(t) = 0\,\} \ge 4 .

Supporting statements

The three equivalent forms of the area formula (1); the existence of a smooth angle function; the identity $k = \theta'$ ; the theorem of turning tangents (the rotation index of a simple closed curve is $\pm 1$ ); the isoperimetric inequality $l^2 \ge 4\pi A$ with equality exactly for circles; and do Carmo's lemma (5), $\int_0^l (Ax + By + C)\,k'(s)\,ds = 0$ , which drives the proof of the goal.

Significance

The isoperimetric inequality is the ancestor of a large family of geometric inequalities, and its sharp case characterizes the circle — the first instance of the pattern "extremal configuration is the round one" that recurs throughout geometry. The four-vertex theorem is a genuinely global statement with no local counterpart: locally, the curvature of a convex arc may be strictly monotone, and it is only the requirement that the curve close up convexly that forces four critical points. Its converse, for strictly positive curvature, was proved by H. Gluck in 1971; do Carmo notes that the theorem also holds for simple closed curves that are not convex, by a harder argument.

Mathlib contains integration, the winding number of a loop in the complex plane and the Jordan curve theorem, but it does not contain the signed curvature of a plane curve, the theorem of turning tangents in this form, the isoperimetric inequality for curves with its equality case, or the four-vertex theorem. What this mission adds is that vocabulary and machine-checked proofs of the four classical statements.

Difficulty

Each target fails for a different reason under the naive approach.

For the area formula, the identification of $\frac12\oint(x\,dy - y\,dx)$ with the area of the interior is exactly the Jordan-curve input that do Carmo declares he is assuming; the formalization avoids that dependency by defining the bounded area through the integral, so a solver has to prove only the integration-by-parts identities among the three forms of (1).

For the theorem of turning tangents, the difficulty is that a smooth lift $\theta$ of the tangent indicatrix must be produced and then shown to increase by exactly $\pm 2\pi$ over one period — a degree-theoretic statement about a loop in the circle, where simplicity of the curve is what excludes the values $0, \pm 2, \pm 3, \dots$ .

For the isoperimetric inequality, Schmidt's proof compares the curve with a circle tangent to two parallel supporting lines and uses the arithmetic–geometric mean inequality; the equality discussion, which is where the characterization of the circle lives, is the delicate part.

For the four-vertex theorem, the obvious argument — "curvature on a compact interval attains a maximum and a minimum, so there are two vertices" — gives only two, and the whole content is the step from two to four. The lemma (5) supplies the contradiction: if $k'$ changed sign only at the maximum and the minimum, a suitable line $Ax + By + C = 0$ through those two points would make the integrand of (5) of one sign and not identically zero.

Formalization scope

Curves are smooth maps ℝ → EuclideanSpace ℝ (Fin 2), closedness being $l$ -periodicity with $l > 0$ , which is do Carmo's condition that the curve and all its derivatives agree at the endpoints. Unit speed is imposed globally, so the parameter is arc length and $l$ is the length. Simplicity is injectivity on the half-open period $[0,l)$ . Convexity is stated per parameter: for each $t$ the trace lies in one closed half-plane of the tangent line at $t$ , the choice of side being allowed to depend on $t$ , as in the book's phrasing.

The area is defined by do Carmo's integral (1) rather than as the measure of the interior of the curve, so no Jordan curve theorem is presupposed; consequently the isoperimetric statement is formulated with the absolute value $|A|$ , which makes it independent of the curve's orientation and equal to the enclosed area for a positively oriented simple curve. The equality case asserts that the trace lies on a circle of positive radius.

"At least four vertices" is formalized as the existence of four pairwise distinct parameters in $[0,l)$ at which $k'$ vanishes, which rules out the degenerate reading in which one vertex is counted several times.

Selected references

Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition, Dover, 2016, §1-7 (area formula, eq. (1), p. 33; isoperimetric inequality, Theorem 1, p. 34; theorem of turning tangents, p. 37; lemma, eq. (5), p. 38; four-vertex theorem, Theorem 2, p. 37).
E. Schmidt, Über das isoperimetrische Problem im Raum von n Dimensionen, Mathematische Zeitschrift 44 (1939), 689–788.
H. Gluck, The converse to the four-vertex theorem, L'Enseignement Mathématique 17 (1971), 295–309.

8 thms4 active usersReviewed

Completed

Group Theory·Captain: marwahaha

A torsion-free hyperbolic group that is not residually finiteOpen Problem

Motivation

Residual finiteness means that finite quotients can distinguish every nonidentity group element. The source asks whether coarse negative curvature forces this separation property even without torsion. The source is OpenAI's September 2026 manuscript.

Setting

A torsion-free group has no nonidentity element whose positive power is the identity. A word-hyperbolic group admits a finite generating set whose Cayley graph has geodesic triangles of uniformly bounded thickness.

Formalization targets

\exists G:\quad G\text{ torsion-free and word-hyperbolic},\qquad\neg\operatorname{ResiduallyFinite}(G).

The theorem states, without a verified proof (it is admitted), that there exists a group G, in the lowest universe Type, that is torsion-free, word-hyperbolic, and not residually finite. Torsion-free means that for every g in G and every positive integer n, g^n = 1 implies g = 1, so no nonidentity element has finite order (this does not assert unique roots). Word-hyperbolic means that there is a finite subset S of G whose unit-edge Cayley graph (the simple graph with the multiplicative Cayley adjacency determined by S) is connected, which says that S generates G, and a natural number δ such that geodesic triangles are uniformly δ-thin. Precisely, for all vertices x, y, z and walks p from x to y, q from y to z and r from z to x, each of which is a geodesic (its length equals the graph distance between its endpoints), every vertex of each side lies within graph distance δ of some vertex on one of the other two sides. The statement also requires that G fail the Mathlib property Group.ResiduallyFinite.

The goal is OAI.Release075.main.

Significance

The goal puts a geometric condition and failure of finite-quotient separation into one existential statement. Torsion-freeness is retained explicitly. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Hyperbolicity concerns large-scale word geometry, whereas residual finiteness quantifies over every finite quotient. Checking a finite list of quotients cannot establish the required failure.

Formalization scope

Hyperbolicity is encoded by vertexwise thin triangles in a connected unit-edge Cayley graph for some finite generating set. Torsion-freeness is the positive-power condition and does not mean a unique-roots property. Residual finiteness uses the Mathlib definition.

The shared definitions are supplied by TorsionFreeHyperbolic. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, A torsion-free hyperbolic group that is not residually finite, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

39 thms3 active usersReviewed

Completed

Differential Geometry·Captain: Lucas

Differential Geometry of Curves and Surfaces IV: Regular Surfaces and Change of ParametersTextbook

Motivation

Before any geometry of surfaces can be done, one has to say what a surface is, in a way that supports calculus: a subset of $\mathbb{R}^3$ that is locally the smooth, non-degenerate image of an open piece of the plane. Every statement in the later theory — the first and second fundamental forms, the Gauss map, curvature, geodesics — is written in local coordinates, and is therefore meaningful only once one knows that the answer does not depend on the coordinates chosen. That independence is the content of the change-of-parameters theorem, which is what makes "differentiable function on a surface" and "geometric quantity of a surface" well-defined notions.

The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §2-2 "Regular Surfaces; Inverse Images of Regular Values" (pp. 54–71) and §2-3 "Change of Parameters; Differentiable Functions on Surfaces" (pp. 72–85): Definition 1 (p. 54), Propositions 1–4 of §2-2 (pp. 59, 61, 63, 65) and Proposition 1 of §2-3 (p. 74).

This is the fourth mission of a series formalizing do Carmo's book, sharing the namespace DoCarmoDG with the others.

Setting

A subset $S \subseteq \mathbb{R}^3$ is a regular surface when every $p \in S$ has an open neighbourhood $V \subseteq \mathbb{R}^3$ such that $V \cap S$ is the image of a map $x : U \to \mathbb{R}^3$ , defined on an open set $U \subseteq \mathbb{R}^2$ , satisfying the three conditions of do Carmo's Definition 1:

$x$ is differentiable, i.e. of class $C^\infty$ on $U$ ;
$x$ is a homeomorphism of $U$ onto $V \cap S$ — it is injective and its inverse is continuous;
(regularity) for every $q \in U$ the differential $dx_q : \mathbb{R}^2 \to \mathbb{R}^3$ is injective.

Such an $x$ is a parametrization, or system of local coordinates, and $V \cap S$ is a coordinate neighbourhood.

Given a differentiable $f$ on an open set $U \subseteq \mathbb{R}^3$ , a value $a$ is a regular value of $f$ when $df_p$ is surjective — equivalently, nonzero — at every $p \in U$ with $f(p) = a$ (do Carmo Definition 2, §2-2).

Formalization targets

Goal — Change of parameters (do Carmo §2-3, Proposition 1)

If $x : U \to S$ and $y : V \to S$ are two parametrizations of a regular surface $S$ with $p \in x(U) \cap y(V) = W$ , then

h = x^{-1} \circ y : y^{-1}(W) \to x^{-1}(W)

is a diffeomorphism: $h$ is differentiable, bijective, and $h^{-1}$ is differentiable.

Supporting statements

The graph of a differentiable function of two variables is a regular surface (Proposition 1); the inverse image of a regular value is a regular surface (Proposition 2); a regular surface is locally the graph of a differentiable function of one of the three coordinate pairs (Proposition 3); and an injective map satisfying conditions 1 and 3 whose image lies in a regular surface automatically has a continuous inverse (Proposition 4).

Significance

Proposition 2 is the practical criterion: it is what shows in one line that spheres, ellipsoids, tori and the level sets of generic polynomials are regular surfaces, and it is applied throughout the book. Proposition 3 is the structural statement that a regular surface is locally a graph, which is the form in which most local computations are carried out; Proposition 4 removes the awkward homeomorphism clause from the verification of examples. The change-of-parameters theorem is what allows every subsequent definition — differentiable function on a surface, tangent plane, first fundamental form, curvature — to be given in coordinates and then shown to be independent of them, and it is also the reason a regular surface carries a smooth structure at all.

Mathlib has smooth manifolds, the implicit and inverse function theorems, and ContDiffOn, but it does not contain do Carmo's concrete definition of a regular surface as a subset of $\mathbb{R}^3$ or these four propositions about it. Establishing them is what allows the rest of this series to work with patches while knowing that the objects so defined are coordinate-independent.

Difficulty

Everything here rests on the inverse function theorem, but each proposition needs it in a slightly different form. Proposition 2 requires completing $f$ to a local diffeomorphism $F(x,y,z) = (x,y,f(x,y,z))$ and reading off the level set — with the complication that which partial derivative is nonzero varies from point to point, so the coordinate that is solved for is not fixed in advance. Proposition 3 needs the same case distinction on which $2 \times 2$ Jacobian minor of $x$ is nonzero, and this is exactly why the conclusion is a disjunction over the three coordinate pairs. Proposition 4 is where the homeomorphism condition is shown to be redundant, and the argument goes through the local factorization $x^{-1} = (\pi \circ x)^{-1} \circ \pi$ .

The change-of-parameters theorem is not a direct application of the inverse function theorem to $h$ : the map $h$ is defined only on a subset of the plane and $x^{-1}$ is, a priori, merely continuous. One first extends $x$ to a local diffeomorphism of a neighbourhood in $\mathbb{R}^3$ and then composes; the continuity of $x^{-1}$ (condition 2 of Definition 1) is what makes the domain of $h$ open, and it cannot be dispensed with.

Formalization scope

A surface is a set S : Set (EuclideanSpace ℝ (Fin 3)), and a parametrization is a map x : ℝ × ℝ → EuclideanSpace ℝ (Fin 3) together with an open U : Set (ℝ × ℝ). Smoothness is ContDiffOn ℝ (⊤ : ℕ∞), matching do Carmo's "differentiable" for $C^\infty$ ; regularity is injectivity of the Fréchet derivative at each point of U, which is do Carmo's condition 3; and the homeomorphism condition is stated as injectivity on U together with the existence of a continuous left inverse on the image, which is the content of "the inverse is continuous". The neighbourhood clause of Definition 1 is x '' U = V ∩ S for an open V containing the point.

Graphs are formalized as three separate sets, one for each of $z = f(x,y)$ , $y = g(x,z)$ and $x = h(y,z)$ , so that Proposition 3 can state its disjunction faithfully; in that statement the neighbourhood is an open set W of $\mathbb{R}^3$ and the claim is W ∩ S = W ∩ graph.

The goal states the diffeomorphism property of $h$ explicitly — two maps, mutually inverse on the relevant domains, both ContDiffOn, together with the openness of those domains — rather than through a bundled structure, so that no library convention is assumed. There is no trivializing reading: the domains are those forced by the two parametrizations, and in the degenerate case where the images do not overlap the statement reduces to a true but empty claim about the empty set, while the substance is in the overlapping case.

Selected references

Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition, Dover, 2016, §2-2 (Definition 1, p. 54; Propositions 1-4, pp. 59-65) and §2-3 (Proposition 1, p. 74).

6 thms3 active usersReviewed

Completed

Differential Geometry·Captain: Lucas

Differential Geometry of Curves and Surfaces II: Theorema EgregiumTextbook

Motivation

Until 1827 the curvature of a surface in space was understood as a statement about how the surface sits inside $\mathbb{R}^3$ : it was computed from the way the unit normal turns, that is, from the second fundamental form. Gauss's Disquisitiones generales circa superficies curvas showed that one particular combination of those extrinsic quantities — the product of the principal curvatures — can be recomputed from measurements made entirely inside the surface, using only lengths of curves drawn on it. This is the Theorema Egregium, and it is the reason the subject splits into extrinsic and intrinsic geometry; the latter is what becomes Riemannian geometry.

The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), §4-3, "The Gauss Theorem and the Equations of Compatibility" (pp. 235–240). The theorem is stated on page 237 and derived from the Gauss formula, equation (5) of that section; the Mainardi–Codazzi equations (6) and (6a) on page 238 complete the list of compatibility equations.

This is the second mission of a series formalizing do Carmo's book; it shares the namespace DoCarmoDG with the first, on the local theory of curves.

Setting

A regular parametrized patch is a map $x : U \to \mathbb{R}^3$ , defined and smooth on an open set $U \subseteq \mathbb{R}^2$ with coordinates $(u,v)$ , whose partial derivatives satisfy $x_u \wedge x_v \neq 0$ at every point of $U$ ; the last condition says that $dx$ is injective, so $\{x_u, x_v\}$ spans a $2$ -dimensional tangent plane at each point and

N = \frac{x_u \wedge x_v}{|x_u \wedge x_v|}

is a unit normal field along the patch.

The first fundamental form is the restriction of the ambient inner product to the tangent plane; in the parametrization it is recorded by the three functions

E = \langle x_u, x_u\rangle, \qquad F = \langle x_u, x_v\rangle, \qquad G = \langle x_v, x_v\rangle,

and $EG - F^2 = |x_u \wedge x_v|^2 > 0$ . The second fundamental form is recorded by

e = \langle N, x_{uu}\rangle, \qquad f = \langle N, x_{uv}\rangle, \qquad g = \langle N, x_{vv}\rangle,

and the Gaussian curvature is

K = \frac{eg - f^2}{EG - F^2}.

The three second derivatives $x_{uu}, x_{uv}, x_{vv}$ decompose in the basis $\{x_u, x_v, N\}$ ; the tangential coefficients are the Christoffel symbols $\Gamma^k_{ij}$ of the patch, and the normal coefficients are $e$ , $f$ , $g$ , which is do Carmo's system (1) of §4-3:

x_{uu} = \Gamma^1_{11} x_u + \Gamma^2_{11} x_v + eN, \qquad x_{uv} = \Gamma^1_{12} x_u + \Gamma^2_{12} x_v + fN, \qquad x_{vv} = \Gamma^1_{22} x_u + \Gamma^2_{22} x_v + gN.

Two patches over the same parameter domain are isometric when their first fundamental forms coincide, $E = \bar E$ , $F = \bar F$ , $G = \bar G$ at every point: lengths of curves, angles and areas computed in the parameter domain then agree, and a local isometry between the two surfaces is obtained by matching parameters.

Formalization targets

Goal — Theorema Egregium (do Carmo, p. 237)

E = \bar E,\ F = \bar F,\ G = \bar G \ \text{ on } U \quad \Longrightarrow \quad K = \bar K \ \text{ on } U .

The Gaussian curvature of a regular patch is determined by its first fundamental form alone, although its definition uses the second fundamental form, i.e. the position of the surface in space.

Supporting statements

The existence and uniqueness of the Christoffel symbols; the linear system (2) expressing them through $E, F, G$ and their first derivatives; the Gauss formula (5),

(\Gamma^2_{12})_u - (\Gamma^2_{11})_v + \Gamma^1_{12}\Gamma^2_{11} + \Gamma^2_{12}\Gamma^2_{12} - \Gamma^2_{11}\Gamma^2_{22} - \Gamma^1_{11}\Gamma^2_{12} = -EK;

the Mainardi–Codazzi equations (6) and (6a); the closed formula for $K$ in an orthogonal parametrization (Exercise 1, p. 240); the invariance of $K$ under a change of parameters; and, as a corollary, that no neighbourhood of a point of the unit sphere is isometric to a piece of a plane (Exercise 4, p. 240).

Significance

The theorem is what makes intrinsic geometry possible: a quantity defined through the embedding turns out to be computable from the metric, so it survives every isometric deformation. Concrete consequences include the impossibility of a distortion-free map of the sphere — the reason every cartographic projection distorts lengths — and the equality of the Gaussian curvatures of the catenoid and the helicoid at corresponding points, which do Carmo notes immediately after the theorem. In the structure of the book, the Gauss formula is also the identity that makes the global Gauss–Bonnet theorem of §4-5 a statement about intrinsic data.

Mathlib has inner product spaces, iterated derivatives and the smooth manifold library, but it does not contain the first and second fundamental forms of a parametrized surface, the Christoffel symbols of a patch, the Gaussian curvature in this sense, or the compatibility equations. This mission produces that vocabulary together with machine-checked proofs of the classical identities. The mathematics is Gauss's, from 1827; what is open is the formalization.

Difficulty

The proof is a computation, but not a short one: one differentiates the system (1), uses $x_{uuv} = x_{uvu}$ , re-expands every second derivative through (1) again, and equates coefficients in the basis $\{x_u, x_v, N\}$ . Formally, the cost sits in three places: justifying the interchange of the mixed partial derivatives; establishing that the coefficient functions $\Gamma^k_{ij}$ obtained pointwise from linear algebra are differentiable in the parameters; and carrying out the coefficient comparison in a basis that is not orthonormal, where one must use that $EG - F^2 \neq 0$ rather than take inner products with an orthonormal frame.

The naive route to the Theorema Egregium — "solve the system (2) for the $\Gamma^k_{ij}$ , then quote the Gauss formula" — is the right one, but the first step must actually be carried out: the system (2) determines the symbols only because each of its three $2 \times 2$ blocks has determinant $EG - F^2 \neq 0$ , and that is where the regularity hypothesis is used.

Formalization scope

A patch is a curried map x : ℝ → ℝ → EuclideanSpace ℝ (Fin 3), so that the partial derivatives $x_u$ and $x_v$ are ordinary one-variable derivatives, and the domain is an open set U : Set (ℝ × ℝ); smoothness is ContDiffOn ℝ (⊤ : ℕ∞) of the uncurried map on U, matching do Carmo's use of "differentiable" for $C^\infty$ . Regularity is stated as $x_u \wedge x_v \neq 0$ on U, with the vector product defined componentwise. All quantities ( $N$ , $E$ , $F$ , $G$ , $e$ , $f$ , $g$ , $K$ ) are total functions of the parameters, taking junk values off U; every statement restricts to points of U.

Christoffel symbols are not defined by a formula: a statement that mentions them quantifies over functions $\Gamma^k_{ij}$ assumed to satisfy do Carmo's decomposition (1) on U, and a separate milestone asserts that such functions exist and are unique on U. The symmetry $\Gamma^k_{12} = \Gamma^k_{21}$ is built into the notation, as in the book.

Isometry is formalized as equality of $E$ , $F$ , $G$ over a common parameter domain rather than as a map between surfaces; together with the milestone on invariance under change of parameters, this recovers do Carmo's statement that $K$ is invariant under local isometries. The formalization deliberately keeps the surface concrete (a patch, not an abstract manifold), which is what makes the compatibility equations expressible as identities between explicit derivatives.

This mission's definition file builds on the vector-product definition introduced in mission I of this series (Fundamental Theorem of the Local Theory of Curves), so mission I must be submitted first: its definitions have to be published before the definition file of this mission can compile.

There is no vacuous reading: the hypotheses are satisfiable — every regular patch, for instance a graph or a surface of revolution, satisfies them — and the conclusion compares two curvature functions pointwise.

Selected references

Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition, Dover, 2016, §2-5, §3-3 and §4-3 (Theorema Egregium on p. 237; Gauss formula, eq. (5); Mainardi–Codazzi, eqs. (6), (6a)).
C. F. Gauss, Disquisitiones generales circa superficies curvas, Commentationes Societatis Regiae Scientiarum Gottingensis Recentiores 6 (1827), 99–146.

10 thms3 active usersReviewed

Completed

Differential Geometry·Captain: Lucas

Differential Geometry of Curves and Surfaces I: Fundamental Theorem of the Local Theory of CurvesTextbook

Motivation

The differential geometry of curves in $\mathbb{R}^3$ is the entry point of every course and every textbook in the subject, and it is the first place where a geometric object is shown to be completely determined by a small list of numerical invariants. A space curve traced out by a particle moving at unit speed bends (curvature) and twists (torsion); the assertion that these two scalar functions determine the curve completely, up to a motion of space, is the prototype of every later "fundamental theorem" of the subject — for surfaces (Bonnet), for Riemannian metrics, and for submanifolds in general.

The reference for this mission is Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition (Dover, 2016), Chapter 1, Sections 1-4 and 1-5. The statement targeted here is the one printed on page 19 under the heading Fundamental Theorem of the Local Theory of Curves; the uniqueness half is proved on pages 20–22, and the existence half is deferred by do Carmo to the appendix of Chapter 4, where it is obtained from the existence and uniqueness theorem for linear systems of ordinary differential equations.

This is the first mission of a series formalizing do Carmo's book. The series shares one Lean namespace, DoCarmoDG, so that later missions on regular surfaces, the Gauss map, and Gauss–Bonnet build on the vocabulary fixed here.

Setting

Let $I = (a,b) \subseteq \mathbb{R}$ be an open interval and let $\alpha : I \to \mathbb{R}^3$ be a smooth map. The curve $\alpha$ is parametrized by arc length if $|\alpha'(s)| = 1$ for every $s \in I$ ; the parameter $s$ is then the arc length measured along the curve.

For such a curve one sets

t(s) = \alpha'(s), \qquad k(s) = |\alpha''(s)| .

The vector $t(s)$ is the unit tangent and the scalar $k(s) \ge 0$ is the curvature at $s$ . Differentiating $\alpha'\cdot\alpha' = 1$ gives $\alpha''\cdot\alpha' = 0$ , so $\alpha''(s)$ is orthogonal to $t(s)$ . At a point where $k(s) \neq 0$ one defines the normal vector and the binormal vector

n(s) = \frac{\alpha''(s)}{k(s)}, \qquad b(s) = t(s) \wedge n(s),

where $\wedge$ is the vector product of $\mathbb{R}^3$ (do Carmo §1-4). The triple $\{t(s), n(s), b(s)\}$ is a positively oriented orthonormal basis, the Frenet trihedron. Since $b$ has constant length and $b' = t \wedge n'$ is orthogonal to $t$ , the derivative $b'(s)$ is a multiple of $n(s)$ , and the torsion $\tau(s)$ is defined by

b'(s) = \tau(s)\, n(s).

This is do Carmo's sign convention; many authors write $-\tau$ for the same quantity, and the mission is committed to do Carmo's. With these conventions the Frenet formulas read

t' = k\,n, \qquad n' = -k\,t - \tau\, b, \qquad b' = \tau\, n .

A rigid motion of $\mathbb{R}^3$ is a map $p \mapsto \rho(p) + c$ where $\rho$ is an orthogonal linear map with positive determinant and $c \in \mathbb{R}^3$ (do Carmo §1-5, Exercise 6).

Formalization targets

Goal — Fundamental theorem of the local theory of curves (do Carmo, p. 19)

Given smooth functions $k, \tau : (a,b) \to \mathbb{R}$ with $k(s) > 0$ :

\exists\, \alpha : (a,b) \to \mathbb{R}^3 \ \text{parametrized by arc length with curvature } k \text{ and torsion } \tau,

\text{and any two such curves } \alpha, \bar\alpha \text{ satisfy } \bar\alpha = \rho \circ \alpha + c \text{ for an orthogonal } \rho \text{ with } \det \rho > 0 .

The two halves are also stated separately as milestones, since they are proved by entirely different means: uniqueness by a Gronwall-free energy argument on the Frenet trihedron, existence by solving a linear ODE system.

Supporting statements

The orthonormality of the Frenet trihedron, the Frenet formulas themselves, the characterization of straight lines by $k \equiv 0$ and of plane curves by $\tau \equiv 0$ , the closed formula $\tau = -\,(\alpha' \wedge \alpha'')\cdot\alpha''' / k^2$ , and the invariance of arc length, curvature and torsion under rigid motions.

Significance

The theorem is the model case of a classification result: a geometric object modulo a symmetry group is faithfully encoded by a complete set of local invariants. Downstream it is what licenses the standard practice of "prescribing curvature and torsion" — constructing curves with specified geometric behaviour, computing with the Frenet apparatus rather than with the curve itself, and recognizing that any identity among $k$ , $\tau$ and their derivatives is a genuine statement about the curve and not about its parametrization. In do Carmo's own development the local canonical form (§1-6) and the global results of §1-7 both rest on the Frenet apparatus fixed here.

Mathlib contains the analytic ingredients — the Picard–Lindelöf theorem, existence and uniqueness for linear ODE systems, orthonormal bases and the orthogonal group of a real inner product space — but it does not contain the Frenet trihedron of a space curve, the torsion of a space curve, or this theorem. What this mission produces is therefore a reusable formal vocabulary for the local theory of space curves, plus machine-checked proofs of the classical statements about it. The mathematics is completely classical and has been known since Frenet (1847) and Serret (1851); what is open here is the formalization, not the mathematics.

Difficulty

The uniqueness half is a short argument on paper — the function $|t - \bar t|^2 + |n - \bar n|^2 + |b - \bar b|^2$ has vanishing derivative by the Frenet formulas — but formally it requires first establishing that the Frenet frame is differentiable and satisfies those formulas, which needs $k > 0$ and the smoothness of $s \mapsto \alpha''(s)$ away from its zeros, and then a connectedness argument on the interval.

The existence half cannot be done by exhibiting a formula: the curve is produced by solving the linear system $F' = A(s) F$ for the $3 \times 3$ frame $F$ , checking that the solution stays orthogonal (this is where the skew-symmetry of $A$ enters), and then integrating the first row. Recovering that the resulting curve has exactly the prescribed curvature and torsion, as computed by the definitions rather than as postulated by the ODE, is the step where most of the formal work sits.

The obvious shortcut — defining torsion by the closed formula $-(\alpha' \wedge \alpha'') \cdot \alpha''' / k^2$ — is not taken here: the definition is the book's, $b' = \tau n$ , and the closed formula is a milestone to be proved.

Formalization scope

Curves are total functions ℝ → EuclideanSpace ℝ (Fin 3) that are assumed smooth only on the open interval Set.Ioo a b; smoothness is ContDiffOn ℝ (⊤ : ℕ∞), matching do Carmo's use of "differentiable" to mean $C^\infty$ . Because the interval is open, the ordinary deriv agrees with the derivative along the interval at every interior point, and all derivatives in the statements are plain iterated deriv. Curvature, normal, binormal and torsion are defined exactly as above; at points where $k = 0$ the normal vector takes the junk value $0$ , so every statement that mentions $n$ , $b$ or $\tau$ carries the hypothesis $k \neq 0$ explicitly.

The vector product is defined componentwise on EuclideanSpace ℝ (Fin 3), and a rigid motion is a LinearIsometryEquiv of EuclideanSpace ℝ (Fin 3) with positive determinant followed by a translation.

Degenerate intervals are not excluded: if $b \le a$ the interval is empty and the statements hold vacuously, which is why the goal is not formulated as a statement about a single point but as a statement about all of $(a,b)$ — no hypothesis is vacuous for $a < b$ , and the existence clause is a genuine construction.

Contributions welcome: the Frenet apparatus and the ODE construction are the reusable parts, and both are prerequisites for the later missions of this series.

Selected references

Manfredo P. do Carmo, Differential Geometry of Curves and Surfaces, 2nd edition, Dover, 2016, Chapter 1, §1-4 and §1-5 (statement on p. 19, uniqueness proof pp. 20–22, existence in the appendix to Chapter 4).
F. Frenet, Sur les courbes à double courbure, Journal de Mathématiques Pures et Appliquées 17 (1852), 437–447.
J. A. Serret, Sur quelques formules relatives à la théorie des courbes à double courbure, Journal de Mathématiques Pures et Appliquées 16 (1851), 193–207.

11 thms3 active usersReviewed

Group Theory·Captain: Lucas

Faithfulness of the Burau representation of B4Research Paper

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:

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.
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.
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:

$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.
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}]$ .
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.
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.

15 thms3 active usersReviewed

Differential Geometry·Captain: xuanji

Strong Whitney embedding in dimension 2nResearch Paper

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.

16 thms3 active usersReviewed

Differential Geometry Number Theory·Captain: t4v1

Thurston's Question 23: rational relations among hyperbolic volumesOpen Problem

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.

20 thms3 active usersReviewed

Algebraic Topology·Captain: Lucas

Smale's question: the homotopy type of Diff(S⁴)Open Problem

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

$\mathrm{Diff}(S^4) \simeq O(5)\times\mathrm{Diff}(D^4)$ (problem statement).
$\mathrm{Diff}(D^4) \simeq \Omega^5(Y,y)$ for some pointed space $(Y,y)$ (Cerf–Morlet, Budney).
$\mathrm{Diff}(D^4)$ is not contractible (Watanabe).
$\mathrm{Diff}(S^2) \simeq O(3)$ (Smale).
$\mathrm{Diff}(S^3) \simeq O(4)$ (Hatcher).
$|\pi_0\,\mathrm{Diff}(S^6)| = 56$ (Kervaire–Milnor and Cerf).
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

11 thms2 active usersReviewed

Completed

Algebraic Topology Symplectic Geometry·Captain: Mazecto

Conley–Zehnder Index I: Axiomatic Characterization on Paths of Symplectic MatricesResearch Paper

Motivation

The Conley–Zehnder index assigns an integer to a path of symplectic matrices that starts at the identity and ends at a matrix without eigenvalue $1$ . It is how periodic orbits of Hamiltonian and Reeb flows get graded. In Floer homology it gives the grading of the chain complex, generated by the $1$ -periodic orbits of a nondegenerate Hamiltonian (Salamon–Zehnder 1992; Salamon 1999). In contact homology and symplectic field theory it grades Reeb orbits. In the analysis of pseudoholomorphic curves it enters the Fredholm index formula for the linearized Cauchy–Riemann operator through the asymptotic orbits. In three-dimensional Reeb dynamics it defines dynamical convexity (every periodic orbit has index at least $3$ ), the hypothesis of the Hofer–Wysocki–Zehnder theorem on disk-like global surfaces of section (HWZ 1998).

Timeline. Conley and Zehnder introduced the index in their Morse-type index theory for periodic solutions of Hamiltonian equations (Conley–Zehnder 1984). Salamon and Zehnder gave the definition through a rotation function $\rho : \mathrm{Sp}(2n) \to S^1$ and related it to the Maslov index (SZ92). Robbin and Salamon extended it to arbitrary paths as a half-integer Maslov-type index (Robbin–Salamon 1993). Gutt attributes the properties naturality, homotopy, zero, product, loop, signature, determinant and inverse, and the characterization of the index by homotopy, loop and signature alone, to Salamon's lecture notes (Sal99) and to Audin–Damian (AD14); the statements used here are those of Gutt, Propositions 8–9. Gutt gives a self-contained account with several equivalent formulas, including the normalized complex determinant of the complex-linear part used below (Gutt 2014, §2).

Setting

Write $\mathbb{R}^{2n}$ with coordinates $(q,p)$ and let

J_0 = \begin{pmatrix} 0 & -\mathrm{Id} \\ \mathrm{Id} & 0 \end{pmatrix}.

The symplectic group $\mathrm{Sp}(2n)$ is the set of real $2n\times 2n$ matrices $A$ with $A J_0 A^{\mathsf T} = J_0$ . Let $\mathrm{Sp}^*(2n)$ be the set of $A \in \mathrm{Sp}(2n)$ with $\det(\mathrm{Id} - A) \neq 0$ .

$\mathrm{SP}(n)$ is the set of continuous paths $\psi : [0,1] \to \mathrm{Sp}(2n)$ with $\psi(0) = \mathrm{Id}$ and $\psi(1) \in \mathrm{Sp}^*(2n)$ . It carries the compact-open topology.

For $A \in \mathrm{Sp}(2n)$ , the complex-linear part is $C_A = \tfrac12 (A - J_0 A J_0)$ . It commutes with $J_0$ , so it has the block form $\begin{pmatrix} X & -Y \\ Y & X\end{pmatrix}$ , which is the complex matrix $X + iY$ once $\mathbb{R}^{2n}$ is identified with $\mathbb{C}^n$ by $(x,y) \mapsto x + iy$ . Set

\hat\rho(A) = \frac{\det_{\mathbb C}(X+iY)}{|\det_{\mathbb C}(X+iY)|} \in S^1.

Let $W^+ = -\mathrm{Id}$ and $W^- = \mathrm{diag}(2,-1,\dots,-1,\tfrac12,-1,\dots,-1)$ . Each $\psi \in \mathrm{SP}(n)$ extends to a path $\tilde\psi : [0,2] \to \mathrm{Sp}(2n)$ with $\tilde\psi = \psi$ on $[0,1]$ , $\tilde\psi(t) \in \mathrm{Sp}^*(2n)$ for $t \geq 1$ , and $\tilde\psi(2) \in \{W^+, W^-\}$ . The map $\hat\rho^2 \circ \tilde\psi$ is then a loop in $S^1$ , and

\mu_{CZ}(\psi) = \deg\big(\hat\rho^2 \circ \tilde\psi\big).

For a loop $\varphi : [0,1] \to \mathrm{Sp}(2n)$ with $\varphi(0) = \varphi(1) = \mathrm{Id}$ , the Maslov index is $\mu(\varphi) = \deg(\hat\rho\circ\varphi)$ . For a symmetric matrix $S$ , $\mathrm{Sign}(S)$ is the number of positive eigenvalues minus the number of negative eigenvalues.

Formalization targets

Goal: existence and uniqueness

The map $\mu_{CZ} : \mathrm{SP}(n) \to \mathbb{Z}$ has the following three properties, and every map $\mu : \mathrm{SP}(n) \to \mathbb{Z}$ with these properties equals $\mu_{CZ}$ :

Homotopy. $\mu$ is constant on the connected components of $\mathrm{SP}(n)$ .
Loop. $\mu(\varphi\psi) = \mu(\psi) + 2\mu(\varphi)$ for every loop $\varphi$ at $\mathrm{Id}$ and every $\psi \in \mathrm{SP}(n)$ .
Signature. If $S = S^{\mathsf T}$ is nondegenerate and all of its eigenvalues have absolute value $< 2\pi$ , then $\mu\big(t \mapsto \exp(tJ_0S)\big) = \tfrac12 \mathrm{Sign}(S)$ .

Milestones

$\det_{\mathbb C} C_A \neq 0$ for every $A \in \mathrm{Sp}(2n)$ .
$\deg(\hat\rho^2\circ\tilde\psi)$ exists and does not depend on the extension $\tilde\psi$ .
$\deg(\hat\rho\circ\varphi)$ is well defined for loops.
Naturality. $\mu_{CZ}(\varphi\psi\varphi^{-1}) = \mu_{CZ}(\psi)$ for every path $\varphi$ in $\mathrm{Sp}(2n)$ .
Homotopy, for $\mu_{CZ}$ .
Zero. If $\psi(s)$ has no eigenvalue on the unit circle for $s > 0$ , then $\mu_{CZ}(\psi) = 0$ .
Product. $\mu_{CZ}(\psi'\diamond\psi'') = \mu_{CZ}(\psi') + \mu_{CZ}(\psi'')$ under the symplectic block embedding $\mathrm{Sp}(2n')\times\mathrm{Sp}(2n'') \hookrightarrow \mathrm{Sp}(2(n'+n''))$ .
Loop, for $\mu_{CZ}$ .
Signature, for $\mu_{CZ}$ .
Determinant. $(-1)^{n-\mu_{CZ}(\psi)} = \operatorname{sign}\det(\mathrm{Id} - \psi(1))$ .
Inverse. $\mu_{CZ}(\psi^{-1}) = \mu_{CZ}(\psi^{\mathsf T}) = -\mu_{CZ}(\psi)$ .
Uniqueness. Homotopy, loop and signature determine $\mu_{CZ}$ on $\mathrm{SP}(n)$ .

Significance

The result. The characterization makes the index a canonical invariant: any construction of an integer invariant of nondegenerate symplectic paths that is homotopy invariant and has the correct loop and signature behaviour is the Conley–Zehnder index. In practice this is how different definitions in the literature are identified with one another (rotation function, polar decomposition, complex-linear part, crossing forms, spectral flow of asymptotic operators). The listed properties are used directly to compute indices of concrete orbits, for instance the iterates of orbits of ellipsoids and the orbits of convex energy surfaces.

Formalizing it. All results here are classical and proved. No formalization of the Conley–Zehnder index exists in Mathlib. This mission produces a reusable library for symplectic linear algebra in Lean: the index and the Maslov index of loops as functions on path spaces, together with their computational properties. It is the first stage of a formalization of the Fredholm theory of linearized Cauchy–Riemann operators, whose index formula is stated in terms of Conley–Zehnder indices. It also gives a general-dimension definition against which the two-dimensional winding-interval definitions used in existing dynamical-convexity statements can be compared.

Difficulty

The index is defined through a choice: an extension of the path to $W^\pm$ inside $\mathrm{Sp}^*(2n)$ and a continuous argument of a circle-valued map. Before any property can be stated as a property of a function, the result must be shown independent of these choices. That is not a local computation: it depends on the global topology of the symplectic group and on how the set of matrices with eigenvalue $1$ sits inside it.

The properties themselves are statements about the degree of maps into $S^1$ built from determinants, and $\hat\rho$ is not a homomorphism. So none of the properties follows from a calculation on a single matrix, and loop and product require control of degrees under pointwise products and block sums. The uniqueness statement quantifies over all integer-valued functions on a path space. The argument for it has to use only the three listed properties and the topology of $\mathrm{SP}(n)$ .

Formalization scope

Namespace ConleyZehnder; all definitions are in ConleyZehnder_Setting.
Matrices are Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ. $J_0$ is Mathlib's Matrix.J, and $\mathrm{Sp}(2n)$ is Matrix.symplecticGroup. Paths are C(unitInterval, Mat n) with the compact-open topology. $\mathrm{SP}(n)$ is a Set of such paths, and "connected component" means connectedComponentIn (SP n).
Index maps are functions $\mu$ on all of C(unitInterval, Mat n). Every property constrains $\mu$ only on $\mathrm{SP}(n)$ , and the paths $\varphi\psi\varphi^{-1}$ , $\psi^{-1}$ , $\psi^{\mathsf T}$ , $\psi'\diamond\psi''$ and $\exp(tJ_0S)$ are passed as continuous maps with the stated pointwise values.
Degree is expressed by continuous real lifts: IsArgLift f θ means $f(t) = e^{i\theta(t)}$ . IsCZValue ψ k says that some extension and some lifts give $2\big(\Delta\theta_\psi + \Delta\theta_\chi\big) = 2\pi k$ , where $\chi$ is the part of the extension after $t = 1$ . czIndex and maslovIndex are defined by choice from these predicates, with fallback value $0$ . Milestones 2 and 3 are what make the fallback unreachable. Without them, any property proved for czIndex would say nothing about the actual index.
The circle-valued map is $\hat\rho$ of Gutt, Corollary 12, formula (9). The rotation function $\rho$ of Salamon–Zehnder (built from eigenvalue multiplicities and Krein signs) is not formalized. Gutt, Proposition 10 and Corollaries 11–12, shows that the degrees agree. The Maslov index of loops is also taken with $\hat\rho$ .
The signature uses Matrix.IsHermitian.eigenvalues; for real matrices, Hermitian means symmetric. The norm bound is stated as $|\lambda| < 2\pi$ for every eigenvalue $\lambda$ . The signature property is stated as $2\mu = \mathrm{Sign}(S)$ .
$n = 0$ is allowed: $\mathrm{SP}(0)$ is a single path and every property holds for it.

Contributions welcome: general lemmas on degrees of maps $[0,1]\to S^1$ (existence and uniqueness of lifts, additivity under products and concatenation, homotopy invariance), and the topology of $\mathrm{Sp}(2n)$ and $\mathrm{Sp}^*(2n)$ . These are reusable well beyond this mission.

Selected references

C. Conley, E. Zehnder, Morse-type index theory for flows and periodic solutions for Hamiltonian equations, Comm. Pure Appl. Math. 37 (1984), 207–253. https://doi.org/10.1002/cpa.3160370204
D. Salamon, E. Zehnder, Morse theory for periodic solutions of Hamiltonian systems and the Maslov index, Comm. Pure Appl. Math. 45 (1992), 1303–1360. https://doi.org/10.1002/cpa.3160451004
J. Robbin, D. Salamon, The Maslov index for paths, Topology 32 (1993), 827–844. https://doi.org/10.1016/0040-9383(93)90052-W
H. Hofer, K. Wysocki, E. Zehnder, The dynamics on three-dimensional strictly convex energy surfaces, Ann. of Math. 148 (1998), 197–289. https://doi.org/10.2307/120994
D. Salamon, Lectures on Floer homology, in: Symplectic Geometry and Topology, IAS/Park City Math. Ser. 7, AMS (1999), 143–229. https://doi.org/10.1090/pcms/007/05
M. Audin, M. Damian, Morse Theory and Floer Homology, Universitext, Springer (2014); French original 2010. https://doi.org/10.1007/978-1-4471-5496-9
J. Gutt, Generalized Conley–Zehnder index, Ann. Fac. Sci. Toulouse Math. (6) 23 (2014), 907–932. https://doi.org/10.5802/afst.1430 (arXiv:1307.7239)

32 thms2 active usersReviewed

Completed

Group Theory·Captain: marwahaha

An Artin group with no geometric CAT(0) actionOpen Problem

Motivation

Artin presentations often admit useful geometric models of nonpositive curvature. The source constructs a finite presentation designed to obstruct every geometric action on a proper CAT(0) space. The source is OpenAI's September 2026 manuscript.

Setting

A geometric action is an isometric group action that is proper and cocompact. CAT(0) is expressed by existence of geodesic segments and Euclidean comparison inequalities. The target uses one explicit Artin matrix on 116 generators.

Formalization targets

M=M^{\mathsf T},\quad M_{ss}=1,\quad M_{st}\in\{2,3,\infty\}\ (s\ne t),\qquad A_M\text{ has no geometric action on a nonempty proper CAT(0) space}.

The following explicit matrix on 116 generators is symmetric, has diagonal entries 1, and has every off-diagonal entry in {2, 3, ∞}, and that its Artin group admits no geometric action on any nonempty proper CAT(0) metric space. Index the generators by 0, …, 115. For each b = 0, 1, 2, form the ordered block (b, (b + 1) mod 3, 5 + 37b, …, 41 + 37b). Distinct generators have matrix entry 3 if they are consecutive in a block; otherwise they have entry 2 if they are nonconsecutive members of a block or one is 3 or 4 and the other is 0, 1, or 2; all remaining entries are ∞. The Artin group has these generators and, for each finite entry n, equates the two alternating words of length n starting with the corresponding generators. Here a CAT(0) space is a geodesic metric space satisfying Euclidean triangle comparison, and proper means that closed balls are compact. The excluded geometric action is an action by isometries such that, for every compact set K, only finitely many group elements g satisfy gK ∩ K ≠ ∅, and some compact set has translates covering the whole space. Thus, for every nonempty proper metric space and every action of this explicitly presented group, at least one of the CAT(0), isometry, compact-intersection finiteness, or compact-covering conditions fails.

The goal is OAI.ArtinCAT0.main.

Significance

The formal statement verifies the matrix’s structural properties and excludes actions of the resulting explicit group. It does not merely assert that some unspecified Artin group has an obstruction. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Ruling out one candidate complex is insufficient because the conclusion ranges over all nonempty proper metric spaces and actions. The algebraic relations must force a contradiction with geometric-action properties themselves.

Formalization scope

The matrix is generated by three overlapping length-39 blocks plus sentinel relations. Properness is compact-intersection finiteness and cocompactness is coverage by translates of a compact set. The action target is universe-polymorphic.

The shared definitions are supplied by ArtinCAT0. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, An Artin group with no geometric CAT(0) action, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms2 active usersReviewed

Completed

Differential Geometry·Captain: wurtle

A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved MetricResearch Paper

Motivation

Along a geodesic of a Riemannian manifold, a Jacobi field describes how nearby geodesics spread apart. Two points of a geodesic are conjugate if some nonzero Jacobi field vanishes at both; a metric has no conjugate points if this never happens. Nonpositive sectional curvature implies no conjugate points (by the Rauch comparison), and the two conditions share many consequences: the universal cover is diffeomorphic to $\mathbb R^n$ via the exponential map, and the fundamental group controls the geometry. For a single metric the converse fails: Gulliver (1975) produced metrics without conjugate points that have regions of positive curvature. The existence question is subtler: must a closed manifold that carries some metric without conjugate points also carry some metric of nonpositive curvature? Ivanov and Kapovitch (2014) and the Burns–Matveev survey (2021) ask this, explicitly including dimension three.

Background

1963. Milnor's Morse Theory develops the index-form framework for conjugate points.
1975. Gulliver shows that absence of conjugate points does not force nonpositive curvature for an individual metric (doi:10.1090/S0002-9947-1975-0383294-0).
1995. Leeb characterizes 3-manifolds with nonpositively curved metrics and gives two-piece graph-manifold obstructions (doi:10.1007/BF01231445).
1996. Kapovich and Leeb study discrete group actions on nonpositively curved spaces (doi:10.1007/BF01445254).
2014. Ivanov and Kapovitch ask the existence question (Questions 1.1, 8.1), single out graph manifolds glued from punctured-torus products, and prove that a closed 3-manifold has a metric without focal points iff it has one of nonpositive curvature (doi:10.4310/jdg/1393424918).
2021. Burns and Matveev list the question (Question 4.1.2) (doi:10.1017/etds.2019.73).

In dimension two the answer is positive (Euler characteristic and uniformization), so dimension three is the first case. The source of this mission is an OpenAI preprint dated September 24, 2026, which answers the question negatively in dimension three.

Setting

Let $M$ be a closed (compact, boundaryless) connected smooth 3-manifold with a smooth Riemannian metric $g$ . In a chart, with Christoffel symbols $\Gamma^i_{jk}$ , a curve $\gamma$ is a geodesic if $\ddot\gamma^i+\Gamma^i_{jk}\dot\gamma^j\dot\gamma^k=0$ . With covariant derivative $D_s$ along $\gamma$ and curvature $R(X,Y)Z=\nabla_X\nabla_YZ-\nabla_Y\nabla_XZ-\nabla_{[X,Y]}Z$ , a Jacobi field is a smooth vector field $J$ along $\gamma$ with

D_s^2J+R(J,\dot\gamma)\dot\gamma=0.

$g$ has no conjugate points if every Jacobi field vanishing at two distinct times vanishes identically. $g$ has nonpositive sectional curvature if $g(R(u,v)v,u)\le0$ for all tangent vectors $u,v$ .

Formalization targets

Goal: Theorem 1.1

\exists\,M\ \text{closed, connected, orientable smooth 3-manifold}:\quad \exists\,g\ \text{without conjugate points},\quad \nexists\,g'\ \text{with } \sec_{g'}\le0.

The Lean statement OAI.ThreeManifold.main_theorem is open on the platform.

Significance

The theorem shows that, starting in dimension three, the existence of a metric without conjugate points is strictly weaker than the existence of a nonpositively curved metric, answering the Ivanov–Kapovitch question. The same manifold carries no locally CAT(0) length metric and, by the Ivanov–Kapovitch equivalence, no metric without focal points, so it separates "no conjugate points" from "no focal points" as well. The example is a graph manifold glued from two copies of (punctured torus) $\times S^1$ , exactly the test case Ivanov and Kapovitch proposed.

The result is stated in an OpenAI preprint; it has not been peer reviewed, and no machine-checked proof exists.

Difficulty

Two separate problems must be solved. The obstruction side (no nonpositively curved metric) follows from Leeb's graph-manifold criterion and is group-theoretic. The construction side is analytic: one must build a metric across the gluing neck and prove that every complete geodesic, including those that enter and leave the neck infinitely often at arbitrary angles, has no conjugate points. Nonpositive curvature is not available in the neck, so the Rauch comparison does not apply; the index form must be controlled with endpoint terms uniformly in entry angle, turning height and excursion time.

Formalization scope

Manifolds are ChartedSpace (Fin 3 → ℝ) with IsManifold 𝓘(ℝ, Fin 3 → ℝ) ∞, compact, connected, Hausdorff, second countable; orientability is OrientedAtlas (all transition maps have positive Jacobian determinant).
Metrics are ContMDiffRiemannianMetric; Christoffel symbols and curvature are computed in every atlas chart from fderiv of the coordinate metric.
IsGeodesicOn g γ U asks for a smooth curve satisfying the geodesic equation in every chart on the open interval U; IsJacobiFieldOn asks for chart-smooth fields satisfying the Jacobi equation.
NoConjugatePoints g: for every open interval U, geodesic and Jacobi field on U, vanishing at two distinct times forces vanishing on U.
NonpositiveSectionalCurvature g: $g(R(u,v)v,u)\le0$ for all chart points and vectors; the goal asserts no smooth metric on the same smooth manifold has this property.

A complete development needs Riemannian geometry in coordinates, geodesic flows and Jacobi fields, the index form, Cartan–Hadamard/flat torus theorems and the group theory of graph manifolds. Contributions formalizing Theorem 2.1 (no proper cocompact CAT(0) action), Lemma 6.2 (index-form criterion) and Proposition 6.1 (assembly of passage estimates) are welcome.

Selected references

OpenAI, A Three-Manifold Without Conjugate Points and Without a Nonpositively Curved Metric, preprint, September 24, 2026. https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Three-Manifold-Without-Conjugate-Points-and-Without-a-Nonpositively-Curved-Metric-September-24-2026/paper.pdf
S. Ivanov, V. Kapovitch, Manifolds without conjugate points and their fundamental groups, J. Differential Geom., 2014. https://doi.org/10.4310/jdg/1393424918
K. Burns, V. S. Matveev, Open problems and questions about geodesics, Ergodic Theory Dynam. Systems, 2021. https://doi.org/10.1017/etds.2019.73
R. Gulliver, On the variety of manifolds without conjugate points, Trans. Amer. Math. Soc., 1975. https://doi.org/10.1090/S0002-9947-1975-0383294-0
B. Leeb, 3-manifolds with(out) metrics of nonpositive curvature, Invent. Math., 1995. https://doi.org/10.1007/BF01231445
M. Kapovich, B. Leeb, Actions of discrete groups on nonpositively curved spaces, Math. Ann., 1996. https://doi.org/10.1007/BF01445254
J. Milnor, Morse Theory, Princeton University Press, 1963.

31 thms2 active usersReviewed

Dynamical Systems·Captain: Lucas

Building Anosov flows on 3-manifolds (Béguin–Bonatti–Yu)Research Paper

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

59 thms2 active usersReviewed

Algebraic Geometry·Captain: Lucas

Algebraicity of Weil classes on abelian sixfolds of discriminant -1Research Paper

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:

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.
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.
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}$ .
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.
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

7 thms2 active usersReviewed

Topology·Captain: Lucas

Which homology 3-spheres bound homology 4-balls?Open Problem

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.

10 thms1 active userReviewed

Topology·Captain: Lucas

Slice–ribbon conjectureOpen Problem

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).

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)$ .
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.
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.
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.
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

[F] Ribbon knots are slice — the converse direction, observed by Fox.
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.
[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

7 thms1 active userReviewed

Topology·Captain: Lucas

Smooth 4-dimensional Poincaré conjectureOpen 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

M \text{ closed smooth 4-manifold},\ M \simeq S^4 \implies M \cong_{C^\infty} S^4.

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.

9 thms1 active userReviewed

Topology·Captain: Lucas

Smooth 4-dimensional Schoenflies problemOpen Problem

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$ ,

\overline{C_x} \text{ is diffeomorphic to } D^4 .

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

Milestones (known results)

Jordan–Brouwer separation, all $n$ : $S^{n+1} \setminus f(S^n)$ has exactly two components, each with frontier $f(S^n)$ .
Generalized Schoenflies theorem (Mazur, Brown), all $n$ : each $\overline{C_x}$ is homeomorphic to $D^{n+1}$ .
Schoenflies, $n = 1$ : each $\overline{C_x}$ is diffeomorphic to $D^2$ .
Alexander, $n = 2$ : each $\overline{C_x}$ is diffeomorphic to $D^3$ .
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

7 thms1 active userReviewed

Completed

Algebraic Topology Category Theory Mathematical Physics·Captain: Alien60

Gauge Functors on a Finite Graph: The Holonomy Equivalence for Non-Abelian Gauge TheoryResearch Paper

Motivation

A gauge theory can be formulated in several mathematically different ways: with potentials (connections), with field strengths (curvature), or with holonomies, the parallel transports around closed loops. Philosophers and physicists ask whether these formulations say the same thing, and which one carries "surplus structure".

Category theory makes the question precise. Each formulation is a category of models, and each translation between formulations is a functor. A functor that is faithful and essentially surjective but not full forgets structure. One that is full and faithful but not essentially surjective forgets properties. One that is full and essentially surjective but not faithful forgets stuff. One that is all three forgets nothing and is an equivalence. This taxonomy is due to Baez, Bartels and Dolan (Baez–Shulman, §2.4).

Weatherall (2016) applied it to electromagnetism. Potentials without gauge arrows forget structure relative to field strengths (Proposition 1). The erratum in arXiv v2 (p. 15) corrects his Proposition 2: the principal-bundle formulation, whose arrows include gauge transformations, forgets only stuff, not nothing. Nguyen, Teh and Wells obtain the same verdict for the gauge-orbit functor (their Proposition 3.2.3). In their footnote 26 they identify the forgotten stuff as the constant ("global") gauge transformations. All of this is abelian, U(1) on a contractible spacetime.

The non-abelian counterpart is the holonomy formulation. Barrett's reconstruction and representation theorems, and their categorical upgrade by Rosenstock and Weatherall (Theorem 2), show that on a connected manifold, principal connections and generalized holonomy maps form equivalent categories. On the topological side, Freed and Quinn (eqs. 3.11–3.13) identify the automorphisms of a finite-group gauge field with a centralizer.

This mission states these results for an arbitrary group $G$ on a finite graph. There the smooth and topological subtleties disappear, but the categorical content survives intact.

Setting

A finite directed graph $X$ has vertices $\mathrm{Fin}\,n_V$ , edges $\mathrm{Fin}\,n_E$ , and maps $\mathrm{src},\mathrm{tgt}$ . A step is an edge traversed forwards or backwards, and a walk $x \to y$ is a list of steps whose endpoints chain. $X$ is connected from $x$ if every vertex is reached by a walk from $x$ .

A connection is $A : E \to G$ . Its holonomy along a walk is the ordered product of $A(e)$ (forwards) and $A(e)^{-1}$ (backwards), as in Baez (1996), §2.
A gauge transformation is $g : V \to G$ , acting by $(g\cdot A)(e) = g(\mathrm{src}\,e)\,A(e)\,g(\mathrm{tgt}\,e)^{-1}$ .
$\mathsf{PotG}$ : objects are connections, and arrows $A \to B$ are gauge transformations with $g\cdot A = B$ . This is the discrete analogue of the groupoid $C_A$ of Nguyen–Teh–Wells.
$\mathsf{HolMap}_x$ : a holonomy map at $x$ assigns a group element to each walk. It is multiplicative on loops at $x$ and unchanged when a backtrack $s, \bar s$ is inserted into a loop at $x$ ; this is the discrete form of thin equivalence. Arrows $H \to H'$ are elements $h$ with $H'(\gamma) = h\,H(\gamma)\,h^{-1}$ on every loop at $x$ . Only values on loops at $x$ matter.
Functors. $\mathrm{hol}_x : \mathsf{PotG} \to \mathsf{HolMap}_x$ sends $A \mapsto \mathrm{hol}_A$ and $g \mapsto g(x)$ . $\mathrm{orbit}$ sends $\mathsf{PotG}$ to the discrete category of gauge orbits.
Curvature. On a 2-complex, each face has a base vertex and a boundary loop. The curvature functor sends $A$ to the family of conjugacy classes of its face holonomies, which is the gauge-invariant non-abelian field strength.

Formalization targets

Goal: the holonomy functor is an equivalence

X \text{ connected from } x \;\Longrightarrow\; \mathrm{hol}_x \text{ is full, faithful and essentially surjective.}

This is the discrete, fixed-base-point form of Rosenstock–Weatherall's Theorem 2. In the taxonomy above, potentials-with-gauge and holonomies forget nothing relative to each other. The statement holds for every group $G$ , finite or not. The base-point-changing arrows of Rosenstock–Weatherall are not included.

Milestones

Faithful. A gauge arrow between two connections is determined by its value at $x$ .
Full. Every conjugation relating the holonomy maps of $A$ and $B$ is realized by a gauge transformation.
Barrett reconstruction. Every holonomy map at $x$ equals $\mathrm{hol}_A$ on all loops at $x$ , for some connection $A$ .
Barrett representation. $\mathrm{hol}_A = \mathrm{hol}_B$ on loops at $x$ iff $B = g\cdot A$ for a gauge transformation with $g(x) = 1$ , and that $g$ is unique.
Stabilizer = centralizer. Evaluation at $x$ is a bijection from the gauge stabilizer of $A$ onto the centralizer of its holonomies at $x$ . This is the non-abelian $H^0$ , the discrete form of Freed–Quinn (3.11)–(3.13).
The orbit functor forgets only stuff. It is full and essentially surjective. It is faithful iff $X$ has no vertices or $G$ is trivial. This is the discrete form of Nguyen–Teh–Wells Proposition 3.2.3 and of Weatherall's corrected Proposition 2.
Aharonov–Bohm. Take $G$ nontrivial, abelian or not. On the boundary of a triangle, which has no faces, the curvature functor is not full: flat connections with different holonomy are not gauge-equivalent. On the filled triangle the curvature functor is full and essentially surjective but not faithful.

Significance

Equivalence of formulations. The goal says that, once gauge transformations are arrows, the potential and holonomy formulations of non-abelian lattice gauge theory are categorically equivalent. This is the precise sense in which "the physics is in the holonomies".
Stuff and global symmetry. Milestones 5–6 locate the forgotten stuff exactly. When potentials are compared with gauge-invariant data that lacks arrows, the stuff is the centralizer of the holonomy group, the global gauge symmetry that survives a choice of connection. In the abelian case this is Nguyen–Teh–Wells' footnote 26. In general it is the automorphism group that weights the Dijkgraaf–Witten / Freed–Quinn sum.
Topology. Milestone 7 shows that on a non-simply-connected graph the curvature formulation also forgets structure. Weatherall's footnote 9 sets this situation aside for Minkowski space.
Novelty. Each ingredient is classical in some setting. A machine-checked statement of the non-abelian classification on finite graphs, in the language of forgetful functors, does not appear to exist. It is a step towards treating the theories-as-categories programme formally.

Difficulty

Combinatorics of walks. Lists of steps, their endpoint conditions, and the interaction of concatenation with backtracking all have to be handled explicitly. The goal and Milestones 1–4 need statements about walks between arbitrary vertices, not only loops.
Essential surjectivity. Reconstruction has to produce a connection from data that is only constrained on loops at one vertex. Connectivity enters non-trivially.
Faithfulness versus fullness. These use the hypotheses differently, and the boundary cases (empty graph, trivial group) have to be tracked.
Milestone 7 needs explicit non-equivalences, and so a gauge invariant separating gauge orbits.

Formalization scope

Graphs. These are finite directed graphs with Fin-indexed cells and are not required to be simple. Loops and multiple edges are allowed. A 2-complex adds faces with a base vertex and a boundary walk proved to be a loop.
Groups. $G$ is any Group; finiteness is not assumed.
Holonomy maps. These are functions on all lists of steps whose axioms only constrain loops at $x$ . Two maps agreeing on loops are isomorphic in $\mathsf{HolMap}_x$ (via $h = 1$ ) but need not be equal. Reconstruction is therefore stated on loops.
Functor properties. These are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj. The goal is their conjunction, not an explicitly constructed inverse.
Excluded. Spacetime symmetries (graph automorphisms), base-point-changing holonomy isomorphisms, and smooth or continuum statements are left out.
Proved in the definitions. Gauge covariance of holonomy along walks is proved in the definitions file, because the functors require it.

Selected references

J. O. Weatherall, "Understanding Gauge", Philosophy of Science 83 (2016) 1039–1049. arXiv:1505.02229. arXiv v2 includes the erratum to Proposition 2 (p. 15).
J. Nguyen, N. J. Teh, L. Wells, "Why surplus structure is not superfluous", British Journal for the Philosophy of Science 71 (2020). arXiv:1712.01228
S. Rosenstock, J. O. Weatherall, "A categorical equivalence between generalized holonomy maps on a connected manifold and principal connections on bundles over that manifold", J. Math. Phys. 57 (2016) 102902. arXiv:1504.02401
D. S. Freed, F. Quinn, "Chern–Simons theory with finite gauge group", Comm. Math. Phys. 156 (1993) 435–472. arXiv:hep-th/9111004
J. C. Baez, M. Shulman, "Lectures on n-categories and cohomology", in Towards Higher Categories, Springer (2010) 1–68. arXiv:math/0608420
J. C. Baez, "Spin network states in gauge theory", Adv. Math. 117 (1996) 253–272. arXiv:gr-qc/9411007

10 thms1 active userReviewed

Completed

Algebraic Topology Category Theory Mathematical Physics·Captain: Alien60

Weatherall 2016: Potentials vs. Field Strengths on a Finite 2-ComplexResearch Paper

Motivation

Philosophers of physics ask when a formulation of a theory carries excess structure: mathematical distinctions between models that make no physical difference. The standard example is electromagnetism written with a vector potential $A$ . Potentials that differ by a gauge transformation $A \mapsto A + d\lambda$ have the same field strength $F = dA$ , and on the usual view they represent the same physical situation.

Weatherall (2016) made this precise with category theory. Each formulation becomes a category of models, and a translation between formulations becomes a functor. A functor that is faithful and essentially surjective but not full forgets structure. One that is full and faithful but not essentially surjective forgets properties. One that is full and essentially surjective but not faithful forgets stuff. Weatherall's Proposition 1 says the functor $A \mapsto dA$ from potentials to field strengths forgets only structure, provided the arrows between potentials are spacetime symmetries that preserve $A$ . His Proposition 2 says the principal-bundle formulation, whose arrows include gauge transformations, forgets nothing. His footnote 15 notes that adding gauge transformations as arrows between potentials yields a category equivalent to that of field strengths (Weatherall, arXiv:1411.5757).

These arguments work on Minkowski space, which is contractible. Weatherall's footnote 9 sets topology aside for that reason. The follow-up literature, for example Nguyen, Teh and Wells (2018), compares these and related functors further. This mission states the comparison exactly on a finite cell complex, where topology cannot be set aside. Each of the three ways a functor can forget information then corresponds to one cohomology group.

Setting

A finite oriented 2-complex $X$ has $n_V$ vertices, $n_E$ edges and $n_P$ faces, together with integer incidence numbers $\partial_1(e,v)$ and $\partial_2(p,e)$ satisfying $\sum_e \partial_2(p,e)\,\partial_1(e,v) = 0$ for every face $p$ and vertex $v$ . Nothing beyond this identity is required, so the incidence data need not come from a geometric complex; all results hold for any such integer data. Fix an additive commutative group $K$ of coefficients, for example $\mathbb{Z}$ , $\mathbb{R}$ , or $\mathbb{Z}/n$ as a discrete stand-in for $U(1)$ . The cochains are $C^0 = K^{V}$ (gauge parameters $\lambda$ ), $C^1 = K^{E}$ (potentials $A$ ) and $C^2 = K^{P}$ (field strengths $F$ ). The coboundaries are

(\delta^0\lambda)(e) = \sum_v \partial_1(e,v)\,\lambda(v), \qquad (\delta^1 A)(p) = \sum_e \partial_2(p,e)\,A(e),

and $\delta^1\delta^0 = 0$ .

There are three categories, with spacetime symmetries taken to be trivial:

$\mathsf{Fld}$ (Weatherall's EM1): its objects are the 2-cochains $F$ , and its only arrows are identities.
$\mathsf{Pot}_0$ (Weatherall's EM2): its objects are the 1-cochains $A$ , and its only arrows are identities.
$\mathsf{Pot}_G$ (potentials with gauge arrows): its objects are the 1-cochains $A$ . An arrow $A \to A'$ is a gauge parameter $\lambda \in C^0$ with $A + \delta^0\lambda = A'$ , and composition adds the parameters. Arrows are the parameters $\lambda$ themselves, so two parameters differing by an element of $\ker\delta^0$ (e.g. a constant) are distinct arrows, just as distinct vertical automorphisms are distinct arrows in Weatherall's bundle category EM3. This is the category of his footnote 15.

The field-strength functors $\mathsf{Pot}_0 \to \mathsf{Fld}$ and $\mathsf{Pot}_G \to \mathsf{Fld}$ send $A \mapsto \delta^1 A$ . In the second functor every gauge arrow goes to an identity.

Cohomology vanishing is stated elementarily:

$H^0 = 0$ means $\delta^0\lambda = 0 \Rightarrow \lambda = 0$ .
$H^1 = 0$ means every $A$ with $\delta^1 A = 0$ equals $\delta^0\lambda$ for some $\lambda$ .
$H^2 = 0$ means every $F$ equals $\delta^1 A$ for some $A$ .

Formalization targets

Goal: the cohomological classification

For every finite 2-complex $X$ and coefficient group $K$ , the functor $\mathsf{Pot}_G \to \mathsf{Fld}$ satisfies

\text{faithful} \iff H^0 = 0,\qquad \text{full} \iff H^1 = 0,\qquad \text{essentially surjective} \iff H^2 = 0.

Milestones

Proposition 1 analogue. If some $\delta^0\lambda \neq 0$ , then $\mathsf{Pot}_0 \to \mathsf{Fld}$ is faithful and not full, and it is essentially surjective iff $H^2 = 0$ .
Faithful iff $H^0 = 0$ .
Full iff $H^1 = 0$ .
Essentially surjective iff $H^2 = 0$ .
Aharonov–Bohm. On the triangle boundary circle3 with $\mathbb{Z}$ coefficients, the potential equal to $1$ on one edge has the same field strength as $0$ . No gauge arrow connects the two, so the functor is not full.
Forgetting only stuff. On the filled triangle with $\mathbb{Z}$ coefficients, the functor is full and essentially surjective but not faithful.

Significance

The result. The classification turns a qualitative philosophical diagnostic into a cohomological criterion.

Structure: Weatherall's "forgets structure" verdict for potentials without gauge arrows is the statement that $\ker\delta^1 \neq 0$ .
Topology: once gauge arrows are added, whether any structure is still forgotten is exactly the question whether $H^1 \neq 0$ . A nonzero $H^1$ is the Aharonov–Bohm situation, in which potentials with equal field strength differ by a gauge-invariant holonomy.
Stuff: the clause $\text{faithful} \iff H^0 = 0$ shows that on a geometric complex (every edge has boundary head minus tail) with at least one vertex and $K \neq 0$ , constant gauge parameters are non-identity automorphisms that the functor sends to identities. The functor therefore forgets stuff. This contrasts with the faithfulness clause of Weatherall's Proposition 2 for the bundle formulation, where the analogous constant vertical automorphisms are the subtle case.

Formalizing it. No machine-checked version of the theories-as-categories programme for gauge theory is known to the author of this mission. This mission is the base case of a planned discrete gauge-functor development: non-abelian groups, nontrivial symmetry groups, and holonomy-based equivalences.

Difficulty

The mathematics is elementary once stated. The work is in making the categorical notions line up with the cochain conditions. Three points need care:

In a discrete category, an isomorphism is an equality.
Fullness must be tested against arrows between arbitrary pairs of potentials, not only potentials with zero field strength.
Faithfulness concerns parallel gauge arrows, which differ exactly by elements of $\ker\delta^0$ .

The concrete milestones require computations on explicit complexes, including a gauge-invariant obstruction for the Aharonov–Bohm example.

Formalization scope

Complexes. Cells are indexed by Fin types, and the incidence numbers are integer-valued. The complex is finite but may be empty in any dimension.
Coefficients. $K$ is any AddCommGroup, and integers act on it by zsmul.
Categories. Fld and Pot0 are Mathlib Discrete categories. PotG carries a hand-written Category instance whose arrows are the structure GaugeHom.
Functor properties. Fullness, faithfulness and essential surjectivity are Mathlib's Functor.Full, Functor.Faithful and Functor.EssSurj.
Symmetries. Spacetime symmetries are fixed to be trivial, so the results compare categories of potentials and fields over a fixed complex.
Non-triviality. The cohomology conditions are explicit Props about the coboundaries, so none of them is a definition that makes a target hold trivially. The hypothesis of Milestone 1 excludes the degenerate case $\delta^0 = 0$ , in which that functor is full.
Infrastructure. The cochain API (delta0, delta1, $\delta^1\delta^0 = 0$ ) is proved in the definitions file and is reusable for discrete gauge theory and toric-code missions.

Selected references

J. O. Weatherall, "Understanding Gauge", Philosophy of Science 83 (2016) 1039–1049. arXiv:1505.02229, doi:10.1086/687936
J. O. Weatherall, "Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?". arXiv:1411.5757
J. Nguyen, N. J. Teh, L. Wells, "Why surplus structure is not superfluous", British Journal for the Philosophy of Science 71 (2020). arXiv:1712.01228

8 thms1 active userReviewed

Combinatorics Graph Theory·Captain: mikedeng1

Planar Graphs Have Bounded Queue-Number 2: Every Graph of Euler Genus g Has Queue-Number at Most 4g + 49Research Paper

Motivation

A queue layout of a graph places its vertices on a line and splits its edges into classes, called queues, so that inside one queue no edge is nested inside another. The minimum number of queues is the queue-number. Queue layouts were introduced by Heath, Leighton and Rosenberg (1992) and Heath and Rosenberg (1992) as the dual of stack layouts (book embeddings): reading the vertex order from left to right, the edges of one queue are opened and closed in first-in first-out order. Queue layouts are closely tied to track layouts and, through them, to three-dimensional grid drawings of graphs (§9 of the paper).

Whether planar graphs have bounded queue-number was asked by Heath, Leighton and Rosenberg in 1992 and stayed open for 27 years. The best general bounds before 2019 grew with the number of vertices: $O(\sqrt n)$ by Heath, Leighton and Rosenberg (1992), $O(\log^2 n)$ by Di Battista, Frati and Pach (2013), and $O(\log n)$ by Dujmović (2015); for Euler genus $g$ , Dujmović, Morin and Wood (2017) had $O(g + \log n)$ . Dujmović, Joret, Micek, Morin, Ueckerdt and Wood (arXiv:1904.04791, J. ACM 2020) proved that every planar graph has queue-number at most $49$ (Theorem 1), and extended the result to every graph embeddable in a fixed surface (Theorem 2) and to every proper minor-closed class (Theorem 3).

This mission is Theorem 2: graphs of Euler genus $g$ have queue-number at most $4g + 49$ . It is the second mission of a two-mission series; the first poses Theorem 1.

Setting

All graphs are finite and simple. A linear ordering $\preceq$ of the vertex set $V(G)$ is fixed. Two edges $vw$ and $xy$ with four distinct ends nest if $v \prec x \prec y \prec w$ (after renaming the ends). A queue is a set of edges no two of which nest. A $k$ -queue layout of $G$ is a linear ordering together with a partition of $E(G)$ into $k$ queues, and $\operatorname{qn}(G) \le k$ means that a $k$ -queue layout exists.

A layering of $G$ is an ordered partition $(V_0, V_1, \dots)$ of $V(G)$ such that every edge joins two vertices of the same or of consecutive layers. A BFS layering takes one root $r$ in each connected component and puts $v$ in layer $\operatorname{dist}(r, v)$ . A BFS spanning tree of a connected graph $G$ rooted at $r$ is a spanning tree $T$ with $\operatorname{dist}_T(r, v) = \operatorname{dist}_G(r, v)$ for every $v$ . A path in $T$ is vertical if the distance to $r$ grows by exactly one at every step.

The Euler genus of the orientable surface with $h$ handles is $2h$ , and that of the non-orientable surface with $c$ cross-caps is $c$ ; the Euler genus of a graph is the least Euler genus of a surface it embeds in (footnote 2 of the paper). Planar graphs are exactly the graphs of Euler genus $0$ . Combinatorially, an embedding of a graph is described by an embedding scheme: a cyclic order of the edges at each vertex (a rotation system) together with a sign on every edge (twisted or not). Tracing faces through the scheme gives a face count $f$ , and with $n$ vertices, $m$ edges and $c$ components the scheme has Euler genus $2c - n + m - f$ .

Formalization targets

Goal: Theorem 2 with the paper's bound

\text{Euler genus of } G \le g \ \Longrightarrow\ \operatorname{qn}(G) \le 4g + 49 .

The paper states Theorem 2 as $\operatorname{qn}(G) = O(g)$ and proves the explicit bound $4g + 49$ in §5. The goal poses that explicit bound, for every finite graph, connected or not.

Milestones

Lemma 18 (p. 18). Every BFS layering $(V_0, V_1, \dots)$ of a planar graph $G$ admits a $49$ -queue layout whose vertex ordering lists $V_0$ , then $V_1$ , then $V_2$ , and so on.
Lemma 21 (p. 19). If $G$ is connected with Euler genus at most $g$ and $T$ is a BFS spanning tree with layering $(V_i)$ , there is a connected (or empty) subgraph $Z$ with at most $2g$ vertices in each layer such that $G - V(Z)$ is planar and sits inside a connected planar graph $G^+$ whose own BFS layering $(W_i)$ satisfies $W_i \cap (V(G)\setminus V(Z)) = V_i \setminus V(Z)$ ; vertical paths of the BFS tree of $G^+$ restrict to vertical paths of $T$ .
The $4g$ -queue step (p. 23). If $G$ has a layering with at most $2g$ vertices of $Z$ per layer and $G - Z$ has a $49$ -queue layout ordered layer by layer, then $\operatorname{qn}(G) \le 4g + 49$ .

Significance

The result. Theorem 2 settles boundedness of the queue-number for every class of graphs embeddable in a fixed surface, with a bound linear in the Euler genus. Through the connection between queue-number and track-number, the paper derives from it (§9, Theorems 54 and 58) that a graph of Euler genus $g$ with $n$ vertices has track-number $g^{O(g^{4/7})}$ and a three-dimensional grid drawing of volume $g^{O(g^{4/7})} n$ , linear in $n$ for every fixed surface. It is also a step on the paper's route to Theorem 3 (proper minor-closed classes), since graphs on surfaces are the basic pieces of the Robertson–Seymour graph minor structure theorem. Lemma 21 is of independent use: it reduces a graph on a surface to a planar graph while controlling BFS layers.

Formalizing it. The result is proved; as far as is known it has no machine-checked proof. A formalization needs queue layouts, layerings, BFS layerings and vertical paths, and, independently of queues, a usable combinatorial theory of graphs on surfaces, which Lean's Mathlib does not have. The Euler genus definition of this mission (embedding schemes and face tracing) and Lemma 21 are reusable well beyond queue layouts.

Difficulty

The obvious reduction, deleting few vertices to make the graph planar, is not enough: a planar subgraph alone does not control how the deleted vertices interact with a queue layout. The deleted set must be thin in every BFS layer, and the planar remainder must carry a BFS layering compatible with the original one, which is what Lemma 21 provides. Its proof cuts the surface along a subgraph made of tree paths and must show that the cut graph is planar by an Euler-characteristic count over face-tracing data, and that distances from a new root agree with the old BFS distances. In Lean, the main obstacle is the surface side: Euler's formula for embedding schemes, the cutting operation on rotation systems, and the passage between the combinatorial notion of Euler genus and the drawing-based notion of planarity. The planar input, Lemma 18, is itself the whole of mission 1's argument (Theorem 15 with Lemmas 5 and 8).

Formalization scope

Graphs are SimpleGraph V on a finite type V : Type with decidable equality and adjacency.
" $\operatorname{qn}(G) \le k$ " is HasQueueLayout G k: an injective map ord : V → ℕ (the linear ordering) and an assignment of the edges of $G$ (G.edgeSet, not all unordered pairs) to Fin k such that no two edges in one queue nest; nesting uses strict inequalities, so edges sharing an end never nest. Queues may be empty.
A layering is a layer function L : V → ℕ; a BFS layering takes one root per component. Vertical paths are nonempty lists indexed from $0$ with distance $d + i$ , $d \ge 0$ .
Euler genus is combinatorial: EulerGenusLE G g asks for an embedding scheme (rotation permutation of the darts, cyclic at every vertex, and a symmetric edge signature) whose Euler genus $2c - n + m - f$ , computed in $\mathbb Z$ , is at most $g$ . The face count is half the number of face-tracing orbits plus the number of isolated vertices. Equivalence with footnote 2's topological definition is the Heffter–Edmonds–Ringel rotation principle and its non-orientable extension, with additivity over components; it is not part of the mission.
Planarity is the published RobertsonSeymour1986.GM5.IsPlanar: a crossing-free drawing in $\mathbb R^2$ by simple arcs. "Euler genus $0$ iff planar" is a theorem connecting the two definitions, not built into either.
"Euler genus $g$ " is read as "at most $g$ " throughout; every bound is monotone in $g$ . In Lemma 21, " $Z$ is connected" reads "empty or connected" (the paper takes $Z = \emptyset$ when $g = 0$ ), and the restriction of a vertical path may be empty.
Trivializing formalizations are ruled out: queues indexed on all pairs Sym2 V would deny edgeless graphs a $0$ -queue layout; non-strict nesting would forbid adjacent edges in one queue; a drawing that tolerates crossings would make every graph planar; a face count without halving, or without isolated vertices, would make the Euler genus too small or too large (the sanity checks confirm $K_3$ has a scheme of Euler genus $0$ , a twisted $K_3$ one of genus $1$ , and two isolated vertices genus $0$ ).
Welcome contributions: Euler's formula for embedding schemes, face-tracing lemmas, the planar case (Lemma 18, via mission 1's results), the cutting construction of Lemma 21, and the purely combinatorial $4g$ -queue step.

Selected references

V. Dujmović, G. Joret, P. Micek, P. Morin, T. Ueckerdt, D. R. Wood, Planar graphs have bounded queue-number, J. ACM 67(4), 2020; arXiv:1904.04791v5. https://arxiv.org/abs/1904.04791 , https://doi.org/10.1145/3385731
L. S. Heath, F. T. Leighton, A. L. Rosenberg, Comparing queues and stacks as mechanisms for laying out graphs, SIAM J. Discrete Math. 5(3), 1992. https://doi.org/10.1137/0405031
L. S. Heath, A. L. Rosenberg, Laying out graphs using queues, SIAM J. Comput. 21(5), 1992. https://doi.org/10.1137/0221055
V. Dujmović, Graph layouts via layered separators, J. Combin. Theory Ser. B 110, 2015. https://doi.org/10.1016/j.jctb.2014.07.005
V. Dujmović, P. Morin, D. R. Wood, Layered separators in minor-closed graph classes with applications, J. Combin. Theory Ser. B 127, 2017. https://doi.org/10.1016/j.jctb.2017.05.006
B. Mohar, C. Thomassen, Graphs on Surfaces, Johns Hopkins University Press, 2001.

9 thms1 active userReviewed

Calculus of Variations·Captain: marwahaha

Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidityOpen Problem

Motivation

Sharp filling inequalities compare the mass of a cycle with the least mass needed to fill it. The selected formulation extends a Euclidean coefficient to proper CAT(0) metric spaces. The pinned manuscript supplies the research context.

Setting

Integral currents are encoded metric currents with integer-multiplicity chart decompositions and integral boundary. The input is a compactly supported n-cycle for n at least two. In the displayed coefficient, σ_n=(n+1)ω_{n+1}, where ω_{n+1} is the Euclidean volume of the unit ball in dimension n+1; this is the published sphereArea convention.

Formalization target

The selected goal is OAI.CAT0Fillings.sharp_integral_filling. Its central assertion is

\partial S=T,\qquad\mathbf M(S)\leq\frac{\mathbf M(T)^{(n+1)/n}}{(n+1)\sigma_n^{1/n}}.

The theorem states that, for a proper metric space X with its Borel σ-algebra that is CAT(0), meaning there is a choice of geodesic parametrization segment(x,y,t) from x to y (with segment(x,y,0)=x, segment(x,y,1)=y, and dist(segment(x,y,s),segment(x,y,t))=|s−t|·dist(x,y) for s,t in [0,1]) satisfying the comparison inequality dist(segment(o,x,s),segment(o,y,t))² ≤ (s·d(o,x) − t·d(o,y))² + s·t·(d(x,y)² − (d(o,x) − d(o,y))²), the following filling property holds for every integer n ≥ 2. Let T be an integral n-current on X, that is, a metric current (a multilinear functional on a bounded Lipschitz function and n Lipschitz functions, with locality, continuity and finite mass) that is a countable sum of disjointly supported integer-multiplicity bi-Lipschitz chart pieces and whose boundary has the same properties, and suppose T is compactly supported and a cycle, meaning its boundary is zero. Then there exists a compactly supported integral (n+1)-current S on X whose boundary is T and whose mass satisfies mass(S) ≤ c_n · mass(T)^((n+1)/n), where c_n = 1/((n+1)·(σ_n)^(1/n)), σ_n = (n+1)·ω_{n+1} is the area of the unit n-sphere and ω_{n+1} is the volume of the unit ball in Euclidean (n+1)-space. This is an admitted theorem statement, not a verified proof.

Significance and status

The goal is the CAT(0) integral-current filling inequality. Euclidean coefficient optimality is an additional reference. The manifold perimeter comparison and equality-rigidity statements in the manuscript are not separate attached targets. The target is currently Open on Prove2Me. The manuscript's mathematical argument and a machine-checked proof of the selected statement are separate deliverables.

Difficulty

The sharp coefficient must hold without a smooth manifold model, while preserving integrality, compact support and the exact boundary.

Formalization scope

The exact published goal, its hypotheses and its referenced definition blocks specify the requested formalization. The explanatory formula above is a summary; all quantifiers and additional clauses in the linked statement remain required.

Additional published targets are included as separate references:

OAI.SharpIntegralFillings.coefficient_optimal (Open).

Selected references

OpenAI, Generalized Cartan–Hadamard isoperimetry and Euclidean equality rigidity, preprint, 2026. Manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Selected goal source.

4 thms1 active userReviewed

Group Theory·Captain: marwahaha

A hyperbolic group with no geometric CAT(0) actionOpen Problem

Motivation

A linear filling inequality captures a form of large-scale negative curvature. The source asks whether a finite aspherical complex with that property must admit a geometric model of local nonpositive curvature. The source is OpenAI's September 2026 manuscript.

Setting

A finite complex has its usual barycentric realization. Asphericity means higher homotopy groups vanish. A linear disk-filling inequality bounds triangular face moves needed to fill an edge loop by a constant times its length.

Formalization targets

\exists K:\quad K\text{ finite, connected, aspherical, with linear disk filling},\quad\pi_1K\text{ hyperbolic with no geometric CAT(0) action}.

The defined proposition MainStatement holds, namely that there exist a finite abstract simplicial complex K on vertices Fin n, with its standard barycentric realization |K| (nonnegative coordinate vectors summing to 1 supported on a face), a basepoint x in |K|, and a real constant C ≥ 0 such that all of the following hold. |K| is connected and aspherical at x, meaning every homotopy group π_{m}(|K|,x) with m ≥ 2 is trivial. K satisfies a linear disk-filling inequality: every closed edge path p that bounds some disk, where a disk is a chain of elementary moves (collapsing a repeated vertex, removing a spur a,b,a, or replacing a,b,c by a,c across a nondegenerate triangular face, which costs one) reducing p to a single vertex, admits such a disk using at most C times (length of p minus 1) triangular faces. The fundamental group G = π₁(|K|,x) is word hyperbolic in the four-point sense: for some finite generating set S and some δ ≥ 0, every a,b,c,d in G satisfy d(a,c)+d(b,d) ≤ max(d(a,b)+d(c,d), d(a,d)+d(b,c)) + 2δ, where d is word distance. G admits no geometric CAT(0) action: there is no proper cocompact isometric action of G on any nonempty proper complete metric space X (in universe u) that is CAT(0), in the sense that segments exist with the squared-distance comparison inequality. Finally, for every finite complex L whose realization is homotopy equivalent to |K|, there is no metric on |L|, inducing its given topology, that is geodesic and locally CAT(−1), meaning each point has a ball that satisfies the hyperbolic-cosine midpoint inequality cosh d(z,m) ≤ (cosh d(z,x)+cosh d(z,y))/(2cosh(d(x,y)/2)) for segment midpoints m.

The goal is OAI.HyperbolicObstruction.main.

Significance

The goal also excludes a finite homotopy-equivalent complex with a compatible geodesic locally CAT(-1) metric. It joins a finite topological model, a group-theoretic obstruction, and a metric-model consequence. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

A large-scale hyperbolicity inequality does not directly construct a local curvature metric. Excluding all geometric actions requires more than finding a defect in the original complex’s chosen metric.

Formalization scope

Word hyperbolicity uses the four-point word-distance condition. Excluded CAT(0) actions are on nonempty proper complete spaces. The final metric must induce the finite realization’s existing topology; changing that topology is not permitted.

The shared definitions are supplied by HyperbolicObstruction. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

OpenAI, A hyperbolic group with no geometric CAT(0) action, preprint, September 2026. Manuscript.
OpenAI, accompanying Lean statement. Pinned source.

2 thms1 active userReviewed

Group Theory·Captain: wurtle

Quasi-isometric recognition of virtually polycyclic groupsResearch Paper

Motivation: recognizing a group from its large-scale geometry

Geometric group theory studies finitely generated groups through their word metrics, which are well defined up to quasi-isometry. A basic question is which algebraic properties are quasi-isometry invariants: if a group $H$ "looks like" a group $P$ from far away, must $H$ share $P$ 's algebraic structure? Gromov's polynomial-growth theorem (1981) answers this for virtually nilpotent groups. The next natural class is the virtually polycyclic groups — groups with a finite-index subgroup admitting a finite subnormal series with cyclic factors — which are exactly, up to finite index, the lattices in connected simply connected solvable Lie groups. Eskin, Fisher and Whyte conjectured that this class is quasi-isometrically rigid, and the question had been settled only for special families such as $\mathrm{Sol}$ and certain abelian-by-abelian groups.

Background

1981 — Gromov: groups of polynomial growth are virtually nilpotent, which settles the virtually nilpotent case (Publ. IHÉS 1981).
2000 — Farb and Mosher pose horizontal-preservation and recognition problems for solvable groups (arXiv:math/0005184).
2004 — Shalom proves that a finitely generated group quasi-isometric to an infinite polycyclic group has a finite-index subgroup with infinite abelianization (Acta Math. 2004).
2007 — Eskin, Fisher and Whyte formulate the lattice-recognition conjecture and its polycyclic form (Conjecture 1.2) (PAMQ 2007).
2010–2013 — Dymarz treats certain diagonalizable models (GAFA 2010); Peng handles nondegenerate unimodular split abelian-by-abelian Lie groups (G&T 2011); Eskin–Fisher–Whyte prove recognition for $\mathrm{Sol}$ by coarse differentiation (Ann. of Math. 2013).
2025 — Dymarz, Fisher and Xie prove a Tukia-type theorem and rigidity for SOL-like groups (Adv. Math. 2025); Le Boudec proves recognition under commability (arXiv:2510.24581); Grayevsky and Pallier treat $\mathrm{Sol}_5$ (arXiv:2509.12823).
2026 — An OpenAI preprint, Quasi-isometric recognition of virtually polycyclic groups (OpenAI Math Release, September 24, 2026), claims recognition for the full class. The preprint has not been peer reviewed and its theorems are not formally verified.

Setting

For finitely generated groups $P,H$ with word metrics, a $(K,C)$ -quasi-isometry $F:P\to H$ satisfies $K^{-1}d(x,x')-C\le d(Fx,Fx')\le Kd(x,x')+C$ and has $C$ -dense image. For finitely generated groups this is equivalent to a coarse equivalence: maps $f:P\to H$ , $g:H\to P$ sending pairs at bounded distance (differences in a fixed finite set) to pairs at bounded distance, with $g\circ f$ and $f\circ g$ at bounded distance from the identities. A uniform lattice in a locally compact group $S$ is a discrete subgroup $\Lambda$ with $S=\Lambda K$ for a compact $K$ ; a lattice is a discrete subgroup whose coset space carries an $S$ -invariant probability measure.

For the height theorem: a connected simply connected Lie group $G$ is real-triangulable if the adjoint representation of its Lie algebra $\mathfrak g$ is simultaneously upper triangular in some real basis, with diagonal characters $\chi_1,\dots,\chi_s$ . Put $\mathfrak k=\bigcap_j\ker\chi_j$ and $W=\mathfrak g/\mathfrak k$ ; the exponential height map $\pi:G\to(W,+)$ is the homomorphism whose differential is the quotient map. $G$ is unimodular if its left Haar measure is right invariant.

Formalization targets

Milestone: uniform bounded height (Theorem 1.4)

Let $G$ be connected, simply connected, real-triangulable and unimodular, with a proper left-invariant metric and a norm on $W$ . There is a finite subgroup $\mathcal A_G\le\mathrm{GL}(W)$ such that for all $K\ge1$ , $C\ge0$ there is $B$ with: every $(K,C)$ self quasi-isometry $F$ of $G$ has some $A_F\in\mathcal A_G$ with

\bigl\|\pi F(g)-\pi F(1)-A_F\,\pi(g)\bigr\|\le B\qquad(g\in G).

Milestone: lattice recognition (Corollary 1.2)

If a finitely generated group $H$ is quasi-isometric to a lattice in a connected simply connected solvable Lie group, then a finite-index subgroup of $H$ is a uniform lattice in some (possibly different) connected simply connected solvable Lie group.

Goal: quasi-isometric recognition (Theorem 1.1)

Let $P$ be finitely generated and virtually polycyclic and $H$ finitely generated. If $H$ is quasi-isometric to $P$ , then

H\ \text{is virtually polycyclic},\quad\text{and some finite-index } \Gamma\le H \text{ is isomorphic to a uniform lattice in a connected simply connected solvable Lie group.}

The second clause is the classical lattice realization of virtually polycyclic groups (Dekimpe's theorem, used in the source's proof of Corollary 1.2), recorded in the same formal statement. All three statements are published on the platform with status Open: no machine-checked proofs exist yet.

Significance

The result itself. Virtual polycyclicity becomes a quasi-isometry invariant among finitely generated groups, extending Gromov's theorem from nilpotent to solvable lattices and resolving the Eskin–Fisher–Whyte conjecture in its lattice form, where the ambient Lie group may change. The bounded-height theorem is a rigidity statement for quasi-isometries of an entire class of solvable Lie groups: up to bounded error and a finite group of linear symmetries, every quasi-isometry preserves height. This is the kind of control that previously required case-by-case coarse differentiation.

Formalizing it. The proof combines Lie theory, measured couplings, reduced cohomology, volume growth, Gromov's theorem and finiteness/duality results for elementary amenable groups — a long chain in which a machine check would add real confidence. Basic objects (coarse equivalences of groups, polycyclic series, uniform lattices, Lie groups with exponential maps) are reusable across geometric group theory.

Difficulty

Quasi-isometries carry no algebraic structure and can be wild at bounded scales, so the comparison group $H$ cannot be assumed solvable or even amenable a priori. Shalom's argument yields only a nontrivial homomorphism to $\mathbb Z$ , not full structure. The geometric core is height rigidity: one must show that a quasi-isometry cannot mix "up" and "down" directions of different exponential rates, uniformly over all quasi-isometries with given constants, and with a bounded (not merely sublinear) error, which is exactly what the later group-theoretic deduction needs.

Formalization scope

Polycyclicity is encoded by an explicit finite cyclic subnormal series; virtual polycyclicity by a finite-index polycyclic subgroup. Quasi-isometry of finitely generated groups is encoded as GroupCoarseEquivalence, with bornologous maps and errors in finite sets — equivalent to quasi-isometry of word metrics.
Simply connected solvable Lie groups are bundled as SimplyConnectedSolvableLieModel (finite-dimensional charted Lie group, Hausdorff, second countable, simply connected, solvable). Uniform lattices are discrete subgroups with a compact fundamental cover; finite-covolume lattices carry an invariant probability measure on the coset space.
In the height theorem, real-triangulability is a TriangularAdjoint basis, $W$ is any normed space linearly isomorphic to the canonical quotient, and $\pi$ is characterized through an exponential map. The metric is any compatible proper left-invariant metric with linear chain bounds — a quasi-isometric generalization of the source's fixed left-invariant Riemannian metric. The finite group $\mathcal A$ is chosen before $K,C$ .
Needed infrastructure: Lie algebras of Lie groups and exponential maps, Haar measure, quasi-isometries, Gromov's theorem, and the theory of elementary amenable groups.

Selected references

M. Gromov, Groups of polynomial growth and expanding maps, Publ. Math. IHÉS 53 (1981), 53–78. https://doi.org/10.1007/BF02698687
Y. Shalom, Harmonic analysis, cohomology, and the large-scale geometry of amenable groups, Acta Math. 192 (2004), 119–185. https://doi.org/10.1007/BF02392739
A. Eskin, D. Fisher and K. Whyte, Quasi-isometries and rigidity of solvable groups, Pure Appl. Math. Q. 3 (2007), 927–947. https://doi.org/10.4310/PAMQ.2007.v3.n4.a3
A. Eskin, D. Fisher and K. Whyte, Coarse differentiation of quasi-isometries II: Rigidity for Sol and lamplighter groups, Ann. of Math. 177 (2013), 869–910. https://doi.org/10.4007/annals.2013.177.3.2
I. Peng, Coarse differentiation and quasi-isometries of a class of solvable Lie groups II, Geom. Topol. 15 (2011), 1927–1981. https://doi.org/10.2140/gt.2011.15.1927
T. Dymarz, Large scale geometry of certain solvable groups, Geom. Funct. Anal. 19 (2010), 1650–1687. https://doi.org/10.1007/s00039-010-0046-y
T. Dymarz, D. Fisher and X. Xie, A Tukia-type theorem for nilpotent Lie groups and quasi-isometric rigidity of solvable groups, Adv. Math. 468 (2025). https://doi.org/10.1016/j.aim.2025.110202
K. Dekimpe, Solvable Lie algebras, Lie groups and polynomial structures, Compos. Math. 121 (2000), 183–204. https://doi.org/10.1023/A:1001738932743
Y. Cornulier and R. Tessera, On the vanishing of reduced 1-cohomology for Banach representations, Ann. Inst. Fourier 70 (2020), 1951–2003. https://doi.org/10.5802/aif.3363
OpenAI, Quasi-isometric recognition of virtually polycyclic groups, OpenAI Math Release preprint, September 24, 2026 (source of the goal; Theorem 1.1 and Corollary 1.2, p. 2; Theorem 1.4, p. 4). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/quasi-isometric-recognition-of-virtually-polycyclic-groups-September-24-2026/paper.pdf

4 thms1 active userReviewed

Geometry & Topology

Missions

Smooth 4-dimensional Poincaré conjecture: foundations and reductionsOpen Problem

Motivation

Historical landmarks

Setting

Formalization targets

Main open goal

Structural and literature milestones

Topological two-disk gluing

Seam–interior smooth compatibility

Significance

Difficulty

Formalization scope

Selected references

Differential Geometry of Curves and Surfaces III: Global Properties of Plane CurvesTextbook

Motivation

Setting

Formalization targets

Goal — Four-vertex theorem (do Carmo, Theorem 2, p. 37)

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

A torsion-free hyperbolic group that is not residually finiteOpen Problem

Motivation

Setting

Formalization targets

Significance

Difficulty

Formalization scope

Selected references

Differential Geometry of Curves and Surfaces IV: Regular Surfaces and Change of ParametersTextbook

Motivation

Setting

Formalization targets

Goal — Change of parameters (do Carmo §2-3, Proposition 1)

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

Differential Geometry of Curves and Surfaces II: Theorema EgregiumTextbook

Motivation

Setting

Formalization targets

Goal — Theorema Egregium (do Carmo, p. 237)

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

Differential Geometry of Curves and Surfaces I: Fundamental Theorem of the Local Theory of CurvesTextbook

Motivation

Setting

Formalization targets

Goal — Fundamental theorem of the local theory of curves (do Carmo, p. 19)

Supporting statements

Significance

Difficulty

Formalization scope

Selected references

Faithfulness of the Burau representation of B4Research Paper

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Strong Whitney embedding in dimension 2nResearch Paper

Motivation: an intrinsic manifold in a fixed Euclidean space

Setting: topology, smoothness, and the differential

Formalization target: the single root theorem

Significance: the full theorem rather than an easier restriction

Difficulty: the dimension bound and the noncompact scope

Formalization scope: unchanged Mathlib predicates

Selected references

Thurston's Question 23: rational relations among hyperbolic volumesOpen Problem

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

Milestone — Lefschetz $(1,1)$