Gribov Ambiguity: no continuous gauge fixing (Singer 1978)Research Paper
## Motivation
In the Feynman path-integral approach to a non-abelian gauge theory one wants to integrate a
gauge-invariant weight over the space $\mathfrak{A}$ of vector potentials (connections) of a
principal bundle. The integrand is constant on the orbits of the group $\mathcal{G}$ of gauge
transformations, so the integral over $\mathfrak{A}$ diverges and one is supposed to integrate
instead over the orbit space $\mathfrak{R} = \mathfrak{A}/\mathcal{G}$. The Faddeev–Popov
procedure realizes this by *fixing a gauge*: choosing, continuously in the orbit, exactly one
vector potential on each orbit, and correcting by a Jacobian determinant.
V. N. Gribov (SLAC Translation 176, 1977) observed that for $SU(2)$ potentials on
$\mathbb{R}^3$ (or $\mathbb{R}^4$) with suitable conditions at infinity, the Coulomb gauge
condition does not do this: the Coulomb slice through the zero potential meets the orbit of the
zero potential again, far from the origin. These extra intersections are the **Gribov copies**;
R. Jackiw, I. Muzinich and C. Rebbi (Phys. Rev. D 17 (1978) 1576) analyzed them in detail.
I. M. Singer, *Some Remarks on the Gribov Ambiguity* (Commun. Math. Phys. **60** (1978) 7–12),
showed that the phenomenon is not a defect of the Coulomb gauge. If the conditions at infinity
are those of Gribov — gauge transformations extending to the one-point compactification with
value $I$ at infinity, so that the base manifold is $M = S^3$ or $M = S^4$ — then **no**
continuous gauge fixing exists at all, in any gauge. The obstruction is topological: the space
of irreducible connections is weakly contractible, while the gauge group is not, and a
weakly contractible principal bundle admits no global continuous section.
## Setting
Fix $N \ge 2$ and take the structure group $SU(N)$, the group of $N \times N$ complex matrices
$U$ with $U^\ast U = I$ and $\det U = 1$, topologized as a subspace of matrices. Let
$S^r$ denote the unit sphere of $\mathbb{R}^{r+1}$, with base point $m$ the north pole.
For the trivial $SU(N)$-bundle over a space $M$, a gauge transformation is a map
$\varphi : M \to SU(N)$, and the **gauge group** is
$$\mathcal{G}(M,N) \;=\; C\bigl(M, SU(N)\bigr),$$
continuous maps with pointwise multiplication and the compact-open topology. Two subobjects
matter. The **based gauge group** $\mathcal{G}_m = \{\varphi : \varphi(m) = I\}$ is the subgroup
of transformations that are the identity at the base point. The constant transformations with
value in the centre $Z_N = \{e^{2\pi i k/N} I\}$ of $SU(N)$ form a normal subgroup, and the
**reduced gauge group** is the quotient
$$\overline{\mathcal{G}}(M,N) \;=\; \mathcal{G}(M,N)/Z_N$$
with the quotient topology. The centre acts trivially on vector potentials, so
$\overline{\mathcal{G}}$ is the group that acts effectively.
A group $G$ acting continuously on a space $\mathfrak{A}$ has orbit space
$\mathfrak{A}/G$ with the quotient topology, and a **gauge fixing** is a continuous map
$s : \mathfrak{A}/G \to \mathfrak{A}$ with $p \circ s = \mathrm{id}$, where
$p : \mathfrak{A} \to \mathfrak{A}/G$ is the projection: a continuous choice of exactly one point
on each orbit. The action is **principal** when it is free and the division map, which sends a
pair of points on one orbit to a group element carrying the second to the first, can be chosen
continuously; this is the topological content of "$p$ is a principal $G$-bundle". The space
$\mathfrak{A}$ is **weakly contractible** when it is nonempty and all its homotopy groups vanish.
In the paper, $\mathfrak{A}$ is the affine space of connections, $\mathfrak{R}$ its set of
irreducible members, and Theorems 1 and 2 say exactly that $\mathfrak{R}$ is a weakly
contractible principal $\overline{\mathcal{G}}$-space.
## Formalization targets
### Goal — Corollary 4 (no gauge fixing)
For $r \in \{3,4\}$, $N \ge 2$, and every weakly contractible principal
$\overline{\mathcal{G}}(S^r,N)$-space $A$:
$$\nexists\, s : A/\overline{\mathcal{G}}(S^r,N) \longrightarrow A \quad\text{continuous with}\quad p \circ s = \mathrm{id}.$$
By Theorems 1 and 2 of the paper the space of irreducible connections over $S^3$ or $S^4$ is such
an $A$, so the goal contains Singer's Corollary 4 for that space; it leaves the analytic
construction of the space of connections unfixed, which is what makes it statable today.
### Milestone level — Theorem 3
$$\exists\, j \ge 1: \quad \pi_j\bigl(\overline{\mathcal{G}}(S^r,N)\bigr) \neq 0, \qquad r \in \{3,4\},\ N \ge 2 .$$
### Milestone level — Theorem 5 and its homotopy inputs
$$\pi_j\bigl(\mathcal{G}_m(S^r,N)\bigr) \;\cong\; \pi_{j+r}\bigl(SU(N)\bigr), \qquad
\pi_3(SU(N)) \cong \mathbb{Z}, \qquad \pi_4(SU(N)) = 0 \ (N\ge 3), \qquad \pi_4(SU(2)) \cong \mathbb{Z}/2 .$$
## Significance
The result rules out the existence of a global gauge in the topological sense: every gauge
condition used in practice is at best a local slice, and the Faddeev–Popov construction has to be
read as a local statement, patched with a partition of unity over the orbit space (as the last
section of the paper proposes). It is the mathematical reason why the Gribov ambiguity cannot be
repaired by a cleverer gauge condition, and it is the origin of the Gribov–Zwanziger restriction
of the functional integral to a fundamental domain.
Formalizing it adds a machine-checked version of an argument that is quoted far more often than
it is checked, and it forces into Lean a piece of infrastructure that Mathlib currently lacks:
homotopy groups of mapping spaces, the long exact sequence of a fibration in the form needed for
$0 \to \mathcal{G}_m \to \mathcal{G} \to SU(N) \to 0$, and the classical computations
$\pi_3(SU(N)) \cong \mathbb{Z}$, $\pi_4(SU(N)) = 0$ for $N \ge 3$, $\pi_4(SU(2)) \cong \mathbb{Z}/2$.
Singer's results are proved mathematics; none of them is formalized, and Mathlib as of the pinned
revision contains homotopy groups as a definition together with their group structure, but
essentially no computation of them.
## Difficulty
The naive approach to the goal — build a section by hand, or average over the group — fails
because $\overline{\mathcal{G}}$ is neither compact nor contractible and the obstruction is
global: locally, slices do exist (that is the content of the generalized Coulomb gauge), so no
local argument can produce a contradiction. The proof has to convert a section into a
homotopy-theoretic statement: a section of a principal bundle trivializes it, exhibiting the
group as a retract of the total space, so all homotopy groups of the group would vanish; the work
is then to show that some homotopy group of the reduced gauge group does not vanish, which needs
the identification of the based gauge group with a mapping space, the exact sequences relating
$\mathcal{G}_m$, $\mathcal{G}$ and $\overline{\mathcal{G}}$, and non-trivial homotopy groups of
$SU(N)$ — including $\pi_6(S^3) \cong \mathbb{Z}/12$ for the $SU(2)$ case of Theorem 3.
## Formalization scope
The formalization commits to the following conventions, all of them visible in the definitions of
this mission.
- The bundle is the **trivial** $SU(N)$-bundle, so gauge transformations are literally maps
$M \to SU(N)$. This is the case of Gribov's original setting over $S^3$; over $S^4$ the paper
also treats bundles of nonzero Pontrjagin index, which are out of scope here.
- Gauge transformations are **continuous**, not smooth, with the compact-open topology; Singer's
Theorem 5 uses smoothing homotopies to pass between the two, and the homotopy-theoretic content
is the same.
- $SU(N)$ is the special unitary group of complex $N \times N$ matrices, with its subspace
topology; $S^r$ is the unit sphere of $\mathbb{R}^{r+1}$ with its subspace topology.
- Homotopy groups are Mathlib's `HomotopyGroup`, based at the identity element.
- The **space of connections is not constructed**: Mathlib has no space of connections on a
principal bundle, and building one is a mission of its own. The goal therefore quantifies over
an arbitrary topological space carrying a weakly contractible principal action of the reduced
gauge group — exactly the properties Theorems 1 and 2 establish for the irreducible
connections.
- This quantification is not vacuous: such spaces exist (the total space of a universal
$\overline{\mathcal{G}}$-bundle is one), so the goal is a genuine non-existence statement and
not a statement about an empty class. Conversely it is not trivially true: the hypotheses do
not mention any homotopy invariant of the gauge group, and refuting a section requires
Theorem 3.
- The paper's analytic statements — Theorem 1 (openness and density of the irreducible
connections, principal bundle structure), Theorem 2 (weak contractibility), Theorem 6
($\pi_1$ of the irreducible orbit space), Theorem 7 (no flat connection), Theorem 8 (tangency
of orbits to the Coulomb slice) and Theorem 9 (the canonical connection and its curvature) —
are out of scope until a space of connections exists in Lean. Contributions that build one, in
reusable form, are welcome and would let this mission be extended to them.
## Selected references
- V. N. Gribov, *Instability of non-abelian gauge theories and impossibility of choice of Coulomb
gauge*, SLAC Translation 176 (1977); Nucl. Phys. B **139** (1978) 1–19,
[doi:10.1016/0550-3213(78)90175-X](https://doi.org/10.1016/0550-3213(78)90175-X).
- I. M. Singer, *Some Remarks on the Gribov Ambiguity*, Commun. Math. Phys. **60** (1978) 7–12,
[doi:10.1007/BF01609471](https://doi.org/10.1007/BF01609471).
- R. Jackiw, I. Muzinich, C. Rebbi, *Coulomb gauge description of large Yang-Mills fields*,
Phys. Rev. D **17** (1978) 1576, [doi:10.1103/PhysRevD.17.1576](https://doi.org/10.1103/PhysRevD.17.1576).
- H. Toda, *Composition methods in homotopy groups of spheres*, Annals of Mathematics Studies 49,
Princeton University Press (1962).
8 thms1 active userReviewed
🏆Completed
Captain: Lucas
Rudin PMA X: Integration of Differential FormsTextbook
## Motivation
Chapter 10 of Walter Rudin's *Principles of Mathematical Analysis* (3rd edition, McGraw-Hill,
1976) builds the calculus of **differential forms** in $\mathbb{R}^n$ and proves the theorem
that unifies the integral theorems of vector analysis. The fundamental theorem of calculus, the
Green, divergence and classical Stokes theorems all say the same thing — that integrating a
derivative over a region is the same as integrating the original object over the boundary of
that region — and **Stokes' theorem** (Theorem 10.33),
$$\int_\Psi d\omega = \int_{\partial \Psi} \omega ,$$
is that statement, once "region" is made precise as a *chain* of parametrized surfaces and
"derivative" as the exterior derivative.
This mission is the tenth in a series formalizing Rudin Chapters 1–11; it uses the inverse
function theorem and the several-variable calculus of Mission IX.
## Setting
For an open $E \subseteq \mathbb{R}^n$, a **$k$-surface** in $E$ is a $C'$-mapping $\Phi$ from a
parameter domain $D \subseteq \mathbb{R}^k$ — a $k$-cell or the standard simplex
$Q^k = \{u : u_i \ge 0, \sum u_i \le 1\}$ — into $E$; surfaces are maps, not point sets. A
**$k$-form** in $E$ is a formal sum
$$\omega = \sum a_{i_1\cdots i_k}(\mathbf{x})\,dx_{i_1}\wedge\cdots\wedge dx_{i_k}$$
with continuous coefficients, whose meaning is the rule assigning to each $k$-surface $\Phi$ the
number
$$\int_\Phi \omega = \int_D \sum a_{i_1\cdots i_k}(\Phi(\mathbf{u}))\,
\frac{\partial(\varphi_{i_1},\dots,\varphi_{i_k})}{\partial(u_1,\dots,u_k)}\,d\mathbf{u}.$$
The **exterior derivative** of $\omega$ is the $(k+1)$-form with coefficients $D_j a_I$; the
**pullback** $\omega_T$ along a differentiable $T$ substitutes $T$ into the coefficients and the
differentials. A **$k$-chain** is a formal integer combination of $k$-surfaces with parameter
domain $Q^k$, its integral is the corresponding combination of integrals, and its **boundary**
$\partial\Psi$ is obtained from the alternating sum $\sum_j (-1)^j$ of the faces of $Q^k$.
## Formalization targets
### Goal — Stokes' theorem (Theorem 10.33)
If $\Psi$ is a $k$-chain of class $C''$ in an open $V \subseteq \mathbb{R}^n$ and $\omega$ is a
$(k-1)$-form of class $C'$ in $V$, then
$$\int_\Psi d\omega = \int_{\partial\Psi} \omega .$$
For $k = n = 1$ this is the fundamental theorem of calculus, for $k = n = 2$ Green's theorem,
for $k = n = 3$ the divergence theorem, and for $k = 2$, $n = 3$ the theorem of Stokes.
### Milestones
$$\text{the iterated integrals of a continuous function on a cell agree} \qquad (10.2)$$
$$\text{partitions of unity subordinate to an open cover of a compact set} \qquad (10.8)$$
$$\int f(\mathbf{y})\,d\mathbf{y} = \int f(T(\mathbf{x}))\,|J_T(\mathbf{x})|\,d\mathbf{x} \qquad (10.9)$$
$$d(d\omega) = 0 \qquad (10.20)$$
$$(d\omega)_T = d(\omega_T) \qquad (10.22\mathrm{c})$$
$$\int_{T\circ\Phi}\omega = \int_\Phi \omega_T \qquad (10.25)$$
$$\text{reordering the vertices of a simplex multiplies the integral by the sign} \qquad (10.27)$$
$$\text{Poincaré's lemma: on a convex open set, closed forms are exact} \qquad (10.39)$$
## Significance
Stokes' theorem is the organizing theorem of multivariable analysis; its formal content is that
$d$ and $\partial$ are adjoint, which is also the starting point of de Rham cohomology.
Poincaré's lemma is its local converse: on a convex set the only obstruction to a closed form
being exact disappears, so the failure of exactness measures the shape of the domain. The change
of variables theorem (10.9) is what makes integrals independent of the parametrization and is
used in the proof of Stokes itself, and partitions of unity (10.8) are the standard device for
passing from local to global statements.
Mathlib has a general change-of-variables theorem for the Lebesgue integral, smooth partitions
of unity, and the theory of alternating forms and de Rham differentials on manifolds; it does
not have Rudin's concrete apparatus of parametrized surfaces, affine chains, and their
boundaries, nor a version of Stokes' theorem for such chains. This mission builds that
apparatus and states the chapter's theorems for it; the definitions are reusable for any
development that wants a hands-on, coordinate-based treatment of forms.
## Difficulty
This is the most demanding mission of the series, for two reasons. First, the objects have to be
set up before anything can be said: forms as coefficient families, their integrals as Jacobian
integrals, chains, and the boundary operator with its signs. Second, Stokes' theorem is proved
by reducing to a single oriented simplex, transporting along the parametrization by Theorem
10.25, and then computing the integral over $Q^k$ by an iterated integral in which all but two
terms of the boundary cancel; the cancellation is entirely a matter of getting the signs of the
face maps right, and it is where a formalization will spend its time.
A further subtlety: with forms presented by coefficients indexed by *all* index tuples, the
identity $d(d\omega) = 0$ is false coefficient-wise and true as an identity of forms. Since
Rudin defines a form to *be* its integration functional, statements of the shape "this form
vanishes" are formalized as "its integral over every surface vanishes", and that is how 10.20,
10.22(c) and 10.39 are stated here.
## Formalization scope
Conventions fixed by this mission:
* Points of $\mathbb{R}^n$ are `Fin n → ℝ`. A $k$-form is `Rudin.KForm k n`, a coefficient
function indexed by all tuples `Fin k → Fin n`, following Rudin's equation (34).
* `Rudin.integralOverCell` and `Rudin.integralOverSimplex` are Rudin's equation (35) for the two
admissible parameter domains, with `Rudin.jacobian` the determinant of the matrix of partial
derivatives. The integral over the parameter domain is the Lebesgue integral for the volume
measure, which agrees with Rudin's Riemann integral for continuous integrands.
* `Rudin.extDeriv` and `Rudin.pullback` are the exterior derivative and the pullback;
`Rudin.Chain`, `Rudin.Chain.integral` and `Rudin.Chain.boundary` are chains with integer
multiplicities, their integrals, and the boundary built from the faces of the standard simplex
with Rudin's signs $(-1)^j$.
* Regularity is `ContDiff ℝ 1` and `ContDiff ℝ 2` for Rudin's $C'$ and $C''$.
* Equalities between forms are stated as equalities of their integrals over surfaces, as
explained above; the goal theorem is an equality of two real numbers, so it is not vacuous.
Contributions of the supporting differential-form identities (10.20, 10.22, 10.25) are
especially welcome, since they are exactly the lemmas the goal theorem consumes.
## Selected references
- Walter Rudin, *Principles of Mathematical Analysis*, 3rd edition, McGraw-Hill, 1976,
Chapter 10 (pp. 245–299).
- Michael Spivak, *Calculus on Manifolds*, W. A. Benjamin, 1965.
18 thms4 active usersReviewed
🏆Completed
Captain: He Wang
Kerr Vacuum Solution Verification in Boyer–Lindquist CoordinatesResearch Paper
## Why a coordinate verification of Kerr
The Kerr metric (Kerr, 1963) is the exact solution of the vacuum Einstein equations that describes the exterior gravitational field of a rotating mass. It is the working model for astrophysical black holes: gravitational-wave templates, black-hole imaging and the classification results of the uniqueness theorems all take it as their starting point. Its form in the coordinates of Boyer and Lindquist (1967) is the one found in every textbook, and the statement that this line element has vanishing Ricci tensor is the single most-cited computation of the subject. That computation is long, it is almost never printed, and in practice it is trusted because computer-algebra systems agree on it. The parent project of this mission builds a certified-discovery pipeline for exact solutions of Einstein's equations in which a symbolic verifier is the oracle; this mission asks for the Kerr instance of that oracle's verdict to be re-established inside a proof assistant, so that the pipeline's benchmark result rests on a kernel-checked proof rather than on a simplification routine.
Timeline: Kerr (1963) found the metric in Kerr-Schild and in his original coordinates; Boyer and Lindquist (1967) introduced the coordinates $(t,r,\theta,\varphi)$ in which the metric below is written and described its maximal analytic extension; Carter (1968) established the separability structure that underlies the closed-form inverse. None of these results has, to the authors' knowledge, a machine-checked proof.
## Setting
Fix real parameters $M$ and $a$. A point of $\mathbb R^4$ is written $x=(x_0,x_1,x_2,x_3)=(t,r,\theta,\varphi)$; in Lean it is a function `Pt := Fin 4 → ℝ`. Write $s=\sin\theta$, $c=\cos\theta$ and
$$\Sigma := r^2+a^2\cos^2\theta,\qquad \Delta := r^2-2Mr+a^2 .$$
The **Boyer-Lindquist Kerr metric** is the symmetric $4\times4$ matrix of functions
$$g_{tt}=-\Big(1-\frac{2Mr}{\Sigma}\Big),\quad g_{rr}=\frac{\Sigma}{\Delta},\quad g_{\theta\theta}=\Sigma,\quad g_{\varphi\varphi}=\Big(r^2+a^2+\frac{2Mra^2\sin^2\theta}{\Sigma}\Big)\sin^2\theta,\quad g_{t\varphi}=-\frac{2Mar\sin^2\theta}{\Sigma},$$
with all other entries zero (signature $(-,+,+,+)$, $G=c=1$). Its **closed-form inverse** $\hat g$ has $\hat g^{rr}=\Delta/\Sigma$, $\hat g^{\theta\theta}=1/\Sigma$ and a $(t,\varphi)$ block with denominator $\Sigma\Delta\sin^2\theta$. The **regular coordinate domain** is
$$\mathrm{Reg}_{M,a}(x)\ :\Longleftrightarrow\ \Sigma\neq0\ \wedge\ \Delta\neq0\ \wedge\ \sin\theta\neq0 .$$
For any matrix of functions $g$ with candidate inverse $\hat g$, the **coordinate partial derivative** $\partial_i f(x)$ is the one-variable derivative at $u=x_i$ of the slice $u\mapsto f(x[i\mapsto u])$, and the **coordinate Christoffel symbols** and **coordinate Ricci tensor** are
$$\Gamma^a_{bc}=\tfrac12\sum_k\hat g^{ak}\big(\partial_c g_{kb}+\partial_b g_{kc}-\partial_k g_{bc}\big),\qquad R_{bd}=\sum_i\Big(\partial_i\Gamma^i_{bd}-\partial_d\Gamma^i_{bi}+\sum_j\big(\Gamma^i_{ij}\Gamma^j_{bd}-\Gamma^i_{dj}\Gamma^j_{bi}\big)\Big).$$
These four definitions (`pd`, `christoffel`, `ricci`, `ricciOf`) form the definition bundle `KerrBL_CoordGeometry`; the metric, its inverse and the regular domain form `KerrBL_Kerr_Metric`.
## Formalization targets
### Goal: Kerr vacuum theorem in Boyer-Lindquist coordinates (`KerrBL.vacuum_Kerr`)
For all real $M,a$ and every $x$ with $\mathrm{Reg}_{M,a}(x)$:
$$\sum_k\hat g^{ik}(x)g_{kj}(x)=\delta_{ij},\qquad u\mapsto g_{ij}(x[l\mapsto u])\ \text{and}\ u\mapsto\Gamma^i_{jk}(x[l\mapsto u])\ \text{are differentiable at } x_l,\qquad R_{bd}(x)=0\ \ \forall\,b,d .$$
The goal deliberately bundles the inverse identity and the two differentiability clauses with Ricci-flatness. Without the first, `ricciOf g ĝ` with a wrong $\hat g$ could vanish trivially; without the other two, the derivative in the definition of $R_{bd}$ could be Mathlib's default value $0$ at a non-differentiable slice. With them, the last clause is a statement about the genuine coordinate Ricci tensor.
### Supporting targets
The milestones follow the three layers of the proof: (I) the inverse identity; (II) the bridge from the generic definitions to explicit closed forms, through derivative certification of the metric, the Christoffel bridge, derivative certification of the generic Christoffel symbols, and the Ricci bridge $R_{bd}(x)=\mathrm{RicciKerr}_{bd}(x)$; (III) the vanishing of the explicit expression for each of the eight components that are not structurally zero, as rational identities in the seven variables $(M,a,r,s,c,S,D)$ under $s^2+c^2=1$, $S=\Sigma$, $D=\Delta$, and finally the vanishing of all sixteen generic components.
## Significance
The result itself is classical: the Boyer-Lindquist Kerr family is a vacuum solution wherever the coordinates are regular. What the mission adds is a proof in which the trusted base is explicit and small: a 45-line generic layer defining $\partial_i$, $\Gamma$ and $R$, and the transcription of five metric components from a hash-locked source file, with source-lock lemmas proving that the compact definitions equal the transcriptions. Everything else, including roughly 120 kB of generated closed forms, is bridged by proof; a wrong closed form can make a bridge theorem unprovable but never a false theorem provable. The generic layer and the bridge pattern are reusable for any coordinate metric in four dimensions, and the pattern of certifying a computer-algebra derivation through polynomial witnesses checked by `linear_combination` is reusable for any rational-function identity.
Status: the theorem is proved in the classical sense since 1963 and verified by every computer-algebra system; the machine-checked coordinate proof is what this mission records. At launch every node of the mission carries an accepted proof.
## Difficulty
The obvious argument is to compute. The difficulty is size and control, not ideas. The Ricci components of Kerr are rational functions whose numerators have up to a few hundred monomials in seven variables; a normalisation tactic applied to the raw expression does not terminate in practice, and a naive $\mathrm{simp}$-based unfolding of the double sums over $\mathrm{Fin}\,4$ produces terms whose elaboration alone exceeds the server budget. The proof therefore has to be organised: opaque atoms for $\Sigma$ and $\Delta$ so that denominators are monomials, per-term clearing lemmas over a common denominator, and a single polynomial identity per component certified by explicit quotient witnesses of the relations $s^2+c^2=1$, $S=\Sigma$, $D=\Delta$. Mathlib's derivative also needs care: `deriv` returns $0$ where a function is not differentiable, so every derivative used in the Ricci formula must be accompanied by a `HasDerivAt` witness, and the differentiability of the generic Christoffel symbols has to be transferred from their closed forms by a locality argument on the open regular domain.
## Formalization scope
The Lean representation commits to the following. Points are `Fin 4 → ℝ` with $0=t$, $1=r$, $2=\theta$, $3=\varphi$; there is no manifold, no chart, no periodicity of $\varphi$ and no range restriction on $r$. Derivatives are Mathlib's `deriv` of coordinate slices. The candidate inverse is data; its correctness is a theorem. The parameters $M,a$ are arbitrary reals: the mission proves Ricci-flatness of the Boyer-Lindquist Kerr family on the regular coordinate domain used by the formalization, not a global Lorentzian-manifold theorem and not a statement restricted to the black-hole regime $M>0$, $|a|\le M$. The axis $\sin\theta=0$ is excluded (the inverse carries $1/\sin^2\theta$) although the metric is smooth there; the loci $\Sigma=0$ and $\Delta=0$ are excluded. Nothing is asserted about signature, uniqueness, symmetry of $R_{bd}$ (all sixteen components are proved separately) or any coordinate-independent curvature quantity. A trivialising formalization is ruled out by the goal's first clause: the Ricci tensor of the specification layer takes the inverse as an argument, and the goal certifies that argument.
Independent blind read-back of the definitions and main statements, performed by a separate agent that saw only the Lean text, returned the following honest statement, recorded here verbatim: "For every pair of real numbers $M$, $a$ and every point $(t,r,\theta,\varphi)\in\mathbb R^4$ at which $r^2+a^2\cos^2\theta\neq0$, $r^2-2Mr+a^2\neq0$ and $\sin\theta\neq0$, all sixteen numbers $R_{bd}$ obtained by evaluating the explicit coordinate formula [...] vanish, where $g$ is the explicitly transcribed Boyer-Lindquist Kerr component matrix, $\hat g$ is an explicitly transcribed matrix that (by `ginv_mul_g_Kerr`, under the same hypothesis) satisfies $\hat g g=I$ at that point, and $\partial_i$ is Mathlib's one-variable `deriv` of the coordinate slice." The two should-fix findings of that read-back (inverse coupling; junk derivative values) are addressed by the first three clauses of the goal.
Infrastructure: three definition bundles (`KerrBL_CoordGeometry`, hand-written; `KerrBL_Kerr_Metric`, generated from the source file and human-auditable; `KerrBL_Kerr_ClosedForms`, generated and untrusted). Reusable beyond the mission: the generic layer, the locality lemma, and the bridge pattern. Natural extensions welcome after release: the two-sided inverse, the $a=0$ reduction to Schwarzschild, and curvature invariants such as the Kretschmann scalar.
## Selected references
- R. P. Kerr, *Gravitational field of a spinning mass as an example of algebraically special metrics*, Phys. Rev. Lett. 11 (1963) 237-238. https://doi.org/10.1103/PhysRevLett.11.237
- R. H. Boyer and R. W. Lindquist, *Maximal analytic extension of the Kerr metric*, J. Math. Phys. 8 (1967) 265-281. https://doi.org/10.1063/1.1705193
- B. Carter, *Global structure of the Kerr family of gravitational fields*, Phys. Rev. 174 (1968) 1559-1571. https://doi.org/10.1103/PhysRev.174.1559
- S. Chandrasekhar, *The Mathematical Theory of Black Holes*, Oxford University Press, 1983, Chapter 6.
- S. M. Carroll, *Spacetime and Geometry*, Cambridge University Press, 2019, Section 6.6.
24 thms1 active userReviewed
Captain: wesleyfei
Almost-Complex-to-Complex Conjecture in Real Dimension at Least SixOpen Problem
## Motivation
An **almost complex structure** gives every tangent space of a smooth manifold the linear algebra of a complex vector space, but it need not come from complex-valued coordinate charts. The gap between these two notions is a global differential-geometric question, not a change of terminology. Granja and Milivojević describe the following as “a major open problem in differential geometry”: whether every closed almost complex manifold of dimension at least six admits an integrable complex structure ([Introduction, p. 1](https://doi.org/10.3842/SIGMA.2022.093)). This mission records that question as an open conjecture, not as an established theorem.
### Timeline
- **1957:** Newlander and Nirenberg proved that an almost complex structure is integrable exactly when its Nijenhuis tensor vanishes, under the regularity assumptions in their theorem. This turns integrability into a nonlinear first-order differential condition rather than a consequence of the pointwise equation $J^2=-\mathrm{id}$ ([article](https://doi.org/10.2307/1970051)).
- **2014–2021:** Bryant’s account of Chern’s program still calls the existence of an integrable almost complex structure on $S^6$ open, while referring to the sphere’s well-known almost complex structure ([abstract](https://arxiv.org/abs/1405.3405)).
- **2022:** Granja and Milivojević state the broader closed-manifold question above and study the topology of spaces of almost complex structures on six-manifolds ([SIGMA article](https://sigma-journal.com/2022/093/)).
## Setting
Fix an integer $n\ge 3$. Let $M$ be a connected, compact, Hausdorff, second-countable smooth manifold without boundary and of **real dimension** $2n$. An almost complex structure on $M$ is a smooth field
$$
J_x:T_xM\longrightarrow T_xM
$$
of real-linear maps satisfying $J_x(J_xv)=-v$ for every $x\in M$ and $v\in T_xM$. This condition forces even real dimension, but by itself supplies no complex coordinate charts.
A **complex structure** of complex dimension $n$ is an atlas with values in $\mathbb C^n$ whose transition maps are complex differentiable. Such an atlas induces an integrable almost complex structure. The target concerns existence on the underlying smooth manifold: the complex structure obtained may induce a different almost complex structure from the supplied $J$. It does not claim that every chosen almost complex structure is integrable.
Here “closed” means compact and without boundary. Connectedness is explicit because it is part of the standing manifold convention in the cited 2022 source. The lower bound is on real dimension: $2n\ge 6$, equivalently $n\ge 3$.
## Formalization target
### Main open conjecture
For every $n\ge 3$ and every closed connected smooth real $2n$-manifold $M$,
$$
M\text{ admits a smooth almost complex structure}
\quad\Longrightarrow\quad
M\text{ admits a compatible complex atlas of complex dimension }n.
$$
“Compatible” means that the underlying real smooth structure of the complex atlas is smoothly equivalent to the given smooth structure on the same topological space. No claim of uniqueness, equality with the original atlas, or integrability of the supplied $J$ is made.
The real six-dimensional case is essential. Since $S^6$ carries an almost complex structure, the conjecture would imply that its underlying smooth manifold carries some complex structure. That special case remains unresolved; restricted nonexistence results, such as results imposing compatibility with a particular metric, do not decide the unrestricted existence question.
## Significance
A positive solution would replace a pointwise tangent-bundle reduction by genuine holomorphic coordinates for every manifold in the stated class. It would in particular settle the existence question for $S^6$. A negative solution would identify additional global obstructions to complex atlases that are invisible to the existence of an almost complex structure.
The formalization isolates a reusable smooth almost complex structure on top of Mathlib’s tangent-bundle and manifold APIs, while making the desired complex atlas explicit. This prevents the central distinction from being hidden inside an unconstrained predicate named “integrable.” It also exposes the compatibility between the original real smooth atlas and the real atlas underlying the complex charts, which future work on characteristic classes, Nijenhuis tensors, and concrete six-manifolds can reuse.
## Difficulty
The equation $J^2=-\mathrm{id}$ is fiberwise algebra. Integrability requires local complex coordinates whose overlaps are holomorphic, equivalently the vanishing condition identified by Newlander and Nirenberg. Smooth variation of $J$ does not make that differential condition automatic. Thus simply viewing each tangent space as a complex vector space does not construct a complex manifold.
The six-sphere shows why the dimension threshold cannot be treated as a routine stable-range simplification. Its known almost complex structure supplies the hypothesis in real dimension six, while no arbitrary complex atlas is known. Likewise, replacing the conclusion by a complex vector-space structure on each tangent fiber would merely repeat the hypothesis and would not address the open problem.
## Formalization scope
The namespace `AlmostComplexToComplex` uses Mathlib’s boundaryless Euclidean manifold model. `AlmostComplexStructure n M` contains a continuous real-linear map on every tangent space, the pointwise identity $J^2=-\mathrm{id}$, and smoothness of the induced self-map of the total tangent bundle. It contains no integrability field.
The main theorem assumes the real atlas is modeled on $\mathbb R^{2n}$ and concludes the existence of charts modeled on $\mathbb C^n$. Mathlib’s `IsManifold` condition over $\mathbb C$ at order one states complex differentiability of chart transitions. Two $C^\infty$ conditions on the identity map compare the original real atlas and the real manifold structure underlying the complex charts in both directions; an unrelated smooth structure therefore cannot satisfy the conclusion merely by being placed on the same carrier type.
This is a chart-level interface, not yet a development of analytic integrability theory. Mathlib at the pinned revision has no ready-made almost-complex/Nijenhuis package connecting the structure above to the Newlander–Nirenberg criterion. The target does not assert that the supplied $J$ is integrable or homotopic to the one induced by the resulting atlas. A dedicated $S^6$ milestone is also outside this minimal draft because faithfully constructing the standard sphere and its known almost complex structure would require additional sourced infrastructure; no surrogate special case is inserted.
## Selected references
- Gustavo Granja and Aleksandar Milivojević, *Topology of Almost Complex Structures on Six-Manifolds*, SIGMA 18 (2022), 093, Introduction, p. 1. [DOI](https://doi.org/10.3842/SIGMA.2022.093); [arXiv](https://arxiv.org/abs/2207.12946).
- August Newlander and Louis Nirenberg, *Complex Analytic Coordinates in Almost Complex Manifolds*, Annals of Mathematics 65 (1957), 391–404. [DOI](https://doi.org/10.2307/1970051).
- Robert L. Bryant, *S.-S. Chern’s Study of Almost-Complex Structures on the Six-Sphere*, arXiv:1405.3405v2 (2021 revision), abstract. [arXiv](https://arxiv.org/abs/1405.3405).
2 thms1 active userReviewed
Captain: xuanji
Strong Whitney embedding in dimension 2nResearch Paper
## Motivation: an intrinsic manifold in a fixed Euclidean space
A **smooth manifold** is a space that can be described locally by real coordinates, even when no single coordinate chart describes the whole space. Differential geometry works with these local descriptions, whereas an embedding realizes the entire space inside one Euclidean space without losing either its topology or its infinitesimal geometry. The **strong Whitney embedding theorem** supplies a dimension bound depending only on the dimension of the manifold. This mission targets the precise version selected by [LeanEval v1](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean), 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/whitney_embedding.toml)).
## 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
## 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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean)).
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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean)).
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](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean) and [manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/whitney_embedding.toml). 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](https://doi.org/10.2307/1969265). Historical attribution as recorded in the LeanEval manifest; no alternate statement from this reference replaces the benchmark goal.
16 thms3 active usersReviewed
Captain: t4v1
Thurston's Question 23: rational relations among hyperbolic volumesOpen Problem
## Motivation
In the last of the twenty-four questions that closed his 1982 survey
*Three-dimensional manifolds, Kleinian groups and hyperbolic geometry*
(Bull. Amer. Math. Soc. **6** (1982), 357–381), Thurston asked to "show that
volumes of hyperbolic $3$-manifolds are not all rationally related" (p. 380). Twenty-two of
the twenty-four have since been answered — geometrization by Perelman, tameness
by Agol and by Calegari–Gabai, the ending lamination conjecture by
Brock–Canary–Minsky, virtual fibering by Agol — and this one is among the two
that remain open.
Some rational relations are forced, and for a trivial reason: a
degree $n$ cover of a hyperbolic $3$-manifold has $n$ times its volume, so any
two commensurable manifolds have rationally related volumes. The question, which
remains open, is whether *every* rational relation arises
that way — equivalently, whether some two hyperbolic $3$-manifolds have
irrational volume ratio. Remarkably, not a single such pair is known.
## Setting
The bundle fixes the meaning of every term. Hyperbolic $3$-space is the upper
half-space $\{(x,y,z) : z > 0\}$. Its volume is Lebesgue measure with density
$z^{-3}$ — the Riemannian volume of the metric $(dx^2+dy^2+dz^2)/z^2$ written
out, so that no Riemannian machinery is required. The hyperbolic distance is
given by its closed formula
$$\cosh d(p,q) \;=\; 1 + \frac{|p-q|^2}{2\,p_3\,q_3}.$$
A Kleinian action is a free, properly discontinuous action by hyperbolic
isometries; the quotient is a complete hyperbolic $3$-manifold, discreteness and
torsion freeness being consequences rather than hypotheses. The volume of the
quotient is the measure of a fundamental domain, in the sense of Mathlib's
`MeasureTheory.IsFundamentalDomain`, and the set of volumes collects those that
are finite and positive.
Two conventions are stated rather than derived, and are worth flagging.
Isometries are not required to preserve orientation, so the set of volumes also
contains those of non-orientable quotients; this enlarges the set but not its
$\mathbb{Q}$-span, so neither goal is affected. And preservation of the
hyperbolic volume is a field of the structure rather than a consequence of
preserving the distance: it holds for every hyperbolic isometry, but deriving it
amounts to classifying $\mathrm{Isom}(\mathbb{H}^3)$, which is not the subject
of this mission.
## Formalization targets
The goal is that the volumes are not all rationally related: there are two of
them, $v$ and $w$, with $v \neq q w$ for every rational $q$.
Two milestones support it. The first is that passing to a subgroup of index $n$
multiplies the volume by $n$, a fundamental domain for the subgroup being the
union of $n$ translates of one for the whole group; this is the source of every
known rational relation, and it is why the question is phrased as it is. The second is that the set of volumes is nonempty — that some
finite-volume hyperbolic $3$-manifold exists at all — without which the goal
would be vacuously false rather than open.
A stronger form of the question, that the $\mathbb{Q}$-span of the set of
volumes is infinite dimensional, is also stated.
## Significance
The question is a geometric statement whose difficulty is arithmetic. For the
Bianchi groups of an imaginary quadratic field $F$, Humbert's formula gives the
covolume as $|\delta_F|^{3/2}\zeta_F(2)/4\pi^2$, so the ratio of two such
volumes is, up to explicit algebraic factors, a ratio of Dedekind zeta values at
$2$; and Neumann and Yang showed that the Bloch invariant of a hyperbolic
$3$-manifold lies in a subgroup of finite $\mathbb{Q}$-rank determined by its
invariant trace field, so that manifolds sharing an invariant trace field with a
single complex place, such as an imaginary quadratic one, have rationally
related volumes. Producing one irrational ratio therefore means
separating two such transcendentals — a statement of the same order of
difficulty as the irrationality of $\zeta(5)$. The value of formalizing the
question is not that it will be closed, but that its statement, and the
elementary relations that make its naive form false, are pinned down exactly.