Geometry & Topology

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.

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.

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:

1. $x$ is differentiable, i.e. of class $C^\infty$ on $U$;
2. $x$ is a homeomorphism of $U$ onto $V \cap S$ — it is injective and its inverse is continuous;
3. (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).

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.

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.

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

1. $\det_{\mathbb C} C_A \neq 0$ for every $A \in \mathrm{Sp}(2n)$.
2. $\deg(\hat\rho^2\circ\tilde\psi)$ exists and does not depend on the extension $\tilde\psi$.
3. $\deg(\hat\rho\circ\varphi)$ is well defined for loops.
4. Naturality. $\mu_{CZ}(\varphi\psi\varphi^{-1}) = \mu_{CZ}(\psi)$ for every path $\varphi$ in $\mathrm{Sp}(2n)$.
5. Homotopy, for $\mu_{CZ}$.
6. Zero. If $\psi(s)$ has no eigenvalue on the unit circle for $s > 0$, then $\mu_{CZ}(\psi) = 0$.
7. 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''))$.
8. Loop, for $\mu_{CZ}$.
9. Signature, for $\mu_{CZ}$.
10. Determinant. $(-1)^{n-\mu_{CZ}(\psi)} = \operatorname{sign}\det(\mathrm{Id} - \psi(1))$.
11. Inverse. $\mu_{CZ}(\psi^{-1}) = \mu_{CZ}(\psi^{\mathsf T}) = -\mu_{CZ}(\psi)$.
12. 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)

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.

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.

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

1. Faithful. A gauge arrow between two connections is determined by its value at $x$.
2. Full. Every conjugation relating the holonomy maps of $A$ and $B$ is realized by a gauge transformation.
3. Barrett reconstruction. Every holonomy map at $x$ equals $\mathrm{hol}_A$ on all loops at $x$, for some connection $A$.
4. 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.
5. 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).
6. 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.
7. 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

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

1. 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$.
2. Faithful iff $H^0 = 0$.
3. Full iff $H^1 = 0$.
4. Essentially surjective iff $H^2 = 0$.
5. 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.
6. 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

Motivation

A contact structure on a manifold of odd dimension $2k+1$ is a field of hyperplanes $\xi=\ker\alpha$ that is as far from integrable as possible. Contact structures are the odd-dimensional counterpart of symplectic forms. They arise on every star-shaped energy level of a Hamiltonian system, on unit cotangent bundles (geodesic flows), and on links of singularities. They are the setting of Reeb dynamics and of the Weinstein conjecture.

Gray's stability theorem says that on a closed manifold contact structures have no local moduli. If $\xi_t$, $t\in[0,1]$, is a smooth family of contact structures, there is an isotopy $\psi_t$ with $T\psi_t(\xi_0)=\xi_t$. A contact structure can therefore be deformed only within its isotopy class, and every classification of contact structures (tight versus overtwisted, Eliashberg's classification on $S^3$) is a classification up to isotopy because of it.

Timeline.

• 1959. Gray proves stability with deformation theory in the style of Kodaira–Spencer (Ann. of Math. 69).
• 1965. Moser proves the analogous stability for volume forms by integrating a time-dependent vector field, now called the Moser trick (Trans. AMS 120).
• Later. The Moser trick becomes the standard proof of Gray's theorem. Geiges' survey gives a short complete proof (arXiv:math/0307242, Theorem 2.20), which is the source of this mission. Its remarks record the limits of the statement: contact forms are not stable (Remark 2.21(1)), and on the open manifold $S^1\times\mathbb{R}^2$ stability fails (Remark 2.21(2), after Eliashberg).

Setting

The closed manifold is a compact submanifold of Euclidean space. Let $F:\mathbb{R}^n\to\mathbb{R}^c$ be smooth, let $M=F^{-1}(0)$ be compact, and assume $DF(y)$ is surjective for every $y\in M$. Then $M$ is a closed smooth manifold of dimension $n-c$ with tangent spaces

$$T_yM=\ker DF(y).$$

A one-form is a smooth map $\alpha:\mathbb{R}^n\to(\mathbb{R}^n)^*$, restricted to $TM$. Its exterior derivative is

$$d\alpha_y(u,v)=D\alpha_y(u)(v)-D\alpha_y(v)(u).$$

• Contact form. $\alpha$ is a contact form on $M$ if at every $y\in M$ the covector $\alpha_y$ is nonzero on $T_yM$ and $d\alpha_y$ is non-degenerate on the hyperplane

$$\xi_y=T_yM\cap\ker\alpha_y.$$

This is the condition $\alpha\wedge(d\alpha)^k\neq0$ in the form of Geiges' Remark 2.3. It forces $\dim M$ to be odd. The contact structure is $\xi=\ker\alpha$. Contact structures are cooriented throughout, as in Geiges' standing assumption (§2).

• Smooth family. A family $\alpha_t$ is smooth if $(t,y)\mapsto\alpha_t(y)$ is smooth. It is a family of contact forms if each $\alpha_t$, $t\in[0,1]$, is a contact form on $M$.
• Isotopy. An isotopy of $M$ is a smooth map $(t,y)\mapsto\psi_t(y)$ with $\psi_0=\mathrm{id}$ on $M$, such that each $\psi_t$, $t\in[0,1]$, maps $M$ bijectively onto $M$ with injective differential on $TM$, i.e. is a diffeomorphism of $M$.
• Pull-back. $(\psi_t^*\alpha)_y(v)=\alpha_{\psi_t(y)}(D\psi_t(y)\,v)$.

Formalization targets

Goal: Gray stability (Theorem 2.20)

For every smooth family of contact forms $\alpha_t$, $t\in[0,1]$, on $M$ there is an isotopy $\psi_t$ of $M$ with

$$T\psi_t(\xi_0)=\xi_t\qquad(t\in[0,1]),\qquad\xi_t=\ker\alpha_t,$$

stated pointwise: for $v\in T_yM$, $\alpha_0(v)=0$ iff $\alpha_t(D\psi_t(y)v)=0$.

The goal concerns the contact structures. It fixes no normalization of the forms and no dimension.

Stronger: conformal form

The same isotopy can be chosen with smooth functions $\lambda_t>0$ such that

$$\psi_t^*\alpha_t=\lambda_t\,\alpha_0\quad\text{on }TM.$$

Stronger: stationary points (Remark 2.21(3))

Moreover, every point $p\in M$ at which $\dot\alpha_t$ vanishes on $T_pM$ for all $t$ stays fixed: $\psi_t(p)=p$.

Significance

The result. Gray stability is the basic rigidity statement of contact topology.

• It reduces the classification of contact structures to isotopy classes, so invariants of a contact manifold are constant along deformations.
• It is the first step of many local normal forms: Darboux's theorem and the neighbourhood theorems for Legendrian and transverse submanifolds are proved by applying it, or its proof, near a submanifold (Geiges §2.4–2.5).
• In Hamiltonian dynamics it identifies the contact structures of a continuous family of star-shaped energy levels. Topological invariants of transverse periodic orbits, such as the self-linking number, are then constant along the family.

Formalizing it. The theorem is classical and has a short proof on paper. Mathlib, at the revision used here, has no differential forms on manifolds, no Lie derivative, no global flows of time-dependent vector fields on compact submanifolds, and no contact structures. The mission builds these concretely on submanifolds of $\mathbb{R}^n$:

• one-forms, their exterior derivative and pull-back;
• the derivative of a pulled-back family along a flow (Lemma 2.19);
• the pointwise linear algebra of a contact form: the Reeb vector, and the unique solution of the Moser equation;
• global flows of smooth time-dependent vector fields tangent to a compact submanifold.

All of these are reusable for Moser's theorem on volume and symplectic forms and for the Darboux and neighbourhood theorems.

Difficulty

The proof is soft, but two steps are not formal.

1. Solving for the vector field. Writing $\psi_t$ as the flow of $X_t$, the equation $\psi_t^*\alpha_t=\lambda_t\alpha_0$ becomes

$$\dot\alpha_t+i_{X_t}d\alpha_t=\mu_t\alpha_t,\qquad X_t\in\xi_t.$$

It has a unique solution at each point, but only because $d\alpha_t$ is non-degenerate on $\xi_t$ and the Reeb vector spans the kernel of $d\alpha_t|_{TM}$. The solution must also depend smoothly on $(t,y)$ and be tangent to $M$; the ambient form $\alpha_t$ is in general not contact off $M$. 2. Integrating it. The isotopy is the flow of $X_t$, which must exist for all $t\in[0,1]$ and stay on $M$. Compactness of $M$ enters exactly here. On open manifolds the statement is false (Remark 2.21(2)).

The tempting shortcut of asking for $\psi_t^*\alpha_t=\alpha_0$ does not work. Contact forms themselves are not stable, as the Hopf family on $S^3$ shows (Remark 2.21(1)), and the conformal factor $\lambda_t$ cannot be dropped.

Formalization scope

• Representation.
  • $\mathbb{R}^n$ is Fin n → ℝ; $M$ is a compact regular level set $F^{-1}(0)$ of a smooth $F:\mathbb{R}^n\to\mathbb{R}^c$.
  • One-forms are maps $\mathbb{R}^n\to(\mathbb{R}^n\to_L\mathbb{R})$, smooth families are jointly smooth in $(t,y)$ on $\mathbb{R}\times\mathbb{R}^n$, and $d\alpha$ is the antisymmetrized derivative.
  • An isotopy is a jointly smooth $\psi:\mathbb{R}\times\mathbb{R}^n\to\mathbb{R}^n$ that restricts, for $t\in[0,1]$, to diffeomorphisms of $M$.
• Committed conventions.
  • Contact structures are cooriented, i.e. given by global contact forms.
  • The contact condition is the non-degeneracy of $d\alpha$ on $\xi$ (Remark 2.3), not a wedge power.
  • Only the restrictions to $TM$ and the values for $t\in[0,1]$ matter.
• Scope relative to the source. Every closed manifold embeds in some $\mathbb{R}^n$, but not every closed manifold is a regular level set, since that requires a trivial normal bundle. The targets cover regular level sets, including all spheres and all star-shaped energy levels. The abstract version on any closed manifold is outside the targets until Mathlib has differential forms on manifolds.
• Ruling out vacuous encodings. The isotopy must start at the identity on $M$, map $M$ onto $M$ for every $t\in[0,1]$, and be a diffeomorphism there. Dropping any of these makes the goal trivial; for instance, the constant isotopy satisfies the goal whenever all $\xi_t$ agree. The Hopf family milestone checks that the contact condition is satisfiable and that the conformal factor is necessary.
• Contributions welcome. The linear-algebra milestones (Reeb vector, Moser equation), Lemma 2.19, global flows on compact level sets, and the Hopf-family example. Moser's theorem for volume forms would be a natural sibling result built on the same infrastructure.

Selected references

• J. W. Gray, Some global properties of contact structures, Ann. of Math. 69 (1959), 421–450. https://doi.org/10.2307/1970192
• H. Geiges, Contact geometry, in Handbook of Differential Geometry, Vol. II, Elsevier (2006), 315–382; §2.2, Lemma 2.19, Theorem 2.20, Remark 2.21. https://arxiv.org/abs/math/0307242
• H. Geiges, An Introduction to Contact Topology, Cambridge Stud. Adv. Math. 109, Cambridge Univ. Press (2008), §2.2. https://doi.org/10.1017/CBO9780511611438
• J. Moser, On the volume elements on a manifold, Trans. Amer. Math. Soc. 120 (1965), 286–294. https://doi.org/10.1090/S0002-9947-1965-0182927-5
• Y. Eliashberg, Contact 3-manifolds twenty years since J. Martinet's work, Ann. Inst. Fourier 42 (1992), 165–192. https://doi.org/10.5802/aif.1288