Differential Geometry

Motivation

General relativity predicts that a black hole, once it has settled down after collapse, retains almost no memory of the matter that formed it. The no-hair theorem, also called the black hole uniqueness theorem, states that all stationary black-hole solutions of the Einstein–Maxwell equations are completely characterized by three externally observable parameters: mass, angular momentum and electric charge; all other information ("hair") disappears behind the event horizon. The phrase "black holes have no hair" was popularized by John Archibald Wheeler. Its observational content is tested in gravitational-wave ringdown signals and in black-hole imaging.

Despite its name, there is no rigorous proof of the general statement: mathematicians refer to it as the no-hair conjecture.

Timeline.

• 1967 — W. Israel proves uniqueness of the Schwarzschild metric among static vacuum black holes (Phys. Rev. 164, 1776).
• 1968 — Israel extends this to static electrovacuum black holes, obtaining Reissner–Nordström (Commun. Math. Phys. 8, 245).
• 1971 — B. Carter shows that an axisymmetric vacuum black hole has only two degrees of freedom (Phys. Rev. Lett. 26, 331); D. C. Robinson later completes uniqueness of Kerr.
• 1970s — S. Hawking's rigidity theorem, combined with Carter and Robinson, yields uniqueness of Kerr in vacuum under the additional hypotheses of non-degenerate horizons and real analyticity of spacetime.
• 2007 — extension to positive cosmological constant (Bhattacharya–Lahiri, arXiv:gr-qc/0702006).

Counterexamples are known in dimensions above four, for non-abelian Yang–Mills fields and for some non-minimally coupled scalar fields; this mission concerns only the four-dimensional Einstein–Maxwell theory with zero cosmological constant.

Setting

A spacetime is a smooth 4-manifold $M$ with a Lorentzian metric $g$ of signature $(-,+,+,+)$, an electromagnetic field $F$ (a 2-form) and a time orientation $T$. The pair $(g,F)$ is electrovacuum if, in geometrized Gaussian units,

$$G_{\mu\nu}=2\Big(F_{\mu\alpha}F_\nu{}^\alpha-\tfrac14g_{\mu\nu}F_{\alpha\beta}F^{\alpha\beta}\Big),\qquad\nabla_\mu F^{\mu\nu}=0,\qquad dF=0 .$$

The spacetime is stationary if a one-parameter group $\varphi_t$ of isometries preserves $F$, and it has a stationary asymptotically flat end $M_{\rm ext}$ if coordinates $(t,\vec x)$, $|\vec x|>R$, cover an open set on which $\varphi_t$ is the time translation and $g_{\mu\nu}-\eta_{\mu\nu}=O(1/|\vec x|)$, $\partial g=O(1/|\vec x|^2)$, $F=O(1/|\vec x|^2)$.

With $I^\pm$ the chronological future and past, the domain of outer communications is $\langle\langle M_{\rm ext}\rangle\rangle=I^+(M_{\rm ext})\cap I^-(M_{\rm ext})$, the black-hole region is $M\setminus I^-(M_{\rm ext})$ and the future event horizon is $\partial I^-(M_{\rm ext})$.

The Kerr–Newman family, in Kerr–Schild coordinates, is $g^{KN}=\eta+f\,k\otimes k$ with

$$f=\frac{r^2(2mr-e^2)}{r^4+a^2z^2},\qquad k=\Big(1,\frac{rx+ay}{r^2+a^2},\frac{ry-ax}{r^2+a^2},\frac zr\Big),\qquad \frac{x^2+y^2}{r^2+a^2}+\frac{z^2}{r^2}=1,$$

with potential $A=\frac{er^3}{r^4+a^2z^2}k$. For $m>0$, $a^2+e^2\le m^2$ its domain of outer communications is $\{r>r_+\}$, $r_+=m+\sqrt{m^2-a^2-e^2}$.

Formalization targets

Goal: the no-hair conjecture

Under the standing hypotheses (smooth electrovacuum, stationary, asymptotically flat end, globally hyperbolic $\langle\langle M_{\rm ext}\rangle\rangle$, nonempty black-hole region, connected event horizon), there are $m>0$, $a$, $e$ with $a^2+e^2\le m^2$, an angle $\beta$ and a diffeomorphism $\Psi$ with

$$\Psi:\{r>r_+\}\xrightarrow{\cong}\langle\langle M_{\rm ext}\rangle\rangle,\qquad\Psi^*g=g^{KN}_{m,a,e},\qquad\Psi^*F=\cos\beta\,F^{KN}+\sin\beta\,\star F^{KN}.$$

Milestones

1. The Kerr–Newman metric solves the Einstein–Maxwell equations where $r>0$.
2. Kerr–Newman black holes satisfy the standing hypotheses (the goal is not vacuous).
3. Israel 1967: static vacuum $\Rightarrow$ Schwarzschild ($a=e=0$).
4. Israel 1968: static electrovacuum $\Rightarrow$ Reissner–Nordström ($a=0$).
5. Carter 1971 / Robinson: axisymmetric vacuum $\Rightarrow$ Kerr ($e=0$).
6. Hawking–Carter–Robinson: analytic vacuum with non-degenerate horizon $\Rightarrow$ Kerr.
7. Frame normalization: a Lorentz boost takes a timelike 4-momentum to rest, $\Lambda P=(\sqrt{-P^2},0,0,0)$.
8. Frame normalization: a rotation aligns the spin, $RJ=(0,0,|J|)$.

Significance

A proof of the goal would establish that the Kerr–Newman metrics exhaust the stationary, asymptotically flat electrovacuum black holes with connected horizon, which is the mathematical basis for treating astrophysical black holes as described by three numbers. It would also remove the analyticity and non-degeneracy hypotheses from the known vacuum results.

No machine-checked proof of any statement in this mission is known. Milestones 1, 7 and 8 are classical computations; milestones 3–6 are published theorems whose proofs rely on substantial Lorentzian geometry and elliptic PDE; the goal is open.

Difficulty

Uniqueness proofs reduce the problem to an elliptic boundary-value problem on the orbit space once enough symmetry is available. In the general stationary case the extra axial symmetry is not known to exist: Hawking's rigidity argument produces it only for analytic metrics, because it extends a Killing field off the horizon by analytic continuation. Without analyticity, unique continuation for the Killing equation across the horizon is the obstruction. Degenerate (extremal) horizons further break arguments that rely on a bifurcation surface.

Formalization scope

Spacetimes are Mathlib smooth manifolds modelled on EuclideanSpace ℝ (Fin 4); the metric and field are fields of continuous bilinear forms on tangent spaces, and curvature and field equations are imposed through components in every chart. Causal sets use $C^1$ curves parametrized by $[0,1]$. The Kerr–Newman comparison spacetime is the region $\{r>r_+\}$ of Kerr–Schild coordinate space with the explicit metric. Magnetic charge is accommodated by the duality angle $\beta$.

The hypotheses are not vacuous: milestone 2 asserts that every Kerr–Newman black hole satisfies them. The connected-horizon hypothesis excludes the static multi-black-hole Majumdar–Papapetrou solutions, which would otherwise contradict the goal.

Needed infrastructure: Levi-Civita connection and curvature on manifolds, causal theory (global hyperbolicity, Cauchy surfaces), Killing fields and their flows, and the elliptic theory of harmonic maps used in uniqueness proofs. Contributions on any of these, and on milestones 1, 7 and 8, are welcome.

Selected references

• Wikipedia, No-hair theorem, revision 1353599195, https://en.wikipedia.org/w/index.php?title=No-hair_theorem&oldid=1353599195
• W. Israel, Event Horizons in Static Vacuum Space-Times, Phys. Rev. 164 (1967) 1776, https://doi.org/10.1103/PhysRev.164.1776
• W. Israel, Event horizons in static electrovac space-times, Commun. Math. Phys. 8 (1968) 245, https://doi.org/10.1007/BF01645859
• B. Carter, Axisymmetric Black Hole Has Only Two Degrees of Freedom, Phys. Rev. Lett. 26 (1971) 331, https://doi.org/10.1103/PhysRevLett.26.331
• S. Bhattacharya, A. Lahiri, No hair theorems for positive Λ, Phys. Rev. Lett. 99 (2007) 201101, https://arxiv.org/abs/gr-qc/0702006

Motivation

Mirror symmetry was discovered in string theory as a duality between families of Calabi–Yau manifolds, and it entered mathematics as a prediction: the generating function counting rational curves on one manifold equals a period integral of a mirror manifold. In his 1994 ICM address, Homological algebra of mirror symmetry (alg-geom/9411018), M. Kontsevich proposed that these numerical coincidences are shadows of an equivalence of categories: the symplectic geometry of $V$ should be encoded by Fukaya's $A_\infty$-category $F(V)$, whose objects are Lagrangian submanifolds and whose products count pseudo-holomorphic discs, and the complex geometry of the mirror $W$ by the derived category $D^b(\mathrm{Coh}\,W)$ of coherent sheaves. His Homological Mirror Conjecture asserts that the derived category built from $F(V)$ embeds as a full triangulated subcategory of $D^b(\mathrm{Coh}\,W)$.

Kontsevich states the conjecture "in slightly vague form", because Fukaya's construction was not, and still is not, available in the generality the statement needs. He therefore closes the paper with the one instance he can compute by hand, in the section Two-dimensional tori: a return: for the flat torus $\Sigma = \mathbb{R}^2/\mathbb{Z}^2$, the objects are closed geodesics with unitary local systems, the products $m_2$ are sums over triangles in the universal cover weighted by $\exp(-\text{area})$, and their structure constants are values of the classical theta-function. He predicts an equivalence with $D^b(\mathrm{Coh}\,E)$ for an elliptic curve $E$. This instance was proved by A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve (math/9801119). Later instances include the four-torus (Abouzaid–Smith, arXiv:0903.3065) and Calabi–Yau hypersurfaces (Sheridan, arXiv:1111.0632). None of this has been formalized.

Setting

Fix a real number $\mathrm{area} > 0$, and let $\Sigma$ be the torus $\mathbb{R}^2/\mathbb{Z}^2$ carrying the translation-invariant symplectic form of total area $\mathrm{area}$; a region of Euclidean area $a$ in coordinates has symplectic area $\mathrm{area}\cdot a$.

A brane $b$ consists of: a primitive vector $v \in \mathbb{Z}^2$ and a point $c \in \mathbb{R}^2$, which together determine the closed geodesic $L_b = \{\,c + tv \bmod \mathbb{Z}^2\,\}$; a grading $\alpha \in \mathbb{R}$, a real lift of the direction angle normalized so that $(\cos \pi\alpha, \sin \pi\alpha)$ is parallel to $v$; and a real constant $\theta$ describing a flat unitary line bundle on $L_b$, whose parallel transport along a path of parameter length $s$ is $\exp(2\pi i\,\theta s)$. Two branes are transverse when $\det(v_1, v_2) \neq 0$; their geodesics then meet in the finite set $L_{b_1} \cap L_{b_2}$, which indexes a basis of the Floer space $\mathrm{Hom}(b_1, b_2)$. All of this space sits in a single degree, the Maslov index

$$\mu(b_1, b_2) \;=\; \lceil \alpha_2 - \alpha_1 \rceil .$$

For three pairwise transverse branes and intersection points $p \in L_1 \cap L_2$, $q \in L_2 \cap L_3$, $r \in L_1 \cap L_3$, a triangle is a triple of lifts $(P, Q, R) \in (\mathbb{R}^2)^3$ of $(p,q,r)$ with $Q - P$ parallel to $v_2$, $R - Q$ parallel to $v_3$, $P - R$ parallel to $v_1$, and positively oriented. Kontsevich's structure constant is

$$c(p,q,r) \;=\; \sum_{\text{triangles}} \exp\bigl(-\text{symplectic area}\bigr)\cdot \bigl(\text{holonomies along the three sides}\bigr),$$

the coefficient of $r$ in $m_2(p, q)$. On the complex side, $D^b_{\mathrm{coh}}(E)$ denotes the complexes of $\mathcal{O}_E$-modules with bounded, coherent cohomology.

Formalization targets

Goal — homological mirror symmetry for the two-torus

For every $\mathrm{area} > 0$ there exist a smooth proper curve $E$ over $\mathbb{C}$, an assignment $b \mapsto \Phi(b)$ of an object of $D^b_{\mathrm{coh}}(E)$ to each brane, and isomorphisms

$$\mathbb{C}^{\,L_{b_1} \cap L_{b_2}} \;\xrightarrow{\ \sim\ }\; \mathrm{Hom}\bigl(\Phi(b_1),\, \Phi(b_2)[\mu(b_1,b_2)]\bigr) \qquad (b_1 \pitchfork b_2),$$

with $\mathrm{Hom}(\Phi(b_1), \Phi(b_2)[d]) = 0$ for $d \neq \mu(b_1,b_2)$, carrying the products $c(p,q,r)$ to composition in $D^b_{\mathrm{coh}}(E)$ whenever $\mu(b_1,b_2) + \mu(b_2,b_3) = \mu(b_1,b_3)$.

Milestones

Existence of the Fukaya $A_\infty$-category of the torus; finiteness of $L_{b_1} \cap L_{b_2}$ with $|\det(v_1,v_2)|$ points; the Maslov relation $\mu(b_1,b_2) + \mu(b_2,b_1) = 1$; $m_1^2 = 0$ together with associativity of $m_2$ up to coboundary; the degeneration of an $A_\infty$-category with $m_{\geq 3} = 0$ to a differential graded category; the theta-function shape of the structure constants; and their associativity equation.

Significance

The conjecture reorganizes mirror symmetry: the numerical predictions compare two elements of an uncountable set of power series, whereas the homological statement compares two objects in a countable set of triangulated categories, and the numerical statements are meant to follow from it. The torus case is the smallest instance in which every ingredient — Lagrangian branes, Maslov grading, disc counts, theta functions, and coherent sheaves on an elliptic curve — is present and computable, so it is the natural first target.

What this mission adds beyond the literature is machine-checked mathematics where none exists. Mathlib currently has no symplectic manifolds, no Lagrangian Floer theory, no Fukaya categories, and no $A_\infty$-categories; it does have schemes, sheaves of modules, and derived categories of abelian categories. The mission supplies the missing $A_\infty$ layer and the torus model, and asks for the comparison theorem. The $A_\infty$ definitions, the derived category with coherent cohomology, and the theta-function estimates are reusable outside this mission.

Difficulty

The obvious route — "transport the Polishchuk–Zaslow proof" — stalls at the point where the two sides are compared. Establishing that the triangle sums converge and equal theta-function values is analysis that Mathlib supports; producing an elliptic curve as a scheme with prescribed parameter, computing $\mathrm{Ext}$-groups between the mirror sheaves, and matching all products simultaneously is not currently supported by any library. A second difficulty is bookkeeping: gradings, Maslov indices and shifts must line up, since the product of two morphisms is nonzero only when $\mu(b_1,b_2)+\mu(b_2,b_3) = \mu(b_1,b_3)$, and the same numerical condition controls which triples of branes bound triangles at all.

Formalization scope

Conventions committed to in Lean. An $A_\infty$-category is encoded as a single graded module $A$ with morphism components $\hom(X,Y)$ and products given by a map on lists, $m[f_1,\dots,f_n] = m_n(f_1 \otimes \cdots \otimes f_n)$ of degree $2-n$, with $m_0 = 0$, and Stasheff signs $(-1)^{r+st}$ in the bar-construction normalization; $m_2(f,g)$ is "$f$ then $g$". Triangles are normalized by requiring the first vertex to lie in $[0,1)^2$, which picks exactly one representative in each $\mathbb{Z}^2$-orbit; only positively oriented triangles are counted; sums are tsums, so convergence is part of the work. The hom-space isomorphisms in the goal are required to be additive, not a priori $\mathbb{C}$-linear, because the derived category of $\mathcal{O}_E$-modules is not equipped with a $\mathbb{C}$-linear structure in Mathlib; the required compatibility with the structure constants pins down the algebra anyway. The goal asks only for the existence of a smooth proper curve $E$ over $\mathbb{C}$; the paper's further prediction that $E$ has parameter $\exp(-\mathrm{area})$ is deliberately left out of the statement.

The goal is not trivially satisfiable: the intersection set of two transverse branes is nonempty, so the required isomorphisms force the corresponding $\mathrm{Hom}$-groups to be nonzero of the right size, in the right degree, with the prescribed products.

The general conjecture, for an arbitrary symplectic manifold with $c_1 = 0$, is not stated here, and deliberately so: without symplectic manifolds and Floer theory in Mathlib, any general statement would have to take the Fukaya category as an unconstrained parameter, which would make it either vacuous or false. Building that infrastructure — symplectic manifolds, graded Lagrangian branes, Floer cohomology, twisted complexes over an $A_\infty$-category and their triangulated structure — is the natural way to extend this mission, and such contributions are welcome.

Selected references

• M. Kontsevich, Homological algebra of mirror symmetry, Proceedings of the International Congress of Mathematicians (Zürich, 1994), alg-geom/9411018.
• A. Polishchuk and E. Zaslow, Categorical mirror symmetry: the elliptic curve, Adv. Theor. Math. Phys. 2 (1998), math/9801119.
• M. Abouzaid and I. Smith, Homological mirror symmetry for the 4-torus, Duke Math. J. 152 (2010), arXiv:0903.3065.
• N. Sheridan, Homological mirror symmetry for Calabi–Yau hypersurfaces in projective space, Invent. Math. 199 (2015), arXiv:1111.0632.

Motivation: an intrinsic manifold in a fixed Euclidean space

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

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

Setting: topology, smoothness, and the differential

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

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

Formalization target: the single root theorem

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

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

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

Significance: the full theorem rather than an easier restriction

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

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

Difficulty: the dimension bound and the noncompact scope

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

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

Formalization scope: unchanged Mathlib predicates

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

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

Selected references

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

Motivation

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

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

Setting

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

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

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

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

Formalization targets

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

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

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

Significance

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

Motivation

Many optimization problems are posed over a manifold rather than a vector space: orthogonality constraints (the Stiefel manifold), unit-norm constraints (the sphere), fixed-rank matrices. In some of them the objective can only be evaluated, not differentiated. Black-box adversarial attacks on a neural network with a norm-constrained perturbation, hyperparameter tuning and simulation-based objectives are examples, and in all of them each function value is also noisy. Zeroth-order (derivative-free) methods replace the gradient by a random finite-difference estimate built from function values alone.

In Euclidean space the analysis of such methods is well developed. Nesterov and Spokoiny (2017) analysed Gaussian-smoothing estimators for deterministic objectives, and Ghadimi and Lan (2013) gave the first non-asymptotic stationarity rates for stochastic nonconvex objectives (the RSGF method). Li, Balasubramanian and Ma (arXiv:2003.11238, published in Mathematics of Operations Research, 2023) carried this programme to embedded submanifolds. They estimate the Riemannian gradient by projecting a Gaussian vector onto the tangent space and moving along a retraction, and they prove convergence rates for the resulting methods. This mission formalizes their rate for the stochastic method, ZO-RSGD (Theorem 3.2).

Setting

Let $E$ be a finite-dimensional real inner product space (the paper's $\mathbb R^n$), and let $\mathcal M \subseteq E$ be a $C^1$ embedded submanifold of dimension $d$. The tangent space $T_x\mathcal M$ at $x \in \mathcal M$ is the linear span of the tangent cone of $\mathcal M$ at $x$. For a submanifold this is the set of velocities $\gamma'(0)$ of curves in $\mathcal M$ through $x$, and it is a subspace of dimension $d$. $\mathcal M$ carries the metric induced by the inner product of $E$, and $P_x$ denotes the orthogonal projection of $E$ onto $T_x\mathcal M$.

A retraction is a map $R$, $(x, \eta) \mapsto R_x(\eta)$. For every $x \in \mathcal M$ it sends all of $T_x\mathcal M$ into $\mathcal M$ and is smooth on $T_x\mathcal M$, with $R_x(0) = x$ and differential the identity at $0$. The Riemannian gradient of a differentiable $f$ is $\operatorname{grad} f(x) = P_x \nabla f(x)$.

The objective is stochastic, $f(x) = \mathbb E_\xi F(x, \xi)$, with noise $\xi$ distributed according to a probability measure $P_\xi$. Two assumptions are imposed:

• Assumption 2.1 ($L$-retraction-smoothness). For almost every $\xi$, $|F(R_x(\eta),\xi) - F(x,\xi) - \langle \operatorname{grad}F(x,\xi), \eta\rangle| \le \frac L2\|\eta\|^2$ for all $x \in \mathcal M$ and $\eta \in T_x\mathcal M$.
• Assumption 2.3 (unbiased oracle, bounded variance). For every $x \in \mathcal M$, $\mathbb E_\xi F(x,\xi) = f(x)$, $\mathbb E_\xi \operatorname{grad}F(x,\xi) = \operatorname{grad}f(x)$ and $\mathbb E_\xi\|\operatorname{grad}F(x,\xi) - \operatorname{grad}f(x)\|^2 \le \sigma^2$.

Given a smoothing parameter $\mu > 0$ and a batch size $m$, draw $m$ independent pairs $(u_{0,i}, \xi_i)$, each with $u_{0,i} \sim \mathcal N(0, I)$ independent of $\xi_i \sim P_\xi$, and put $u_i = P_x u_{0,i}$. The mini-batch zeroth-order Riemannian gradient is

$$\bar g_{\mu,\xi}(x) = \frac1m\sum_{i=1}^m \frac{F(R_x(\mu u_i), \xi_i) - F(x, \xi_i)}{\mu}\,u_i .$$

ZO-RSGD (Algorithm 2) starts at $x_0 \in \mathcal M$ and iterates $x_{k+1} = R_{x_k}(-\hat\eta\,\bar g_{\mu,\xi}(x_k))$ with step $\hat\eta = 1/L$ and a fresh batch at every step. $x^*$ denotes a minimizer of $f$ over $\mathcal M$.

Formalization targets

Goal: Theorem 3.2

If $m \ge 16(d+4)$, then for every $N$

$$\frac{1}{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2 \le 4L\,\frac{f(x_0) - f(x^*)}{N+1} + 2\mu^2L^2(d+6)^3 + \frac{16(d+4)}{m}\sigma^2 .$$

The constants are the paper's own. The goal states the rate for every $\mu$, $m$ and $N$. It does not state the parameter choices $\mu = O(\epsilon/d^{3/2})$, $m = O(d\sigma^2/\epsilon^2)$, $N = O(1/\epsilon^2)$ that follow from it.

Milestones

• Lemma 2.1. For a $d$-dimensional subspace $\mathcal X$ with projection $P$, $u = Pu_0$ and $x \in \mathcal X$: $\mathbb E\langle x,u\rangle u = x$ and $\mathbb E\langle x,u\rangle^2 = \|x\|^2$.
• Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p \le (n+p)^{p/2}$ for a standard Gaussian $u$ on $\mathbb R^n$ and $p \ge 2$. This is already proved on the platform and is reused.
• Corollary 2.1. $\mathbb E\|Pu_0\|^p \le (d+p)^{p/2}$.
• Proposition 2.1(a). $\|\mathbb E\,g_\mu(x) - \operatorname{grad}f(x)\| \le \frac{\mu L}{2}(d+3)^{3/2}$ for the single-sample estimator $g_\mu$.
• Lemma 3.1. $\mathbb E\|\bar g_{\mu,\xi}(x) - \operatorname{grad}f(x)\|^2 \le \mu^2L^2(d+6)^3 + \frac{8(d+4)}{m}\sigma^2 + \frac{8(d+4)}{m}\|\operatorname{grad}f(x)\|^2$.

Significance

Theorem 3.2 is the basic complexity result for derivative-free stochastic optimization on manifolds. With the parameter choices of (3.10) it gives an $\epsilon$-stationary point in expectation after $O(d/\epsilon^4)$ noisy function evaluations. The dependence is on the manifold dimension $d$, not on the ambient dimension $n$. This matches the Euclidean rate of Ghadimi and Lan with $n$ replaced by $d$, and it is what makes projected-Gaussian estimators attractive when $d \ll n$ (for example, low-dimensional Stiefel manifolds embedded in large matrix spaces).

The results are proved in the paper (main text, p. 17, and Appendix C) but, to our knowledge, none of them has been machine-checked. The Euclidean Gaussian moment bound (Lemma 2.2) is formalized on the platform. The Euclidean RSGF results of Ghadimi and Lan are stated on the platform, and they are different statements: they use $x + \mu u$ instead of a retraction, the full space instead of a tangent space, and a random output index. A complete formalization would also produce reusable infrastructure: Gaussian identities for orthogonal projections, the projected-Gaussian moment bound, and a template for proving stationarity rates of random iterates on a product probability space.

Difficulty

The Euclidean argument relies on a smoothed function $f_\mu(x) = \mathbb E f(x + \mu u)$ whose gradient is exactly the mean of the estimator. That identity has no Riemannian analogue: $R_x(\mu u)$ is not a translate, so $\mathbb E\,g_\mu(x)$ is not the gradient of any smoothed function. The bias in Proposition 2.1(a) has to be bounded directly from Assumption 2.1, and this is why the estimator is only approximately unbiased.

The convergence proof needs a one-step descent inequality conditioned on the past. The direction at step $k$ is projected onto $T_{x_k}\mathcal M$, which depends on all earlier draws, so the conditional bound of Lemma 3.1 must be integrated against the product law of the batches. A naive reading that samples every direction from one fixed subspace, or that treats the iterates as deterministic, does not describe the algorithm. A further subtlety is that the gradient term of Lemma 3.1 must be absorbed by the descent of one step. This requires the batch to be large compared with the dimension, $m \ge 16(d+4)$.

Formalization scope

• $E$ is any finite-dimensional real inner product space with its Borel σ-algebra. The Gaussian is Mathlib's stdGaussian E.
• $\mathcal M$ and its dimension are given by the published ProjLikeRetr.Retractor.IsSubmanifold 1 d M (a $C^1$ coordinate-slice submanifold), so $d$ is tied to $\mathcal M$ and is never a free number. $T_x\mathcal M$ is the published ProjLikeRetr.Retractor.tangentSpace M x, never an arbitrary subspace.
• The retraction is defined on all of each tangent space, as the paper requires (Assumption 2.1 holds "for all $\eta \in T_x\mathcal M$, i.e., $\rho_x = \infty$"). The objective $f$ and the samples $F(\cdot,\xi)$ are assumed differentiable rather than smooth, which is all the gradient formula (2.3) uses.
• Added hypotheses. The goal assumes $m \ge 16(d+4)$. The paper's proof assumes it explicitly, but the theorem statement omits it. The goal also assumes that $(x,\eta) \mapsto R_x(\eta)$ and $x \mapsto P_x$ are measurable, so that the iterates are random variables; this holds for closed $\mathcal M$ such as spheres and Stiefel manifolds. Lemma 3.1 is stated for every $m \ge 1$. The paper's last proof step uses $m \ge 2$, but the bound holds for $m = 1$ as well.
• The iterates are defined for every $k$ on the sequence space of i.i.d. batches (the algorithm without a stopping index), so $x_{N+1}$ exists.
• No junk expectations. Every expectation of a nonnegative quantity is a lower Lebesgue integral compared with ENNReal.ofReal of the bound. Every vector-valued expectation comes with an integrability conclusion, and Assumption 2.3 carries the integrability of $F(x,\cdot)$ and $\operatorname{grad}F(x,\cdot)$. So no statement can hold because a Bochner integral defaulted to $0$.
• The $O(\cdot)$ parameter choices (3.10) and the oracle complexity $mN = O(d/\epsilon^4)$ are not formalized.
• The development needs projections of Gaussian measures onto subspaces, moments of Gaussian norms, conditional expectation along an i.i.d. sequence of batches, and telescoping. Proofs of any milestone are welcome, as are general lemmas about the push-forward of stdGaussian under an orthogonal projection.

Selected references

• J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023. Preprint arXiv:2003.11238v3. https://arxiv.org/abs/2003.11238
• Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17, 2017. https://doi.org/10.1007/s10208-015-9296-2
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23(4), 2013. https://arxiv.org/abs/1309.5549
• K. Balasubramanian, S. Ghadimi, Zeroth-Order Nonconvex Stochastic Optimization: Handling Constraints, High Dimensionality, and Saddle Points, Foundations of Computational Mathematics, 2022. https://arxiv.org/abs/1809.06474
• N. Boumal, P.-A. Absil, C. Cartis, Global Rates of Convergence for Nonconvex Optimization on Manifolds, IMA Journal of Numerical Analysis, 2019. https://arxiv.org/abs/1605.08101
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008.

Motivation

Many optimization problems in statistics and machine learning constrain the variable to a smooth manifold: orthonormal frames in sparse PCA and dictionary learning (the Stiefel manifold), unit vectors in phase retrieval (the sphere), fixed-rank matrices in matrix completion. Riemannian optimization handles these problems directly on the manifold. A step is taken in the tangent space and mapped back to the manifold by a retraction.

In several applications the objective can be evaluated but not differentiated: black-box adversarial attacks, simulation-based models, and hyperparameter or policy tuning. Zeroth-order (derivative-free) methods replace the gradient by an estimator built from function values. In Euclidean space the standard construction is Gaussian smoothing, analysed by Nesterov and Spokoiny (2017) and Ghadimi and Lan (2013). Li, Balasubramanian and Ma (arXiv:2003.11238; Mathematics of Operations Research, 2023) carry the construction over to embedded submanifolds. They sample a Gaussian vector, project it onto the tangent space, and use the retraction in place of the straight line $x+\mu u$. This mission formalizes their first optimization guarantee: the convergence rate of zeroth-order Riemannian gradient descent (ZO-RGD).

Setting

Let $E$ be a finite-dimensional real inner product space (the ambient $\mathbb R^n$). Let $M\subseteq E$ be a $C^1$ embedded submanifold of dimension $d$. At each $x\in M$ the tangent space $T_xM$ is a $d$-dimensional linear subspace of $E$; let $P_x$ denote the orthogonal projection onto it. $M$ carries the metric induced by the inner product of $E$.

A retraction is a map $(x,\eta)\mapsto R_x(\eta)$ such that, for every $x\in M$, $R_x$ is smooth on $T_xM$, maps $T_xM$ into $M$, satisfies $R_x(0)=x$, and has the identity as its differential at $0$. In this mission $R_x$ is defined on all of $T_xM$.

For a differentiable $f:E\to\mathbb R$ the Riemannian gradient is $\operatorname{grad} f(x)=P_x\nabla f(x)$. Assumption 2.1 (retraction smoothness) asks for a constant $L\ge0$ such that

$$\big|f(R_x(\eta))-f(x)-\langle \operatorname{grad} f(x),\eta\rangle\big|\le \tfrac L2\|\eta\|^2\qquad(x\in M,\ \eta\in T_xM).$$

Given $\mu>0$ and a standard Gaussian vector $u_0\sim N(0,I_n)$ of $E$, set $u=P_xu_0$. The zeroth-order Riemannian gradient estimator is

$$g_\mu(x)=\frac{f(R_x(\mu u))-f(x)}{\mu}\,u .$$

ZO-RGD (Algorithm 1) starts at $x_0\in M$, draws independent Gaussian vectors $u_0^0,u_0^1,\dots$, and sets $x_{k+1}=R_{x_k}(-\hat\eta\, g_\mu(x_k))$, where $g_\mu(x_k)$ uses $u_k=P_{x_k}u_0^k$. The step size is $\hat\eta=1/(2(d+4)L)$. Let $x^*\in M$ be a minimizer of $f$ over $M$.

Formalization targets

Goal: Theorem 3.1

For every $N\ge0$,

$$\frac1{N+1}\sum_{k=0}^{N}\mathbb E\,\|\operatorname{grad} f(x_k)\|^2\le\frac4{\hat\eta}\left(\frac{f(x_0)-f(x^*)}{N+1}+C(\mu)\right),$$

where $4/\hat\eta=8(d+4)L$ and

$$C(\mu)=\frac{\mu^2L}{16}\frac{(d+3)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{d+4}+\frac{\mu^2L}{16}\frac{(d+6)^3}{(d+4)^2}.$$

Milestones

These are the paper's own intermediate results (§2.2, p. 8):

1. Lemma 2.1. For a subspace $\mathcal X$ with projection $P$, $u=Pu_0$ and $x\in\mathcal X$: $\mathbb E\langle x,u\rangle u=x$ and $\mathbb E\langle x,u\rangle^2=\|x\|^2$.
2. Lemma 2.2 (Nesterov–Spokoiny). $\mathbb E\|u\|^p\le(n+p)^{p/2}$ for $p\ge2$. This result is already on the platform as a proved theorem and is referenced.
3. Corollary 2.1. If $\dim\mathcal X=d$, then $\mathbb E\|Pu_0\|^p\le(d+p)^{p/2}$.
4. Proposition 2.1(a). $\|\mathbb E g_\mu(x)-\operatorname{grad} f(x)\|\le\frac{\mu L}{2}(d+3)^{3/2}$.
5. Proposition 2.1(b). $\|\operatorname{grad} f(x)\|^2\le2\|\mathbb E g_\mu(x)\|^2+\frac{\mu^2}{2}L^2(d+6)^3$.
6. Proposition 2.1(c). $\mathbb E\|g_\mu(x)\|^2\le\frac{\mu^2}{2}L^2(d+6)^3+2(d+4)\|\operatorname{grad} f(x)\|^2$.

Significance

Theorem 3.1 shows that ZO-RGD reaches an $\epsilon$-stationary point in expectation using $O(d/\epsilon^2)$ function evaluations, provided the smoothing parameter is of order $\epsilon/d^{3/2}$. The dimension that enters is the intrinsic dimension $d$ of the manifold, not the ambient dimension $n$. For the Stiefel manifold of $n\times p$ orthonormal frames this is the difference between $np-p(p+1)/2$ and $np$, and for the sphere between $n-1$ and $n$. More importantly, the estimator never explores normal directions. The three estimates of Proposition 2.1 are the toolkit that the paper reuses for its stochastic (ZO-RSGD), proximal (ZO-ManPG) and second-order variants.

The paper proves these results on paper; none of them has a machine-checked proof. The mission adds three things. It gives a precise model of a random iterate sequence on a submanifold, driven by the infinite product of Gaussian draws. It formalizes the projected-Gaussian identities, which are reusable for any method that samples in tangent spaces. And it pins down the constants. In checking the constants, the printed Proposition 2.1(b) turned out to be false for large $L$ (its proof yields $L^2$, not $L$), and the middle term of the printed $C(\mu)$ inherits that slip. The statements here carry the constants the proofs actually give.

Difficulty

In Euclidean space, $\mathbb E\,g_\mu(x)$ is exactly the gradient of the Gaussian-smoothed function $f_\mu(x)=\mathbb E f(x+\mu u)$, and the analysis runs on $f_\mu$. Once a retraction replaces $x+\mu u$, no smoothed function has $\mathbb E g_\mu$ as its gradient. The bias must be estimated directly from Assumption 2.1, which controls $f\circ R_x$ only along the tangent space. The moment bounds must then be taken for a Gaussian projected onto a subspace that changes with $x$.

In the descent argument, the direction $u_k$ is sampled in $T_{x_k}M$, which depends on all earlier draws. The expectation of step $k$ is therefore conditional on the past. Summing the one-step inequality requires conditional expectations on the product space, together with measurability of the iterate map. Finiteness of $\mathbb E f(x_k)$ is not given and must be handled as well.

Formalization scope

• Space. The ambient space is a finite-dimensional real inner product space $E$. The standard Gaussian is Mathlib's stdGaussian E, so $\kappa^{-1}\int\cdots e^{-\|u_0\|^2/2}du_0$ becomes integration against it.
• Manifold and tangent spaces. The manifold is given by the published coordinate-slice predicate ProjLikeRetr.Retractor.IsSubmanifold 1 d M, which ties $d$ to $M$. The tangent space is the published ProjLikeRetr.Retractor.tangentSpace M x, the span of Mathlib's tangent cone. Neither $d$ nor the tangent spaces are free parameters.
• Retraction. The retraction is global: Assumption 2.1 is required for every $\eta\in T_xM$ (the paper's "$\rho_x=\infty$"). "Smooth" means $C^\infty$, not analytic.
• Regularity of $f$. $f$ is assumed differentiable on $E$, which is what the definition $\operatorname{grad} f=P_x\nabla f$ needs. This is weaker than the paper's "smooth".
• Constants. The goal takes $L>0$, because the step size divides by $L$. The milestones take $L\ge0$ and $\mu>0$.
• Draws and iterates. The draws live on $E^{\mathbb N}$ with the infinite product of standard Gaussian measures. The iterates are defined for every $k$: the algorithm runs without a stopping time, so the sum over $k=0,\dots,N$ is meaningful.
• Minimizer. $x^*$ is an attained minimizer over $M$.
• Measurability. The goal adds two measurability hypotheses that make the iterates random variables: $(x,\eta)\mapsto R_x(\eta)$ is measurable and $x\mapsto P_x$ is measurable. Both hold for closed manifolds such as spheres and Stiefel manifolds.
• Corrected constants. Proposition 2.1(b) carries $L^2$, and the middle term of $C(\mu)$ carries $L$. The milestone texts keep the printed forms. Proposition 2.1(a) and (c) are as printed.
• Not formalized. The parameter choices $\mu=O(\epsilon/d^{3/2})$, $N=O(d/\epsilon^2)$ in the theorem's second sentence are an $O(\cdot)$ statement.

Several trivializing formalizations are ruled out. A Bochner integral of a non-integrable function is $0$, so every expectation in a conclusion is either a lower Lebesgue integral compared with a finite bound or paired with an integrability conjunct. The dimension $d$ comes from the manifold, not from a free natural number. The projection is onto $M$'s own tangent space, never onto an arbitrary subspace field.

A complete development needs the following infrastructure:

• the law of $P u_0$ (a standard Gaussian on the subspace);
• Gaussian moment bounds;
• conditional expectation along the product filtration;
• measurability of the iterate map.

The projected-Gaussian lemmas and the iterate model are reusable for the stochastic variant (ZO-RSGD) in the companion mission. Contributions of proofs for any milestone, and of general lemmas about Gaussian measures restricted to subspaces, are welcome.

Selected references

• J. Li, K. Balasubramanian, S. Ma, Stochastic Zeroth-Order Riemannian Derivative Estimation and Optimization, Mathematics of Operations Research, 2023; preprint arXiv:2003.11238v3, 2021. https://arxiv.org/abs/2003.11238
• Y. Nesterov, V. Spokoiny, Random Gradient-Free Minimization of Convex Functions, Foundations of Computational Mathematics 17 (2017) 527–566. https://doi.org/10.1007/s10208-015-9296-2
• S. Ghadimi, G. Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, SIAM Journal on Optimization 23 (2013) 2341–2368. https://doi.org/10.1137/120880811
• P.-A. Absil, R. Mahony, R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Princeton University Press, 2008. https://doi.org/10.1515/9781400830244

Motivation

That noncooperative play usually wastes something is part of the folklore of game theory, with the Prisoner's Dilemma as its emblem: each player's best reply leads to an outcome that both would trade for another. Pradeep Dubey's paper turns this folklore into a theorem about smooth games. For games whose payoffs are twice continuously differentiable, and for all payoffs outside a negligible (closed, nowhere dense) set, Nash equilibria are finite in number and are Pareto-inefficient unless some player sits at a vertex of his strategy set. The same conclusion applies to Nash's mixed extensions of finite games (Nash 1951), where a vertex is a pure strategy.

The question is basic to welfare analysis of strategic interaction: market games, oligopoly, public goods and trading mechanisms (Shapley and Shubik 1977) all ask whether equilibrium outcomes can be efficient. Dubey's answer is that efficiency of an equilibrium is non-generic, so a model that delivers it is exploiting special structure.

Timeline. Nash (1951) introduced equilibrium points and multi-matrix games. Smale (1973, "Optimizing several functions") gave the first-order condition for Pareto optimality of several smooth functions: at an efficient interior point the gradients are linearly dependent. Harsanyi (1973, IJGT 2:235–250) proved that generic finite games have finitely many, indeed an odd number of, mixed equilibria. Dubey's Cowles Foundation Discussion Paper 508R (1978) stated finiteness and inefficiency; the version formalized here is the rewrite IIASA WP-83-74 (1983), published as Mathematics of Operations Research 11(1):1–8 (1986).

Setting

There are $n\ge2$ players $N=\{1,\dots,n\}$. Player $i$'s strategy set is the unit simplex

$$S^i=\Big\{x\in\mathbb R^{k(i)}_+ : \sum_{j=1}^{k(i)}x_j\le1\Big\},\qquad k(i)\ge1,$$

whose vertices (extreme points) are the origin and the unit vectors. Profiles $s=(s^1,\dots,s^n)$ range over $S=S^1\times\dots\times S^n\subset\mathbb R^{r(n)}$, $r(n)=\sum_i k(i)$.

Fix open neighbourhoods $V^i\supseteq S^i$ and $V=V^1\times\dots\times V^n$. The space $U$ consists of the $C^2$ functions $f:V\to\mathbb R$ with finite $C^2$-norm $\|f\|=\sup\{\|f(s)\|,\|Df(s)\|,\|D^2f(s)\|: s\in V\}$. A game is $u=(u^1,\dots,u^n)\in(U)^n$. For $T\subseteq N$, $(s|e)$ replaces $s^i$ by $e^i$ for $i\in T$. A profile $s\in S$ is $T$-efficient if no $e\in\times_{i\in T}S^i$ gives $u^i(s|e)\ge u^i(s)$ for all $i\in T$ with strict inequality for some $j\in T$. It is a Nash equilibrium if it is $\{i\}$-efficient for each $i$, efficient if it is $N$-efficient, and a strong Nash equilibrium if it is $T$-efficient for every $T$. The three sets are $N(u)$, $E(u)$, $G(u)$.

In the proof, $D_u(s)$ is the $n\times r(n)$ matrix with rows $Du^i(s)$; $N^*$ is the subspace of matrices whose $i$-th row vanishes on player $i$'s block of columns; $E^*$ is the set of matrices with linearly dependent rows.

Formalization targets

Goal: the Theorem (p. 3)

There is an open dense set $U_0\subseteq(U)^n$ such that for $u\in U_0$:

$$\text{(a) } N(u)\text{ is finite};\quad \text{(b) } s\in N(u)\cap E(u)\Rightarrow \exists j,\ s^j\text{ is a vertex};\quad \text{(c) } s\in G(u)\Rightarrow \text{at most one } s^j \text{ is not a vertex}.$$

Milestones (pp. 4–6)

For interior profiles ($s^i\in\operatorname{Int}S^i$ for all $i$):

$$\text{(i) } s\in N(u)\Rightarrow D_u(s)\in N^*,\qquad \text{(ii) } s\in E(u)\Rightarrow D_u(s)\in E^*,$$

$\operatorname{codim}N^*=r(n)$; the linear perturbation $u_t^i(x)=u_0^i(x)+t\sum_j y_{ij}x_j$ satisfies $\frac{d}{dt}D(u_t,s_0)|_{t=0}=y$ (the computation behind (**)); claim (*) for $M=N^*$: for an open dense set of games $D_u$ is transverse to $N^*$ on a compact neighbourhood $\underline V$ of $S$; under that transversality $S\cap D_u^{-1}(N^*)$ is finite; and the Theorem restricted to interior profiles.

Companions

The Theorem (Multi-Matrix) (p. 14): for an open dense set of payoff vectors $a\in(\mathbb R^K)^n$, the mixed Nash equilibria of $\Pi_a$ are finite, an efficient one has a player using a pure strategy, and a strong one is pure. From the example of §3: every game $(P,Q)$ on $[0,1]^2$ with payoffs $u_P(x,y)=-[(x-a)^2+(y-b)^2]$ has a unique Nash equilibrium (p. 9); Lemma 1, $E(P,Q)=r_X(L(P,Q))$ (p. 9); Lemma 2(a), an interior equilibrium is efficient iff $a=c$ or $b=d$ (p. 10).

Significance

The theorem gives the generic structure of equilibrium sets in smooth games: isolated and finitely many equilibria, and a sharp location of the only places where efficient equilibria can survive, namely the vertices. It explains why efficiency results for noncooperative models need boundary solutions or non-generic structure, and in its multi-matrix form it shows that strong equilibria of generic finite games are in pure strategies. It also supplies the finiteness of equilibria used in comparative-statics and index arguments.

On the formalization side, the result is proved on paper but has no machine-checked version. A complete development would give Lean its first generic-finiteness theorem for Nash equilibria of smooth games, a first-order Pareto condition in the form of Smale's lemma, and a parametric transversality argument in finite dimensions. The multi-matrix companion connects to the published vocabulary of finite games (agt_games), and the example of §3 is an elementary, fully explicit check of the general picture.

Difficulty

The interior case reduces, by (i) and (ii), to a dimension count: $D_u^{-1}(N^*)$ should be zero-dimensional and $D_u^{-1}(N^*\cap E^*)$ empty. Neither holds for every game: they hold only when $D_u$ is transverse to $N^*$ and to the strata of $N^*\cap E^*$, and the step that requires work is showing that transversality is an open and dense condition in the $C^2$ topology. Density is not obtained by adding linear functions to the payoffs: a linear function has finite $C^2$-norm on $V$ only when $V$ is bounded, so perturbations must be localized. The step from interior profiles to the whole of $S$ is a second difficulty. It requires repeating the argument on every product of faces of the simplices and on every subgame, and then intersecting finitely many open dense sets. Efficiency at a boundary point is not $T$-efficiency in a subgame, so the reduction has to be made with care.

Formalization scope

Players are Fin n with 2 ≤ n; block sizes k : Fin n → ℕ with 1 ≤ k i; profiles are ∀ i, Fin (k i) → ℝ. The simplex is the paper's corner simplex {x ≥ 0, ∑ x ≤ 1}, not the probability simplex; "vertex" is Set.extremePoints. The neighbourhoods $V^i$ are taken open, and the goal is stated for every such choice, not assuming $V$ bounded or convex. Payoffs are total functions; a game is ContDiffOn ℝ 2 on $V$ with finite $C^2$-norm, which takes values in $[0,\infty]$, so no junk real supremum enters. "Open dense in $(U)^n$" is written in $\varepsilon$-form for the product of $C^2$-norm topologies; Lean's sup-type norms are equivalent to the Euclidean ones, so the open dense sets are the same. Deviations range over all strategies in $\times_{i\in T}S^i$, not only pure or vertex deviations.

Added hypotheses, all disclosed in the items: openness of $V^i$; interiority of every $s^i$ on milestones (i), (ii) and the finiteness step (the proof's standing case assumption); $M=N^*$ in claim (*). The printed "By (i), $N(u)\subset S\cap D_u^{-1}(N^*)$" is stated for interior equilibria, which is where (i) applies.

A trivializing formalization is ruled out: the open dense set must contain games arbitrarily close to every game (the zero game is a game, so it is never empty), interiority appears only in the milestones and not in the goal, and efficiency is with respect to all deviations in $S$.

Not stated: (*) for a general submanifold $M$, and the decomposition of $N^*\cap E^*$ into submanifolds of codimension $\ge r(n)+1$, both of which need embedded submanifolds of $\mathbb R^N$; Remarks 1–4 (Remark 4's openness claim for strictly concave payoffs is false as printed); Lemma 2(b); §5, which the author leaves as a conjecture. Contributions welcome: a finite-dimensional parametric transversality theorem, Smale's first-order Pareto condition, and the face-by-face reduction.

Selected references

• P. Dubey, Inefficiency of Nash Equilibria, IIASA Working Paper WP-83-74, 1983; Mathematics of Operations Research 11(1):1–8, 1986. https://doi.org/10.1287/moor.11.1.1
• J. F. Nash, Non-Cooperative Games, Annals of Mathematics 54:286–295, 1951. https://doi.org/10.2307/1969529
• J. C. Harsanyi, Oddness of the Number of Equilibrium Points: A New Proof, International Journal of Game Theory 2:235–250, 1973. https://doi.org/10.1007/BF01737572
• S. Smale, Optimizing Several Functions, Manifolds — Tokyo 1973, Proceedings of the International Conference on Manifolds, University of Tokyo Press, 1975.
• R. Abraham and J. Robbin, Transversal Mappings and Flows, W. A. Benjamin, New York, 1967.
• L. S. Shapley and M. Shubik, Trade Using One Commodity as a Means of Payment, Journal of Political Economy 85:937–968, 1977. https://doi.org/10.1086/260617

Motivation

A lower bound $K$ on the Ricci curvature of a Riemannian manifold and an upper bound $N$ on its dimension can be expressed without coordinates in two ways. The Bakry–Émery condition $\mathrm{BE}(K,N)$ is a property of the heat semigroup and its generator: the iterated carré du champ $\Gamma_2$ dominates $K\Gamma+\frac1N(\Delta f)^2$ (Bakry–Émery 1985). The Riemannian curvature-dimension conditions $\mathrm{RCD}(K,\infty)$ and $\mathrm{RCD}^*(K,N)$ are properties of a metric measure space, defined through optimal transport (Ambrosio–Gigli–Savaré 2014). A basic test for any notion of "Ricci curvature at least $K$, dimension at most $N$" is its behaviour under products: on a product of manifolds, Ricci curvature bounds combine and dimensions add.

The paper of Ambrosio, Gigli and Savaré (arXiv:1209.5786) proves that $\mathrm{BE}(K,\infty)$ and $\mathrm{RCD}(K,\infty)$ coincide on a natural class of Dirichlet-form spaces, and draws from it, in its §5.1, two tensorization results. The first (Theorem 5.1) is the stability of $\mathrm{RCD}(K,\infty)$ under products. This had been proved in Ambrosio–Gigli–Savaré 2014 only under a nonbranching assumption on the factors; the equivalence removes that assumption. The second (Theorem 5.2) is the dimensional statement: the product of two Riemannian Energy measure spaces satisfying $\mathrm{BE}(K,N_X)$ and $\mathrm{BE}(K,N_Y)$ satisfies $\mathrm{BE}(K,N_X+N_Y)$, the bound on the dimension of the product that the smooth case predicts.

Setting

Let $X$ be a complete separable metric space with a Borel measure $\mathfrak m$. A Dirichlet form is a quadratic, $L^2$-lower semicontinuous, Markovian functional $\mathcal E:L^2(X,\mathfrak m)\to[0,\infty]$ with dense domain $\mathbb V$. Its generator $\Delta_{\mathcal E}$ is defined by $\mathcal E(f,g)=-\int g\,\Delta_{\mathcal E}f\,d\mathfrak m$ for all $g\in\mathbb V$, and its heat flow $\mathsf P_t$ solves $\frac{d}{dt}\mathsf P_tf=\Delta_{\mathcal E}\mathsf P_tf$. The carré du champ $\Gamma(f)$ is the density of $\varphi\mapsto\mathcal E(f,f\varphi)-\frac12\mathcal E(f^2,\varphi)$. For $\nu=1/N\ge0$, $\mathrm{BE}(K,N)$ is the weak form (2.33) of $\Gamma_2\ge K\Gamma+\nu(\Delta f)^2$, written through the functional $\mathsf A_t[f;\varphi](s)=\frac12\int(\mathsf P_{t-s}f)^2\mathsf P_s\varphi\,d\mathfrak m$.

The intrinsic distance is $\mathsf d_{\mathcal E}(x,y)=\sup\{|\psi(y)-\psi(x)|:\psi\text{ continuous},\ \Gamma(\psi)\le1\}$. An Energy measure space (Definition 3.6) is a strongly local Dirichlet form on a space whose metric is $\mathsf d_{\mathcal E}$, with full-support measure and an exhausting function; a Riemannian Energy measure space (Definition 3.16) is in addition upper regular, and every $\psi$ with $\Gamma(\psi)\le1$ has a continuous version. An $\mathrm{RCD}(K,\infty)$ space (Definition 3.1) is a length metric measure space with the growth bounds (MD.b) and (MD.exp) on which the relative entropy has an $\mathrm{EVI}_K$ gradient flow in $(\mathscr P_2(X),W_2)$.

The product (5.1) of $(X,\mathsf d_X,\mathfrak m_X)$ and $(Y,\mathsf d_Y,\mathfrak m_Y)$ is $Z=X\times Y$ with

$$\mathsf d((x,y),(x',y'))=\sqrt{\mathsf d_X^2(x,x')+\mathsf d_Y^2(y,y')},\qquad\mathfrak m=\mathfrak m_X\times\mathfrak m_Y,$$

and the Cartesian Dirichlet form (5.2) is

$$\mathcal E(f)=\int_Y\mathcal E^X(f^y)\,d\mathfrak m_Y(y)+\int_X\mathcal E^Y(f^x)\,d\mathfrak m_X(x),$$

where $f^y=f(\cdot,y)$ and $f^x=f(x,\cdot)$.

Formalization targets

Goal: Theorem 5.2

If $(X,\mathcal E^X,\mathfrak m_X)$ and $(Y,\mathcal E^Y,\mathfrak m_Y)$ are Riemannian Energy measure spaces satisfying (MD.exp), $\mathrm{BE}(K,N_X)$ and $\mathrm{BE}(K,N_Y)$, then

$$(Z,\mathcal E,\mathfrak m)\ \text{is a Riemannian Energy measure space with}\ \mathsf d_{\mathcal E}=\mathsf d\ \text{and}\ \mathrm{BE}(K,N_X+N_Y).$$

In the parametrization $\nu=1/N$ the product satisfies $\mathrm{BE}$ with $\nu_Z=\nu_X\nu_Y/(\nu_X+\nu_Y)$.

Milestones

1. Corollary 4.18 (i), p. 58: under (MD+exp) and a quadratic Cheeger energy, the length property together with the gradient bound

$$|\mathrm D\mathsf P_tf|^2\le e^{-2Kt}\mathsf P_t(|\mathrm Df|_w^2)\tag{4.30}$$

implies $\mathrm{RCD}(K,\infty)$. 2. Theorem 5.1, p. 60: the product of two $\mathrm{RCD}(K,\infty)$ spaces is $\mathrm{RCD}(K,\infty)$. 3. The elementary inequality of p. 62: $\nu_Xa^2+\nu_Yb^2\ge\frac{\nu_X\nu_Y}{\nu_X+\nu_Y}(a+b)^2$ for positive $\nu_X,\nu_Y$ and nonnegative $a,b$. 4. Lemma 5.3, p. 62: $\Delta_Zf(x,y)=\Delta_Xf^y(x)+\Delta_Yf^x(y)$ under the fibrewise regularity (5.9), for the RCD factors and their Cheeger forms fixed in §5.1.

Significance

Theorem 5.1 shows that $\mathrm{RCD}(K,\infty)$ is closed under products with no nonbranching condition on the factors, the hypothesis under which Ambrosio–Gigli–Savaré 2014 had obtained it. Theorem 5.2 gives the dimensional version for Dirichlet-form spaces, $\mathrm{BE}(K,N_X)\times\mathrm{BE}(K,N_Y)\Rightarrow\mathrm{BE}(K,N_X+N_Y)$: a product of spaces of finite dimension has finite dimension, with the bound $N_X+N_Y$ of the smooth case, while the condition $\mathrm{BE}(K,\infty)$ alone loses all dimensional information.

Both results are proved in the paper; none of them, nor the objects they are stated for, has a machine-checked proof. The mission produces a Lean statement of the Cartesian Dirichlet form and of the product structure, the statements of the two tensorization theorems, and the characterization of $\mathrm{RCD}(K,\infty)$ that drives Theorem 5.1. A formal proof would also check the measure-theoretic steps that the paper takes for granted: the measurability of $y\mapsto\mathcal E^X(f^y)$, the Fubini arguments of Lemma 5.3, and the identification of the domain of the Cartesian form (cited from [Ambrosio–Gigli–Savaré 2014], Theorem 6.18).

Difficulty

The obvious argument works fibre by fibre: apply $\mathrm{BE}(K,N_X)$ to each section $f^y$ and $\mathrm{BE}(K,N_Y)$ to each $f^x$, and add. This fails as stated, because $\mathsf P_t$ on $Z$ does not act on the sections separately: $(\mathsf P_tf)^y$ is an average over $y'$ of the semigroup of $X$ applied to $f^{y'}$, weighted by the heat kernel of $Y$, so fibrewise gradient and Laplacian bounds have to be transported through this average. For Theorem 5.2 a second step is not fibrewise at all: before any dimensional estimate, the product has to be shown to be a Riemannian Energy measure space whose intrinsic distance is the product distance, which in the paper goes through Theorem 5.1 and hence through the equivalence $\mathrm{BE}(K,\infty)\Leftrightarrow\mathrm{RCD}(K,\infty)$ of Theorem 4.17.

Formalization scope

Functions on $X$ are X → ℝ, and $L^2$ membership is MemLp f 2 m; every object is invariant under $\mathfrak m$-a.e. equality. Dirichlet forms take values in $[0,\infty]$ and are $+\infty$ off $L^2$. Heat flows are passed as functions pinned by the predicate IsHeatSemigroup. $\Gamma(f)$ is a predicate on a density. $\mathrm{BE}(K,N)$ is parametrized by $\nu=1/N\ge0$; $\nu_Z=\nu_X\nu_Y/(\nu_X+\nu_Y)$ is $0$ when either factor has $N=\infty$. The product $Z$ is WithLp 2 (X × Y), whose metric is the $\ell^2$ distance (5.1); the plain type X × Y would carry the max-metric. The second term of (5.2) uses $\mathcal E^Y$, correcting the printed $\mathcal E^X(f^x)$. Factors are σ-finite.

Theorem 5.2 assumes (MD.exp) for both factors: its proof invokes Theorem 5.1, whose factors must be $\mathrm{RCD}(K,\infty)$, which a Riemannian Energy measure space with $\mathrm{BE}(K,\infty)$ is only under (MD.exp). In Corollary 4.18, the minimal weak gradient is written as $|\mathrm Df|_w^2=\Gamma(f)$, the identity that (QCh) asserts. Lemma 5.3 carries the RCD and Cheeger-form assumptions established at the opening of §5.1. The elementary inequality retains the printed $a,b\ge0$; applying it to signed Laplacians requires its all-real extension.

The goal is not met by stating $\mathrm{BE}$ on the product with $\nu_Z=0$: that is $\mathrm{BE}(K,\infty)$, a strictly weaker claim; nor by defining the product form through the Cheeger energy of $Z$ instead of (5.2).

A complete development needs the Cartesian form's domain theorem, a pointwise version of the heat semigroups, Theorem 4.17 of the paper and the converse $\mathrm{RCD}(K,\infty)\Rightarrow\mathrm{BE}(K,\infty)$ from [Ambrosio–Gigli–Savaré 2014]. The product layer (sections, Cartesian form, Lemma 5.3) is reusable for any tensorization argument on Dirichlet forms. Proofs of the elementary inequality and of Lemma 5.3 are the natural first contributions.

Selected references

• L. Ambrosio, N. Gigli, G. Savaré, Bakry–Émery curvature-dimension condition and Riemannian Ricci curvature bounds, Ann. Probab. 43(1), 339–404, 2015. arXiv:1209.5786v4
• L. Ambrosio, N. Gigli, G. Savaré, Metric measure spaces with Riemannian Ricci curvature bounded from below, Duke Math. J. 163(7), 1405–1490, 2014. arXiv:1109.0222
• D. Bakry, M. Émery, Diffusions hypercontractives, Séminaire de Probabilités XIX, Lecture Notes in Math. 1123, 177–206, 1985. doi:10.1007/BFb0075847