The Monotonicity Theorem in O-Minimal Geometry 1: Monotonicity TheoremTextbook
## Motivation
An **o-minimal structure** is a setting in which every definable subset of the line is tame: a finite union of points and open intervals. This single axiom rules out oscillation, space-filling behavior, and other pathologies, and it makes one-variable definable functions tractable. The central consequence is the **Monotonicity Theorem**: every definable function on an interval is piecewise constant or strictly monotone and continuous, with only finitely many pieces.
The result originates in the work of Pillay and Steinhorn on o-minimality and is presented systematically in Lou van den Dries, *Tame Topology and O-minimal Structures*, Chapter 3 ([Cambridge University Press, 1998](https://doi.org/10.1017/CBO9780511529219)). A concise expository account is given in Mário Edmundo, *O-minimal structures* ([arXiv:math/0012051](https://arxiv.org/abs/math/0012051)). This mission formalizes the one-dimensional monotonicity theorem and its supporting lemmas in Lean 4 against Mathlib, as a verified entry point to o-minimal geometry.
## Setting
Let $R$ be a type equipped with a **dense linear order without endpoints** $D$: an irreflexive, transitive, trichotomous relation $D.\mathrm{lt}$ in which every strict inequality admits an interpolant and every element has strict predecessors and successors. Finite Cartesian powers are represented as coordinate tuples $\mathrm{Power}\,R\,n := \mathrm{Fin}\,n \to R$, with coordinate projections, deletion, and append operations defined explicitly.
An **o-minimal structure** $M$ over $D$ is a family $M.S\,n$ of collections of subsets of $\mathrm{Power}\,R\,n$, closed under finite unions and intersections, containing diagonals and the order relation, closed under products, coordinate reindexing, and existential projection, and satisfying the o-minimality axiom: every member of $M.S\,1$ is a finite union of points and open intervals. A **definable function** $f$ with domain $I$ and codomain $B$ is a dependent function on the corresponding subtypes whose domain, codomain, and graph are all members of $M$.
For $a < b$ in $\mathrm{Power}\,R\,1$, the **open interval** $(a,b)$ is the set of coordinate tuples whose single coordinate lies strictly between the two endpoint values, with endpoint variants allowing $-\infty$ and $+\infty$. A function is **strictly increasing** (respectively **strictly decreasing**) on $I$ when $x < y$ implies $f(x) < f(y)$ (respectively $f(y) < f(x)$) in the first output coordinate. **Continuity** at a domain point is the graph-based epsilon-delta predicate: $x$ belongs to $\mathrm{ContinuousPoints}\,D\,I\,G$ exactly when the graph $G$ meets every sufficiently small box around $(x, f(x))$ in the graph of a locally oscillation-free correspondence. Finiteness and infinitude of one-dimensional sets are expressed through first-coordinate listings.
## Formalization targets
### Goal — Monotonicity theorem
$$f : I \to B\ \text{definable},\ I\ \text{infinite} \implies \exists\, a = p_0 < p_1 < \cdots < p_k = b\ \text{with each}\ (p_i, p_{i+1})\ \text{good}.$$
An open cell $(p_i, p_{i+1})$ is **good** when $f$ restricted to $I \cap (p_i,p_{i+1})$ is constant, or strictly increasing and continuous there, or strictly decreasing and continuous there. The number $k$ of cut points is finite and depends on $f$, $a$, and $b$; no bound on $k$ is asserted.
### Supporting targets
$$I\ \text{definable and infinite} \implies I\ \text{contains a nonempty open interval}.$$
$$f\ \text{definable} \implies \text{each value fiber}\ f^{-1}(z)\ \text{is definable}.$$
$$\text{Either some value fiber is infinite or every value fiber is finite}.$$
$$f\ \text{definable on infinite}\ I \implies f\ \text{is constant or injective on some subinterval}.$$
$$f\ \text{injective and definable} \implies f\ \text{is strictly monotone on some subinterval}.$$
$$f\ \text{strictly monotone and definable} \implies f\ \text{is continuous on some subinterval}.$$
## Significance
*The result itself.* The Monotonicity Theorem is the foundation of one-dimensional o-minimal geometry. It implies that definable sets have finitely many connected components, that definable functions have finite limits at endpoints, and that higher-dimensional cell decomposition can proceed by induction on dimension. Without it, the correspondence between definability and geometric tameness remains unestablished.
*Formalizing it.* The classical proofs are known and appear in the references above; what is missing is a machine-checked version with explicit definability bookkeeping. This mission produces Lean 4 declarations for the order, interval, monotonicity, graph, and continuity predicates together with the theorem and its lemmas, all verified against the pinned Mathlib revision. The definability infrastructure (products, projections, fiber extraction) is reusable for subsequent cell-decomposition missions. Status honesty: the one-dimensional interval-extraction lemmas are machine-checked; the local constancy-or-injectivity lemma, the injective-to-monotone lemma, the finite-partition assembly, and the goal theorem itself remain open targets.
## Difficulty
The naive argument fixes a point and inspects nearby values, but definability does not by itself provide any neighborhood on which behavior is uniform. The fiber dichotomy illustrates the obstruction: knowing that each fiber $f^{-1}(z)$ is definable does not decide whether some fiber contains an interval or every fiber is finite, and the two cases require different constructions (a constancy interval versus an injective-selection interval). Similarly, injectivity alone does not yield monotonicity without partitioning the domain by local sign patterns and applying o-minimality to select a uniform pattern on a subinterval. Each step fails until the relevant definable set is exhibited and the one-dimensional interval lemma is applied to it.
## Formalization scope
Lean represents one-dimensional points as functions $\mathrm{Fin}\,1 \to R$, with order, intervals, and finiteness stated through the first coordinate. Definability is always the structure membership predicate $M.S\,n$, never an informal attribute. Continuity is the graph-based $\mathrm{ContinuousPoints}$ predicate applied to $\mathrm{FunctionGraph}\,f.\mathrm{toFun}$; a submission that discharges a continuity goal from the domain inclusion alone, or that replaces the continuity predicate by the domain set, does not satisfy the statement. The goal quantifies over cut points $p : \mathrm{Fin}\,(k+1) \to \mathrm{Power}\,R\,1$ with $p_0 = a$, $p_{\mathrm{last}} = b$, and strict increase at each step; the intervening sets $J$ are the open intervals determined by consecutive finite endpoints.
Contributions welcome: direct proofs of the open leaves (fiber definability, the finite-fiber injective-interval construction, the injective-to-monotone step, the finite-partition assembly), sharper statements with explicit endpoint bounds, and reusable o-minimal infrastructure beyond this mission. Out of scope: higher-dimensional cell decomposition, differentiability, and integration of definable functions.
## Selected references
- Lou van den Dries, Tame Topology and O-minimal Structures, London Mathematical Society Lecture Note Series 248, Cambridge University Press, 1998, Chapter 3. DOI: 10.1017/CBO9780511525919.
- Mário J. Edmundo, An Introduction to O-minimal Structures, 2000. arXiv:math/0012051.
32 thms1 active userReviewed
Captain: Lucas
Faithfulness of the Burau representation of B4Research Paper
## Motivation
In 1935 Werner Burau attached to every braid on $n$ strands a matrix over the ring of Laurent polynomials $\mathbb{Z}[t,t^{-1}]$. The resulting homomorphism $\rho_n : B_n \to \mathrm{GL}_n(\mathbb{Z}[t,t^{-1}])$ is the oldest and most studied linear representation of the braid group, and whether it is *faithful* — whether a nontrivial braid can act as the identity matrix — became one of the best known questions about braid groups.
The history is short and sharp:
* **1969** — Magnus and Peluso prove that $\rho_3$ is faithful, by a direct algebraic computation.
* **1991** — Moody proves $\rho_n$ is **not** faithful for $n \ge 9$.
* **1993** — Long and Paton improve this to $n \ge 6$.
* **1999** — Bigelow settles $n = 5$: $\rho_5$ is not faithful.
* This left exactly one open case, $n = 4$, which appears as Question 3.1 in Margalit's problem list for mapping class groups.
* **2026** — Bharathram, Birman and Brendle prove that $\rho_4$ **is** faithful ([arXiv:2607.05283](https://arxiv.org/abs/2607.05283)), closing the last case.
## Setting
Let $n \ge 1$. The braid group $B_n$ is taken here in Artin's presentation: generators $\sigma_1,\dots,\sigma_{n-1}$ subject to
$$\sigma_i\sigma_j = \sigma_j\sigma_i \quad (|i-j| \ge 2), \qquad \sigma_i\sigma_{i+1}\sigma_i = \sigma_{i+1}\sigma_i\sigma_{i+1}.$$
Let $R = \mathbb{Z}[t,t^{-1}]$. The **unreduced Burau representation** is the homomorphism
$$\rho_n : B_n \longrightarrow \mathrm{GL}_n(R), \qquad \sigma_i \longmapsto I_{i-1} \oplus \begin{pmatrix} 1-t & t \\ 1 & 0\end{pmatrix} \oplus I_{n-i-1},$$
i.e. the identity matrix altered only in the two rows and columns $i$, $i+1$. That these matrices satisfy the two families of braid relations — so that $\rho_n$ is well defined — is proved in the mission's definition file, together with the invertibility of each generator matrix (its inverse is the identity altered by the block $\begin{pmatrix} 0 & 1 \\ t^{-1} & 1-t^{-1}\end{pmatrix}$).
Equivalently, $\rho_n$ is the action of the mapping class group of the $n$-punctured disk $D_n$ on the relative homology $H_1(\widetilde{D_n}, \{\tilde p_*\})$ of the infinite cyclic cover determined by total winding number; this is the description used throughout the source paper.
A representation is **faithful** when it is injective.
## Target
The goal of the mission is the Main Theorem of the paper:
$$\rho_4 : B_4 \longrightarrow \mathrm{GL}_4(\mathbb{Z}[t,t^{-1}]) \ \text{ is injective.}$$
The milestones are three supporting results, each of which can be attacked independently:
1. **Theorem 4.1 (Magnus–Peluso).** $\rho_3$ is injective. The paper gives a new topological proof of this classical statement, and the same argument is the model for the four-strand case.
2. **Observation 2.1.** If a braid $\Phi \in B_n$ satisfies $\rho_n(\Phi) = I$, then its image under the standard inclusion $B_n \hookrightarrow B_{n+1}$ (add one unbraided strand) satisfies $\rho_{n+1}(\iota(\Phi)) = I$. The paper uses this to move a four-strand braid into $B_5$, where a parity obstruction can be applied.
3. **Long's criterion** ([Long 1986, Theorem 2.2], quoted in Section 1 of the paper). If $N \trianglelefteq B_n$ is nontrivial and not contained in the centre, and $\rho_n$ is injective on $N$, then $\rho_n$ is injective. This is what reduces the Main Theorem to faithfulness on the Brunnian subgroup $\mathrm{Brun}_4$.
## Significance
Faithfulness of $\rho_4$ closes the classification of the faithful Burau representations: $\rho_n$ is faithful exactly for $n \le 4$. It immediately gives faithfulness of the Jones representation of $B_4$ (Corollary 1.1 of the paper), since the Jones representation contains the reduced Burau representation as a summand. Beyond the statement itself, the kernel and the image of $\rho_n$ for $n \ge 5$ remain poorly understood, and the paper's disk-sequence and parity technology is proposed by its authors as a tool for that problem.
For formalization, essentially nothing of this is machine-checked today: Mathlib has neither braid groups nor the Burau representation. This mission puts in place a checked definition of $\rho_n$ over $\mathbb{Z}[t,t^{-1}]$ (including well-definedness and invertibility), and then asks for the mathematics. Even the three-strand case — Magnus–Peluso, known since 1969 — is not formalized anywhere, and it is the natural first target.
## Difficulty
The obvious approach fails in both directions. One cannot simply compute: a braid in the kernel would have to be found or excluded among infinitely many words, and no normal form for $B_4$ turns injectivity of $\rho_4$ into a finite check. Nor can one argue by a free-subgroup / ping-pong pattern, which is how *non*-faithfulness is proved for $n \ge 5$.
The source argument is topological. To a braid $\Phi$ one associates the arc $\beta = (\beta_*^3)\Phi$ and the sequence of punctured disks cut out by its intersections with a fixed arc $\alpha$; the Moody polynomial $M(\alpha,\beta) \in \mathbb{Z}[t,t^{-1}]$ then obstructs membership in the kernel provided no cancellation occurs among its monomials. Three-strand braids always satisfy the relevant parity condition; four-strand braids do not, and the paper repairs this by pushing a point-pushing braid $\Phi \in K_4$ into $B_5$ and applying Moody's theorem there. A complete formalization therefore needs curves on punctured disks, minimal position, and the Birman exact sequence — none of which exist in Mathlib. Contributions that build any of that infrastructure are as welcome as contributions to the statements themselves.
## Formalization scope
Conventions fixed by the Lean development:
1. $B_n$ is the abstract group given by Artin's presentation, with generators indexed by $\mathrm{Fin}(n-1)$ using truncated subtraction; the generator of index $i$ is $\sigma_{i+1}$. This is the already-published definition reused by the mission, so results proved here interoperate with other braid-group missions.
2. The representation is the **unreduced** Burau representation, of size $n \times n$, not the reduced $(n-1)$-dimensional one; the variable is written $t$ and the coefficient ring is $\mathbb{Z}[t,t^{-1}]$.
3. Faithfulness is stated as injectivity of the group homomorphism, not as triviality of the kernel on some subgroup, and it is the genuine homomorphism out of the presented group: the braid relations are verified for the Burau matrices in the definition file, so no statement here is vacuous or conditional on well-definedness.
4. Long's criterion is stated for all $n$; for $n \le 2$ its noncentrality hypothesis cannot be satisfied, so its content is the case $n \ge 3$ that the paper uses.
A complete development will additionally need: point-pushing subgroups and the Brunnian group $\mathrm{Brun}_4$, the Moody polynomial of a pair of arcs, and winding-number sequences. These are not yet formalized and are deliberately not part of the current statements; proposals for faithful formalizations of them are welcome in the mission discussion.
## Selected references
* V. Bharathram, J. S. Birman, T. E. Brendle, *The Burau representation is faithful for n = 4*, 2026, [arXiv:2607.05283](https://arxiv.org/abs/2607.05283).
* W. Magnus, A. Peluso, *On a theorem of V. I. Arnold*, Comm. Pure Appl. Math. 22 (1969), 683–692, [DOI:10.1002/cpa.3160220508](https://doi.org/10.1002/cpa.3160220508).
* D. D. Long, *A note on the normal subgroups of mapping class groups*, Math. Proc. Cambridge Philos. Soc. 99 (1986), 79–87, [DOI:10.1017/S0305004100063969](https://doi.org/10.1017/S0305004100063969).
* J. A. Moody, *The Burau representation of the braid group $B_n$ is unfaithful for large $n$*, Bull. Amer. Math. Soc. 25 (1991), 379–384, [DOI:10.1090/S0273-0979-1991-16080-5](https://doi.org/10.1090/S0273-0979-1991-16080-5).
* D. D. Long, M. Paton, *The Burau representation is not faithful for $n \ge 6$*, Topology 32 (1993), 439–447, [DOI:10.1016/0040-9383(93)90030-Y](https://doi.org/10.1016/0040-9383(93)90030-Y).
* S. Bigelow, *The Burau representation is not faithful for $n = 5$*, Geom. Topol. 3 (1999), 397–404, [DOI:10.2140/gt.1999.3.397](https://doi.org/10.2140/gt.1999.3.397).
7 thms2 active usersReviewed
Captain: Lucas
Algebraicity of Weil classes on abelian sixfolds of discriminant -1Research Paper
## Motivation
The Hodge conjecture predicts that on a non-singular complex projective variety $X$ every rational cohomology class of type $(p,p)$ is a rational linear combination of the classes of algebraic subvarieties of $X$. Abelian varieties are the oldest testing ground for the conjecture, and the hardest known classes on them were isolated by A. Weil. A $2n$-dimensional complex abelian variety $A$ is **of Weil type** for an imaginary quadratic field $K=\mathbb{Q}(\sqrt{-d})$ if $K$ embeds into $\mathrm{End}_{\mathbb{Q}}(A)$ in such a way that both eigenspaces of $\eta(\sqrt{-d})$ meet $H^{1,0}(A)$ in an $n$-dimensional subspace. Such an $A$ carries a distinguished two-dimensional space of rational $(n,n)$-classes, the **Weil classes**, which for a generic $A$ of Weil type does not lie in the subring generated by divisor classes. Weil classes are therefore the standard obstruction to the Hodge conjecture in low dimension: for abelian fourfolds the conjecture reduces to their algebraicity.
Timeline of the unconditional results on algebraicity of Weil classes:
- A. Weil (1977) constructed the classes and showed that the generic abelian variety of Weil type has a three-dimensional space of rational $(n,n)$-classes, spanned by $h^n$ and the two-dimensional Weil plane.
- C. Schoen (Compositio Math. 65 (1988) and its 1998 Addendum, Compositio Math. 114) proved algebraicity for fourfolds of Weil type with $K=\mathbb{Q}(\sqrt{-3})$ and arbitrary discriminant, for sixfolds with $K=\mathbb{Q}(\sqrt{-3})$ and trivial discriminant, and for fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$; a second proof of the last case is in B. van Geemen's survey (1994).
- K. Koike (Canad. Math. Bull. 47 (2004)) proved algebraicity for sixfolds with $K=\mathbb{Q}(\sqrt{-1})$ and discriminant $-1$, which yields fourfolds with $K=\mathbb{Q}(\sqrt{-1})$ and arbitrary discriminant.
- E. Markman (JEMS 25 (2023)) proved algebraicity for fourfolds, arbitrary $K$, and discriminant $1$.
- E. Markman, [arXiv:2502.03415](https://arxiv.org/abs/2502.03415), proves algebraicity for **sixfolds of discriminant $-1$ and every imaginary quadratic $K$**, and deduces the Hodge conjecture for all abelian fourfolds.
## Setting
Fix $g$ and present a $g$-dimensional complex torus by its first homology: a complex structure $J$ on $H_1(A,\mathbb{R})=\mathbb{R}^{2g}$ with $J^2=-1$, the lattice being $\mathbb{Z}^{2g}\subset\mathbb{R}^{2g}$. A **polarization** is a rational alternating form $E$ on $H_1(A,\mathbb{Q})=\mathbb{Q}^{2g}$ satisfying the Riemann relations $E(Jx,Jy)=E(x,y)$ and $E(x,Jx)>0$ for $x\neq 0$. Cohomology is $H^k(A,\mathbb{C})=\wedge^k H^1(A,\mathbb{C})$, realized as the alternating $\mathbb{C}$-multilinear forms on $H_1(A,\mathbb{C})=\mathbb{C}^{2g}$; a class is **rational** if its values on rational vectors are rational, and it has **type** $(p,q)$ if it is multiplied by $z^p\bar z^{q}$ under the scaling action $v\mapsto (\mathrm{Re}\,z)v+(\mathrm{Im}\,z)Jv$ of $z\in\mathbb{C}$. A **Hodge class** of degree $2p$ is a rational class of type $(p,p)$.
Let $g=2n$ and $K=\mathbb{Q}(\sqrt{-d})$ with $d>0$. A **polarized abelian $2n$-fold of Weil type** is such an $(A,E)$ together with a rational endomorphism $M=\eta(\sqrt{-d})$ of $H_1(A,\mathbb{Q})$ with
$$M^2=-d,\qquad MJ=JM,\qquad E(Mx,My)=d\,E(x,y),$$
the last condition saying that $\eta(k)$ multiplies the polarization class by the norm $\mathrm{Nm}(k)$, and such that each of the two eigenspaces $W,\overline{W}\subset H_1(A,\mathbb{C})$ of $M$ meets the $i$-eigenspace of $J$ in an $n$-dimensional subspace. The **Hodge–Weil classes** are the rational classes in
$$\widehat{HW}\;=\;\big(\wedge^{2n}W\;\oplus\;\wedge^{2n}\overline{W}\big)\cap H^{2n}(A,\mathbb{Q}),$$
equivalently the rational degree-$2n$ classes that vanish on every tuple of vectors containing both a vector of $W$ and a vector of $\overline{W}$.
The form $H(x,y)=E(Mx,y)+\sqrt{-d}\,E(x,y)$ is $K$-valued and hermitian on $H_1(A,\mathbb{Q})$, viewed as a $K$-vector space through $\eta$. The determinant of its Gram matrix in a $K$-basis lies in $\mathbb{Q}^{\times}$, and its class in $\mathbb{Q}^{\times}/\mathrm{Nm}(K^{\times})$ is the **discriminant** $\det H$ of $(A,\eta,h)$. Discriminant $-1$ means that this determinant equals $-(a^2+dc^2)$ for some rationals $a,c$ not both zero.
**Algebraicity** is not modelled abstractly. An abelian variety is tied to a genuine non-singular projective variety $X\subseteq\mathbb{P}^N$ by a *projective realization*: a smooth, $\mathbb{Z}^{2g}$-periodic immersion $u:\mathbb{R}^{2g}\to X$, surjective onto $X$ and injective modulo the lattice, whose differential intertwines $J$ with the complex structure of $\mathbb{P}^N$. A class $w\in H^{2p}(A,\mathbb{C})$ is algebraic when some de Rham class of $X$ whose periods over the $2p$-cycles swept out by rational vectors $\lambda_1,\dots,\lambda_{2p}$ equal $w(\lambda_1,\dots,\lambda_{2p})$ is a rational combination of cycle classes $\mathrm{cl}(Z)$ of irreducible subvarieties $Z\subseteq X$ of dimension $g-p$. Cycle classes, de Rham cohomology of a projective variety, $(p,q)$-types and Hodge classes are taken from the platform's `HodgeConjecture` bundle, which formalizes §1 of Deligne's Clay problem description.
## Formalization targets
### Goal — Theorem 1.5.1 of arXiv:2502.03415
$$\text{For every } d>0:\ \text{the Hodge–Weil classes of a polarized abelian sixfold of Weil type with CM by }\mathbb{Q}(\sqrt{-d})\text{ and discriminant }-1\text{ are algebraic.}$$
The statement fixes neither the field $K$ nor the sixfold: it quantifies over every $d>0$, every polarized abelian sixfold of Weil type of discriminant $-1$, and every projective realization of it.
### Milestone — Weil's plane of Hodge–Weil classes (§1.1)
$$\widehat{HW}\ \text{is a two-dimensional }\mathbb{Q}\text{-space, and each of its elements has type }(n,n).$$
### Milestone — Schoen's degeneration step (§1.6)
$$\text{Goal for all sixfolds of discriminant }-1\ \Longrightarrow\ \text{Hodge–Weil classes of every abelian fourfold of Weil type are algebraic,}$$
for every imaginary quadratic $K$ and every discriminant; this is the use made of Schoen's Proposition 10 (Compositio Math. 114 (1998)) in the paper.
### Milestone — Corollary 1.6.1
$$\text{The Hodge conjecture holds for abelian fourfolds.}$$
### Milestone — Lefschetz $(1,1)$
Divisor classes: every Hodge class in $H^2$ of a non-singular projective variety is algebraic. This is an already published platform statement, imported here as a reference, since the reduction in Corollary 1.6.1 uses the algebraicity of divisor classes.
## Significance
Weil classes are, by the results of Moonen–Zarhin (Duke Math. J. 77 (1995), Math. Ann. 315 (1999)), the only obstruction left in dimension four: for a simple abelian fourfold $H^{2,2}(A,\mathbb{Q})$ is spanned by quadratic expressions in divisor classes and by Weil classes, and the non-simple cases reduce to products treated by Ramón Marí (Collect. Math. 59 (2008)) and Moonen–Zarhin. The goal theorem therefore closes the Hodge conjecture for abelian fourfolds, the first dimension in which the conjecture for abelian varieties was open.
Formalizing it produces, first, a reusable Lean model of polarized abelian varieties, of complex multiplication of Weil type, of the Hodge–Weil plane and of the discriminant, tied to an honest notion of algebraic cohomology class through projective realizations. None of these objects exists in Mathlib today. The result itself is proved in the source preprint and has no machine-checked proof; the milestones below are equally unformalized, including the classical statements of Weil and Schoen that the paper's Corollary depends on.
## Difficulty
The naive attack — write down subvarieties whose classes span $\widehat{HW}$ — fails because Weil classes are not expressible through divisors: for a generic abelian variety of Weil type the Néron–Severi group is cyclic while $H^{n,n}(A,\mathbb{Q})$ is three-dimensional, so no product of divisor classes reaches the Weil plane. The source constructs instead a reflexive sheaf $\mathcal{E}$ on $X\times\hat X$, for $X$ the Jacobian of a genus-$3$ curve, whose characteristic class $\kappa(\mathcal{E})$ remains of Hodge type along all deformations of $(X\times\hat X,\eta,h)$ as a polarized abelian sixfold of Weil type, and deforms the pair over that moduli space using a semiregularity theorem for twisted sheaves. Each of these steps — Orlov's derived equivalence, spinor geometry of the Mukai lattice, semiregularity — is itself missing from Mathlib, which is why the milestone list stays on the Hodge-theoretic side of the argument rather than transcribing the sheaf-theoretic core.
## Formalization scope
Conventions the Lean development commits to:
1. Complex tori are presented by $(J,E)$ on $\mathbb{R}^{2g}$ with the lattice $\mathbb{Z}^{2g}$; the polarization form is rational rather than integral, which is the isogeny-invariant form of the Riemann relations.
2. Cohomology is the space of alternating multilinear forms on $H_1(A,\mathbb{C})$, i.e. invariant forms on the torus; a period over a lattice cube is used to compare it with the de Rham cohomology of a projective realization.
3. The Weil condition is imposed symmetrically on both eigenspaces of $\eta(\sqrt{-d})$, so it does not depend on the choice of convention for $H^{1,0}$ versus $H^{0,1}$.
4. Discriminant $-1$ is stated as the existence of a $K$-basis in which the Gram determinant of $H$ is $-\mathrm{Nm}(k)$; changing the basis multiplies the determinant by a norm, so the condition is basis-independent.
5. Algebraicity always refers to cycle classes of subvarieties of an actual projective variety, in the sense of Deligne's formulation, never to an abstract subspace of "algebraic" classes; in particular the goal cannot be satisfied by exhibiting a formal object, and the hypotheses are satisfiable — abelian varieties of Weil type of discriminant $-1$ exist for every $K$, and abelian varieties admit projective realizations.
A complete development needs, beyond what is drafted here: the spin representation of the Mukai lattice of an abelian $n$-fold, pure spinors and $K$-secant lines, Orlov's equivalence, Atiyah classes and semiregularity for twisted sheaves. Contributions establishing any of these, or proving the Hodge-theoretic milestones, are welcome.
## Selected references
- E. Markman, *Cycles on abelian $2n$-folds of Weil type from secant sheaves on abelian $n$-folds*, arXiv:2502.03415. https://arxiv.org/abs/2502.03415
- A. Weil, *Abelian varieties and the Hodge ring*, Collected Papers III, Springer 1980, 421–429.
- C. Schoen, *Hodge classes on self-products of a variety with an automorphism*, Compositio Math. 65 (1988), 3–32; *Addendum*, Compositio Math. 114 (1998), 329–336. https://eudml.org/doc/89880
- B. van Geemen, *An introduction to the Hodge conjecture for abelian varieties*, Lecture Notes in Math. 1594, Springer 1994, 233–252. https://doi.org/10.1007/BFb0094425
- K. Koike, *Algebraicity of some Weil Hodge classes*, Canad. Math. Bull. 47 (2004), 566–572. https://doi.org/10.4153/CMB-2004-055-3
- B. Moonen, Y. Zarhin, *Hodge classes and Tate classes on simple abelian fourfolds*, Duke Math. J. 77 (1995), 553–581. https://doi.org/10.1215/S0012-7094-95-07717-5
- B. Moonen, Y. Zarhin, *Hodge classes on abelian varieties of low dimension*, Math. Ann. 315 (1999), 711–733. https://doi.org/10.1007/s002080050333
- J. Ramón Marí, *On the Hodge conjecture for products of certain surfaces*, Collect. Math. 59 (2008), 1–26. https://doi.org/10.1007/BF03191179
- E. Markman, *The monodromy of generalized Kummer varieties and algebraic cycles on their intermediate Jacobians*, J. Eur. Math. Soc. 25 (2023), 231–321. https://doi.org/10.4171/JEMS/1199
- P. Deligne, *The Hodge conjecture*, Clay Mathematics Institute Millennium Prize Problem description, 2000. https://www.claymath.org/wp-content/uploads/2022/06/hodge.pdf
7 thms2 active usersReviewed
Captain: ryanshin
Smooth 4-dimensional Poincaré conjecture: foundations and reductionsOpen Problem
## Motivation
The **smooth four-dimensional Poincaré conjecture** asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of *K3 — A New Problem List in Low-Dimensional Topology*. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. [Baykur–Kirby–Ruberman, Problem 4.1](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf)
### Historical landmarks
- **1961:** Smale proved that a closed smooth manifold homotopy equivalent to a sphere of dimension at least five is homeomorphic to that sphere. This is not a theorem that all such smooth manifolds are diffeomorphic to the standard sphere. [Smale, Theorem A](https://www.math.uchicago.edu/~shmuel/tom-readings/Smale,%20PC.pdf)
- **1982:** Freedman established the topological four-dimensional Poincaré theorem: a topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to it. [Freedman, Theorem 1.6](https://www.maths.gla.ac.uk/~mpowell/1982_The%20topology%20of%20four-dimensional%20manifolds.pdf)
- **2026:** The *K3* problem list continues to distinguish this established topological result from the open smooth sphere problem. [Problem 4.1, pp. 191–192](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf)
## Setting
Let $S^4$ be the unit sphere in $ℝ^5$, with its standard stereographic smooth structure. A **homeomorphism** is a continuous bijection with continuous inverse; a **diffeomorphism** is a smooth bijection with smooth inverse. A **smooth atlas** is a collection of local Euclidean coordinates whose transition maps are smooth.
The manifold $M$ is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on $ℝ^4$. The given atlas is arbitrary: it is not defined by transporting the standard structure from $S^4$.
For a homeomorphism $e:N\to S^4$, let $\mathcal A_e$ denote the atlas transported from the standard sphere along $e$. A **structomorphism** for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate $\mathsf{SPC4Pullback}$ requires, for every given smooth atlas $\mathcal A$ on such an $N$ and every such $e$, a structomorphism between $(N,\mathcal A)$ and $(N,\mathcal A_e)$. It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, *SPC4.lean*, lines 53–81 and 211–221]
## Formalization targets
### Main open goal
For every manifold $M$ with the preceding hypotheses, the goal is
$$
M\cong_{\mathrm{Top}}S^4
\quad\Longrightarrow\quad
M\cong_{\mathrm{Diff}}S^4.
$$
This is the source predicate $\mathsf{SPC4}$. Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.
### Structural and literature milestones
The atlas formulation has the exact equivalence
$$
\mathsf{SPC4}\quad\Longleftrightarrow\quad\mathsf{SPC4Pullback}.
$$
The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence
$$
\operatorname{Structomorph}(\mathcal G^{\infty},M,N)
\simeq \operatorname{Diff}^{\infty}(M,N),
$$
where $\mathcal G^{\infty}$ is the smooth coordinate-change groupoid for the common model. [Shin, *SPC4.lean*, lines 334–365; *Bridge.lean*]
Write $F_4$ for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:
$$
M\simeq S^4\quad\Longrightarrow\quad M\cong_{\mathrm{Top}}S^4,
$$
where $\simeq$ denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If $\mathsf{SPC4Homotopy}$ denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:
$$
F_4\quad\Longrightarrow\quad
(\mathsf{SPC4}\Longleftrightarrow\mathsf{SPC4Homotopy}).
$$
Explicit standard-disk foundations form another track. For every $m\geq0$, they concern the manifold-with-boundary structure on $\overline B^{m+1}$, its boundary set $S^m$, and the smooth collar
$$
c:S^m\times[0,1]\longrightarrow\overline B^{m+1},
\qquad c(u,t)=(1-t/2)u.
$$
The collar is a closed embedding, has image
$$
\{z\in\overline B^{m+1}:\|z\|\geq1/2\},
$$
and satisfies $c(u,0)=u$, using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a $C^k$ map from a $C^k$ manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is $C^k$. These targets concern the actual disk smooth structure. [Shin, *Disk.lean*, lines 1076–1141 and 1263–1318]
### Topological two-disk gluing
For each integer $m\geq0$, let $D^{m+1}=\overline B^{m+1}$ be the closed unit disk in $\mathbb R^{m+1}$ and let $\varphi:S^m\to S^m$ be any homeomorphism of its boundary. The **twisted double** identifies the boundary point $u$ in a left copy of the disk with $\varphi(u)$ in a right copy. With the quotient topology, the target is
$$
X_\varphi:=\bigl(D^{m+1}_L\sqcup D^{m+1}_R\bigr)/(u_L\sim\varphi(u)_R)
\quad\cong_{\mathrm{Top}}\quad S^{m+1}.
$$
This statement is published as [SP4Gluing.twistedSphere_homeomorphic](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c). The theorem and its supporting [continuity](https://prove2.me/theorems/e09b0118-b3a4-44e3-9ba2-e70fb31a2faa) and [injectivity](https://prove2.me/theorems/12c0403c-fdcf-4202-8b53-9f12893b568f) lemmas have accepted Lean proofs contributed by [carlok](https://prove2.me/users/fca9fd8a-84f4-46ca-8845-a4a2b665381d). All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.
### Seam–interior smooth compatibility
For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth $\varphi^{-1}$; the reverse requires smooth $\varphi$. The [single compatibility target](https://prove2.me/theorems/f1e93fb9-c414-46aa-8b6c-fc6978243ee7) concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, *Hemisphere.lean*, lines 2439–3577]
## Significance
A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.
The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.
The [topological two-disk gluing result](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c) identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.
Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by [wamlart](https://prove2.me/users/70d2064f-6b47-4a3f-bb90-74e71a55cbb7): [orbit augmentation](https://prove2.me/theorems/85478003-b7db-44ef-be81-1c0fc5d7a8b4), [region homology budgets](https://prove2.me/theorems/e3d78c98-ef71-4b2a-a04a-7fd93fe9246f), [two-corner homology budgets](https://prove2.me/theorems/f6cc0221-29eb-4e8a-9649-8856b2954f2a), [the Laurent mass threshold](https://prove2.me/theorems/2d22450e-c4ce-4a0c-8829-b51d65e80eb5), and [mass-two positivity](https://prove2.me/theorems/988bc029-7a8a-43d7-9413-9e9cc3f86c24). No theorem currently connects their completion to a proof or disproof of $\mathsf{SPC4}$. They are exploratory tools, not established milestones in a proof of the main goal.
## Difficulty
A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.
Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.
## Formalization scope
The sphere goal quantifies over `Type` in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order $\infty$. Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.
The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every $m\geq0$, so their dimensions are $m+1\geq1$. The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.
The separate source assertion `SPC4Ball` is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.
## Selected references
- R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., *K3 — A New Problem List in Low-Dimensional Topology*, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. [Author PDF](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf).
- Michael Hartley Freedman, *The topology of four-dimensional manifolds*, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. [DOI](https://doi.org/10.4310/jdg/1214437136); [primary-article scan](https://www.maths.gla.ac.uk/~mpowell/1982_The%20topology%20of%20four-dimensional%20manifolds.pdf).
- Stephen Smale, *Generalized Poincaré's Conjecture in Dimensions Greater Than Four*, Annals of Mathematics 74 (1961), 391–406, Theorem A. [DOI](https://doi.org/10.2307/1970239); [primary-article scan](https://www.math.uchicago.edu/~shmuel/tom-readings/Smale,%20PC.pdf).
- Ryan Shin, *SPC4.lean*, *Bridge.lean* and *Disk.lean*, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: `b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc`, `e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302`, `889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e`.
- Ryan Shin, *Hemisphere.lean*, unpublished Lean source file, 2026, declaration `twistedSphereHomeoSphere`; source SHA-256 `c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828`. [Published topological two-disk gluing target](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c); the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.
60 thms5 active usersReviewed
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.