Duan–Wu–Zhou Fourth-Power Bound: omega < 2.37193Research Paper
## Motivation
The **matrix-multiplication exponent** measures how the arithmetic cost of multiplying square matrices grows with their dimension. An improvement in this exponent is relevant both to algebraic complexity and to algorithms whose running times depend on matrix multiplication. This mission formalizes a known improvement using the fourth power of the Coppersmith–Winograd tensor; it does not claim a new mathematical record.
Duan, Wu, and Zhou identify a loss that arises when constituent tensors are analyzed independently although some of their finer components can coexist inside a shared variable block. Their asymmetric-hashing method recovers part of this combination loss. The paper's headline result concerns the eighth power. Its separate fourth-power computation reports $2.371919$ in Table 3, printed page 78. The present target is the slightly weaker exact rational endpoint $2.37193$. [Duan–Wu–Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*](https://arxiv.org/abs/2210.10173v5).
## Setting
Fix an arbitrary field $K$. The **matrix-multiplication tensor** $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. Its tensor rank is the smallest number of pure tensors whose sum is that tensor. The existing Lean definition `matMulExp K` takes the infimum of $\log R(\langle n,n,n\rangle_K)/\log n$ over integers $n\ge2$, with the value $3$ at the two excluded small dimensions. This definition is reused without alteration.
A **restriction** applies a linear map separately to each of a tensor's three variable spaces. A **degeneration** allows polynomial families of such maps and takes an appropriate leading coefficient. The order of the Lean relation is target first: `Restrict A B` means that $A$ is obtained from $B$. A direct sum uses disjoint variable spaces; a collection of overlapping restrictions does not constitute a direct sum.
The **Coppersmith–Winograd tensor** $CW_q$ has border rank at most $q+2$. This mission fixes $q=5$ and uses the literal tensor $T=(CW_5\otimes CW_5)\otimes(CW_5\otimes CW_5)$, whose asymptotic-rank budget is $7^4=2401$. Its standard coordinate partition has 45 coarse components $T_{ijk}$ indexed by nonnegative integers $i+j+k=8$. Each coarse component consists of ordered products of square components, whose grades sum to $(i,j,k)$. [Duan–Wu–Zhou, Sections 3 and 6–8](https://arxiv.org/abs/2210.10173v5).
A **restricted-splitting value pair** consists of a lower value bound and a prescribed distribution on finer Z-variable blocks. In a tensor power, Z-blocks with the wrong empirical split distribution are removed before measuring value. Sixfold symmetrization, using all permutations of the three modes, is part of this definition. Keeping the scalar and discarding the prescribed distribution loses information required by the recursion. [Duan–Wu–Zhou, Definition 3.9, Equation (3), and Definition 8.1](https://arxiv.org/abs/2210.10173v5).
## Formalization targets
The goal is precisely
$$\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{237193}{100000}.$$
It has the same field quantification and exponent definition as the completed Schönhage and Stothers goals. Only the name and rational endpoint change. No distribution, optimizer, characteristic restriction, or unproved value bound is a hypothesis of this goal.
The supporting targets concern the literal fourth-power source; prescribed-splitting component values; the recursive and global extraction inequalities of Equations (34) and (25); an exact certificate for the released fourth-power computation; and the value-to-exponent implication of Theorem 3.2. The proof outline distinguishes stable formal statements from source-level tasks whose complete Lean interfaces still require development. It does not turn an unspecified certificate into an assumption that the desired extraction exists.
The compact milestone list contains four precise statements: the literal fine-to-coarse product restriction; the fourth-power asymptotic-rank bound; existence of a strict six-symmetrized value surplus; and the conditional implication from that surplus to the goal. Together with the root, these are five review items. The first, second, and fourth milestones are marked Proved. The surplus remains Open. An accepted root reduction links the surplus to the proved capstone; it is a proof sketch, not a proof of the exponent bound. Recursive component extraction and exact numerical certification remain substantial work inside that open target.
The planned internal parameter is $\tau=790643/1000000$. Thus $3\tau=2.371929<2.37193$. The substantive value obligation is a strict surplus over $2401$ for the actual fourth-power source, with asymptotic losses absorbed by choosing strict lower rates. The exact certificate must establish this surplus; neither its existence nor its numerical slack is presently claimed as proved.
## Significance
The result would extend the formalized Stothers endpoint $2.3737$ to an asymmetric fourth-power bound. More importantly, it would provide restricted-splitting interfaces that can support subsequent higher-power and more-asymmetric analyses. The mathematical improvement is already established in the cited paper. The task here is to reconstruct its argument with machine-checked statements, concrete tensor maps, and exact numerical bounds.
The earlier square and Stothers mission roots are marked Proved. Reusable infrastructure includes polynomial degenerations, tensor powers, direct-sum value witnesses, hashing and hole-repair lemmas, the literal fourth-power grading, and the final exponent bridge. Two additional literal fourth-power support/restriction bridges and an additive entropy certificate with directed-log inputs are also marked Proved. These statuses do not imply that the new restricted-value recursion or numerical witness is already formalized.
## Difficulty
The central difficulty is retaining the correct dependence between each value bound and its prescribed split distribution. The released fourth-power data contains consumer-specific copies of square value pairs. Equal coarse grades do not justify identifying their chosen distributions. The 21 positive fourth-power components use the six-region recursion, whereas the 24 components with a zero coordinate require the boundary merging argument. [Duan–Wu–Zhou, Equation (34), Section 7.3, and released implementation](https://osf.io/dta6p/).
Global hashing must additionally control competitors with the same marginals, shared Z-blocks, missing fine blocks, and subexponential losses. An isolated restriction into each constituent is insufficient to establish a simultaneous extraction. Numerical optimization presents a separate issue: floating-point normalization and approximate maximum-entropy computations are not exact feasibility or entropy proofs. Exact marginal constraints, positivity domains, and directed error bounds must all be checked.
## Formalization scope
The environment is pinned to Mathlib `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e` and Lean `v4.29.0-rc3`. The development reuses `TensorObj`, `MMObj`, `Degenerates`, `HasTauValueAtLeast`, the six-symmetrized value infrastructure, and `matMulExp`. All endpoint theorems remain uniform over arbitrary fields. Finite profiles use exact integer counts; rational distributions must have compatible unbounded lengths before an asymptotic statement is invoked. Real limiting rates are represented with explicit strict slack where the existing finite-witness predicate does not guarantee endpoint attainment.
No constant-valued replacement for tensor value, opaque witness carrying its desired conclusion, or external direct sum substituted for overlapping source blocks is admissible. New definitions must specify the actual coordinate projections and restrictions they represent. The authors' optimizer is used to find candidate data, not trusted as a proof oracle. Contributions to restricted-power semantics, consumer-specific square pairs, boundary merging, recursive extraction, exact entropy bounds, and source-to-exponent bridges are all directly relevant to the goal.
## Selected references
- Ran Duan, Hongxun Wu, and Renfei Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*, FOCS 2023. [Full paper, version 5](https://arxiv.org/abs/2210.10173v5).
- Duan–Wu–Zhou, accompanying optimization and verification code, including `power4_dup_2.371919.mat`. [Authors' release](https://osf.io/dta6p/).
- A. M. Davie and A. J. Stothers, *Improved Bound for Complexity of Matrix Multiplication*, Proceedings of the Royal Society of Edinburgh Section A 143(2), 2013. [DOI](https://doi.org/10.1017/S0308210511001646).
- Arnold Schönhage, *Partial and Total Matrix Multiplication*, SIAM Journal on Computing 10(3), 1981. [DOI](https://doi.org/10.1137/0210032).
## Motivation
A **strongly regular graph** with parameters $(n,k,\lambda,\mu)$ is a finite simple graph on $n$ vertices in which every vertex has exactly $k$ neighbours, every pair of adjacent vertices has exactly $\lambda$ common neighbours, and every pair of non-adjacent vertices has exactly $\mu$ common neighbours. For most parameter tuples the elementary counting and integrality conditions already decide existence; the interesting cases are those that survive every known feasibility test and still resist construction. The tuple $(99,14,1,2)$ is the smallest such case in the family $\lambda = 1$, $\mu = 2$, and its existence has been open for more than fifty years. John Horton Conway offered \$1000 for a resolution, as one of five problems posed at the 2014 DIMACS conference on Challenges of Identifying Integer Sequences ([Conway, *Five \$1,000 Problems (Update 2017)*](https://oeis.org/A248380/a248380.pdf)).
Timeline of the problem and of what is known about it:
- **1969/1971** — the parameter set is raised by Norman Biggs in his Southampton lectures (*Finite Groups of Automorphisms*, LMS Lecture Note Series 6, p. 111).
- **1973** — Berlekamp, van Lint and Seidel construct a strongly regular graph with parameters $(243,22,1,2)$ as the coset graph of the perfect ternary Golay code, settling one of the five feasible parameter tuples in this family.
- **1975** — the existence question appears as Problem 7 (attributed to J. J. Seidel) in R. K. Guy's problem list, *The Geometry of Metric and Linear Spaces*, Springer LNM 490, pp. 237–238; Conway had worked on it by then.
- **1984** — H. A. Wilbrink, [*On the $(99,14,1,2)$ strongly regular graph*](https://research.tue.nl/files/2449333/256699.pdf), shows that such a graph cannot be vertex-transitive: no group of automorphisms can act transitively on its 99 vertices.
- **1988** — Brouwer and Neumaier, [*A remark on partial linear spaces of girth 5 with an application to strongly regular graphs*](https://ir.cwi.nl/pub/1721), Combinatorica 8, 57–61.
- **2004** — Makhnev and Minakova, *On automorphisms of strongly regular graphs with $\lambda=1$, $\mu=2$*, Discrete Math. Appl. 14(2), and **2011** — Behbahani and Lam, [*Strongly regular graphs with non-trivial automorphisms*](https://doi.org/10.1016/j.disc.2010.10.005), Discrete Math. 311, 132–144: further restrictions on the possible automorphism groups.
- **2014/2017** — Conway's prize offer publicises the problem.
No graph with these parameters has been found, and no non-existence proof is known.
## Setting
Fix a finite vertex set $V$ and a simple graph $g$ on $V$ (irreflexive, symmetric adjacency $\mathrm{Adj}$). For vertices $v,w$ write $N(v) = \{u : \mathrm{Adj}(v,u)\}$ for the neighbourhood of $v$ and $N(v)\cap N(w)$ for the set of common neighbours. The graph $g$ is **strongly regular with parameters $(n,k,\lambda,\mu)$**, written $\mathrm{IsSRGWith}\ g\ n\ k\ \lambda\ \mu$, when
- $|V| = n$;
- $|N(v)| = k$ for every vertex $v$;
- $|N(v)\cap N(w)| = \lambda$ whenever $v$ and $w$ are adjacent;
- $|N(v)\cap N(w)| = \mu$ whenever $v \neq w$ are non-adjacent.
The case $\lambda = 1$ says that every edge lies in exactly one triangle — equivalently, the neighbourhood of each vertex induces a perfect matching, so such graphs are **locally linear**. The case $\mu = 2$ says that every non-adjacent pair is the pair of opposite corners of exactly one $4$-cycle. Conway's problem asks for $(n,k) = (99,14)$ with these two local conditions.
Counting paths of length two from a fixed vertex gives $k(k-\lambda-1) = (n-k-1)\mu$, which for $\lambda=1$, $\mu=2$ reduces to $2n = k^2 + 2$; with $k = 14$ this yields $n = 99$. Writing $A$ for the adjacency matrix, $I$ for the identity and $J$ for the all-ones matrix, strong regularity is equivalent to the matrix identity $A^2 = kI + \lambda A + \mu(J - I - A)$, which for $(99,14,1,2)$ reads $A^2 + A = 12I + 2J$; the eigenvalues of $A$ other than $k=14$ are then $3$ and $-4$, and integrality of their multiplicities ($54$ and $44$) is one of the feasibility conditions that $(99,14,1,2)$ passes.
## Formalization targets
### Goal
$$\exists\ \alpha,\ \exists\ g \text{ a simple graph on } \alpha,\quad \mathrm{IsSRGWith}\ g\ 99\ 14\ 1\ 2 .$$
The goal is Mathlib's own `proof_wanted conway_99` in `Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean`, stated verbatim: existence of a finite type carrying a strongly regular graph with parameters $(99,14,1,2)$. A resolution in either direction is welcome — a proof settles the existence half, and a proof of the negation settles the non-existence half; the platform records the two as proof and disproof of the same statement.
### Supporting targets
$$2n = k^2 + 2, \qquad k \text{ even}, \qquad k \in \{2,4,14,22,112,994\}$$
for every strongly regular graph with $\lambda = 1$, $\mu = 2$: the counting identity, local linearity, and the integrality restriction that cuts the family down to five non-degenerate parameter tuples.
$$\exists\, g,\ \mathrm{IsSRGWith}\ g\ 9\ 4\ 1\ 2, \qquad \exists\, g,\ \mathrm{IsSRGWith}\ g\ 243\ 22\ 1\ 2$$
the two members of the family that are known to exist: the $3\times 3$ rook's graph (the Paley graph on $9$ vertices) and the Berlekamp–van Lint–Seidel graph.
$$|E(g)| = 693, \qquad |\{\text{triangles of } g\}| = 231, \qquad A^2 + A = 12I + 2J, \qquad g \text{ not vertex-transitive}$$
structural consequences for a hypothetical $99$-graph, the last one being Wilbrink's theorem.
## Significance
A $(99,14,1,2)$ graph, if it exists, is a locally linear graph of maximal density in its parameter range and a partial linear space of girth $5$ with $99$ points and $231$ lines of size $3$; its existence would also produce new association schemes and new examples for the general classification of strongly regular graphs. A non-existence proof would be the first case in this family ruled out by anything other than the classical feasibility conditions, and would say something new about how far local conditions ($\lambda=1$, $\mu=2$) constrain global structure.
Nothing in this mission is presently formalized. Mathlib defines `SimpleGraph.IsSRGWith`, proves the counting identity `IsSRGWith.param_eq`, the complement rule `IsSRGWith.compl`, and the matrix identity `IsSRGWith.matrix_eq`, and records the $99$-graph problem as a `proof_wanted`. The supporting targets are of three kinds: results that are proved in the literature and only need formalizing (existence at $(9,4,1,2)$ and $(243,22,1,2)$; Wilbrink's non-vertex-transitivity; the integrality restriction on $k$); routine consequences that supply reusable infrastructure (edge and triangle counts, the spectral identity, evenness of $k$); and the goal itself, which is open mathematics.
## Difficulty
The obvious approaches fail for concrete reasons. Exhaustive search is out of range: the graph has $693$ edges among $\binom{99}{2} = 4851$ pairs, and no isomorph-free generation of locally linear graphs on $99$ vertices is feasible. Algebraic constructions are blocked by Wilbrink's theorem — the graph cannot be vertex-transitive, so it is not a Cayley graph and cannot be produced by the group-theoretic constructions that yield most known strongly regular graphs, including the two that work at $(9,4,1,2)$ and $(243,22,1,2)$. On the non-existence side, every classical feasibility test (the counting identity, integrality of the eigenvalue multiplicities, the Krein conditions, the absolute bound) is passed by $(99,14,1,2)$, so a proof of non-existence needs an argument that does not factor through the parameters alone.
## Formalization scope
All statements are phrased with Mathlib's `SimpleGraph.IsSRGWith` on a `Fintype` vertex type with `DecidableRel` adjacency, and use `Fintype.card`, `SimpleGraph.edgeFinset`, `SimpleGraph.cliqueFinset 3` (triangles as $3$-cliques), `SimpleGraph.adjMatrix` over $\mathbb{Z}$, and graph isomorphisms `g ≃g g` for automorphisms. The goal quantifies over `α : Type` together with a `Fintype α` instance, so the vertex set is finite by construction and the empty type does not satisfy the cardinality clause; the statement is therefore not vacuously satisfiable. Note that Mathlib's definition constrains $\lambda$ only through pairs that are actually adjacent and $\mu$ only through pairs that are actually distinct and non-adjacent, so degenerate small graphs (the one-vertex graph, $K_3$) do satisfy `IsSRGWith` with $\lambda = 1$, $\mu = 2$; the supporting statements carry the cardinality hypotheses ($0 < n$, $1 < n$) that exclude them where needed, and the degenerate degree $k = 2$ is listed explicitly in the classification of feasible degrees.
Infrastructure a complete development needs, and which is reusable beyond this mission: interface lemmas for counting common neighbours in a strongly regular graph; the spectral theory of the adjacency matrix (multiplicities of the two non-principal eigenvalues, and their integrality), which is the missing ingredient for the classification of feasible degrees; a Lean construction of the perfect ternary Golay code and its coset graph, for the $(243,22,1,2)$ case; and decision procedures for strong regularity of an explicitly given small graph, for the $(9,4,1,2)$ case. Contributions to any of these are welcome, as are partial non-existence results (for instance, restrictions on automorphisms of prime order) submitted as separate statements.
## Selected references
- N. Biggs, *Finite Groups of Automorphisms: Course Given at the University of Southampton, October–December 1969*, London Mathematical Society Lecture Note Series 6, Cambridge University Press, 1971, p. 111.
- E. R. Berlekamp, J. H. van Lint, J. J. Seidel, *A strongly regular graph derived from the perfect ternary Golay code*, in: A Survey of Combinatorial Theory, North-Holland, 1973, pp. 25–30.
- R. K. Guy, *Problems*, in: The Geometry of Metric and Linear Spaces, Springer Lecture Notes in Mathematics 490, 1975, pp. 233–244 (Problem 7, J. J. Seidel, pp. 237–238). [doi:10.1007/BFb0081147](https://doi.org/10.1007/BFb0081147)
- H. A. Wilbrink, *On the $(99,14,1,2)$ strongly regular graph*, in: Papers dedicated to J. J. Seidel, EUT Report 84-WSK-03, Eindhoven University of Technology, 1984, pp. 342–355. [PDF](https://research.tue.nl/files/2449333/256699.pdf)
- A. E. Brouwer, A. Neumaier, *A remark on partial linear spaces of girth 5 with an application to strongly regular graphs*, Combinatorica 8 (1988), 57–61. [doi:10.1007/BF02122552](https://doi.org/10.1007/BF02122552)
- A. A. Makhnev, I. M. Minakova, *On automorphisms of strongly regular graphs with $\lambda=1$, $\mu=2$*, Discrete Mathematics and Applications 14 (2004), no. 2. [doi:10.1515/156939204872374](https://doi.org/10.1515/156939204872374)
- M. Behbahani, C. Lam, *Strongly regular graphs with non-trivial automorphisms*, Discrete Mathematics 311 (2011), 132–144. [doi:10.1016/j.disc.2010.10.005](https://doi.org/10.1016/j.disc.2010.10.005)
- J. H. Conway, *Five \$1,000 Problems (Update 2017)*, OEIS. [PDF](https://oeis.org/A248380/a248380.pdf)
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).
Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem
## The problem of solving linear inequalities
The **linear feasibility problem** takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns
$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$
has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.
What "polynomial time" means here depends on the machine. In the **bit model** the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the **real-number model** the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations *and* polynomially bounded intermediate bit sizes — is called **strongly polynomial**. This mission fixes the real-number model precisely as a **Blum–Shub–Smale (BSS) machine** ([Blum–Shub–Smale 1989](https://doi.org/10.1090/S0273-0979-1989-15750-9)): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be **uniform**, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.
## Why it matters
For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — [Tardos (1986)](https://doi.org/10.1287/opre.34.2.250) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice ([Spielman–Teng 2004](https://doi.org/10.1145/990308.990310)).
For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century ([Smale 1998](https://doi.org/10.1007/BF03025291)), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.
## The question and what is known
$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$
The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).
*Lower bounds.* [Klee–Minty (1972)](https://link.springer.com/rwe/10.1007/978-0-387-74759-0_339) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by [Friedmann–Hansen–Zwick (2011)](https://doi.org/10.1145/1993636.1993675) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from [Kalai (1992)](https://doi.org/10.1145/129712.129759) and [Matoušek–Sharir–Welzl (1996)](https://doi.org/10.1007/BF01940877). On the interior-point side, [Allamigeon–Benchimol–Gaubert–Joswig (2018)](https://doi.org/10.1137/17M1142132) showed by tropical methods that log-barrier path following is not strongly polynomial, and [Allamigeon–Gaubert–Vandame (2022)](https://arxiv.org/abs/2201.02186) extended this to **every** self-concordant barrier: no interior-point method of that class can settle the question positively.
*Polynomial algorithms in weaker senses.* [Khachiyan (1979/80)](https://doi.org/10.1016/0041-5553(80)90061-0) proved LP feasibility is polynomial in the bit model via the ellipsoid method; [Karmarkar (1984)](https://doi.org/10.1007/BF02579150) and then [Renegar (1988)](https://doi.org/10.1007/BF01580724) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. [Megiddo (1984)](https://doi.org/10.1145/2422.322418) solved LP in linear time for every fixed dimension; [Tardos (1986)](https://doi.org/10.1287/opre.34.2.250) gave the combinatorial strongly polynomial class; [Vavasis–Ye (1996)](https://doi.org/10.1007/BF02592148) and [Dadush–Huiberts–Natura–Végh (2020)](https://arxiv.org/abs/1912.06252) replaced the bit size by condition measures of $A$ alone; [Ye (2011)](https://doi.org/10.1287/moor.1110.0516) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.
The central difficulty is visible in every positive result: each known iteration count is controlled by a *scale-dependent* quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What *is* already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission *Introduction to Linear Optimization IV*), the ellipsoid method with its volume-halving correctness theorem (*XI*), interior-point path following (*XII*), and self-concordance with the barrier method (*Convex Optimization VI*).
## A hierarchy of formalization targets
The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.
**Level 0 — the model works.** A uniform BSS program decides one-variable feasibility in linear time:
$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$
It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.
**Level 1 — the classical method is exponential.** On the Klee–Minty cube, Dantzig's rule admits a run of
$$2^n - 1 \text{ pivots}$$
from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.
**Level 2 — the bit model succeeds.** Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within
$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$
The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.
**Level 3 — the goal (open).** A uniform program with data-independent polynomial cost:
$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$
The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.
## Formalization scope
Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing `LinearOptimization` development over `Matrix (Fin m) (Fin n) ℝ`, with $\{x \mid Ax \ge b\}$ as `polyhedron A b`; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new `SmaleNinth` definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite `BSSProgram` terms under the fixed `encodeLP` input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.
The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.
## Selected references
- L. Blum, M. Shub, S. Smale, *On a theory of computation and complexity over the real numbers*, Bull. AMS 21(1):1–46, 1989. [DOI](https://doi.org/10.1090/S0273-0979-1989-15750-9)
- S. Smale, *Mathematical problems for the next century*, Math. Intelligencer 20(2):7–15, 1998. [DOI](https://doi.org/10.1007/BF03025291)
- V. Klee, G. J. Minty, *How good is the simplex algorithm?*, in Inequalities III, Academic Press, 1972, pp. 159–175.
- L. G. Khachiyan, *Polynomial algorithms in linear programming*, USSR Comput. Math. Math. Phys. 20:53–72, 1980. [DOI](https://doi.org/10.1016/0041-5553(80)90061-0)
- N. Karmarkar, *A new polynomial-time algorithm for linear programming*, Combinatorica 4:373–395, 1984. [DOI](https://doi.org/10.1007/BF02579150)
- J. Renegar, *A polynomial-time algorithm, based on Newton's method, for linear programming*, Math. Programming 40:59–93, 1988. [DOI](https://doi.org/10.1007/BF01580724)
- É. Tardos, *A strongly polynomial algorithm to solve combinatorial linear programs*, Oper. Res. 34(2):250–256, 1986. [DOI](https://doi.org/10.1287/opre.34.2.250)
- N. Megiddo, *Linear programming in linear time when the dimension is fixed*, J. ACM 31(1):114–127, 1984. [DOI](https://doi.org/10.1145/2422.322418)
- G. Kalai, *A subexponential randomized simplex algorithm*, STOC 1992. [DOI](https://doi.org/10.1145/129712.129759)
- O. Friedmann, T. D. Hansen, U. Zwick, *Subexponential lower bounds for randomized pivoting rules for the simplex algorithm*, STOC 2011. [DOI](https://doi.org/10.1145/1993636.1993675)
- D. A. Spielman, S.-H. Teng, *Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time*, J. ACM 51(3):385–463, 2004. [DOI](https://doi.org/10.1145/990308.990310)
- S. A. Vavasis, Y. Ye, *A primal-dual interior point method whose running time depends only on the constraint matrix*, Math. Programming 74:79–120, 1996. [DOI](https://doi.org/10.1007/BF02592148)
- Y. Ye, *The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate*, Math. Oper. Res. 36(4):593–603, 2011. [DOI](https://doi.org/10.1287/moor.1110.0516)
- X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, *Log-barrier interior point methods are not strongly polynomial*, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. [DOI](https://doi.org/10.1137/17M1142132)
- X. Allamigeon, S. Gaubert, N. Vandame, *No self-concordant barrier interior point method is strongly polynomial*, STOC 2022. [arXiv](https://arxiv.org/abs/2201.02186)
- D. Dadush, S. Huiberts, B. Natura, L. A. Végh, *A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix*, STOC 2020. [arXiv](https://arxiv.org/abs/1912.06252)
- D. Bertsimas, J. N. Tsitsiklis, *Introduction to Linear Optimization*, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the *Introduction to Linear Optimization* mission series).
- B. Korte, J. Vygen, *Combinatorial Optimization: Theory and Algorithms*, 6th ed., Springer, 2018, §4.1–4.5.
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.
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.
## Motivation: classify three-dimensional periodic symmetry
A **space group** describes the rigid motions compatible with a periodic spatial symmetry. The classification concerns possible symmetry types, rather than the size or shape of a particular drawing of a crystal. The classical three-dimensional numbers are 230, 219 when mirror-related types are identified, and 65 for the orientation-preserving subfamily. These are the three numbers recorded in [Oliver Knill’s survey, §94, “Crystallography,” p. 41](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Keeping their conventions separate matters: changing which coordinate transformations are allowed changes what counts as the same type.
The target is the known classification result selected by **LeanEval v1**, not an unsolved classification conjecture. Its authoritative specification is [the declaration `LeanEval.Geometry.SpaceGroupsProblem.space_groups`](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The accompanying [benchmark manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml) attributes the classification independently to Fedorov and Schoenflies in 1891. The work requested here is a machine-checked proof of that fixed statement.
## Setting: groups, transformations, and orientation
For a natural number $d$, let $E(d)=\mathbb R^d$ with its Euclidean inner product. A **Euclidean isometry** is an invertible affine distance-preserving transformation of this space. The objects being counted are subgroups $G$ of this full motion group. In the [benchmark’s definitions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), $G$ is **discrete** when, for every point $x$ and every real $\varepsilon>0$, the set of its elements satisfying $\operatorname{dist}(gx,x)\leq\varepsilon$ is finite.
Such a group is **crystallographic** when it also contains translations by the members of some linearly independent family of $d$ vectors. Translation by $v$ means exactly that the transformation sends every $x$ to $x+v$. These conditions specify the underlying groups directly; they do not start with a list of previously classified examples. Although the structure field containing the translation condition is called `cocompact`, its actual content is the existence of these independent translations, not a separately assumed compact quotient.
An **affine equivalence** between two groups is an invertible affine map whose conjugation carries the first group’s set of transformations onto the second’s. It need not be an isometry. An **orientation-preserving affine equivalence** additionally requires the determinant of that affine map’s linear part to be positive. Separately, an individual isometry preserves orientation when its own linear part has positive determinant. The **Sohncke subfamily** restricts the groups themselves: every element of a group must preserve orientation. This is distinct from restricting the map used to compare two groups, as explicitly distinguished by the [source definitions and notes](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean).
## Target: one conjunction, with all three exact counts
Write $C_{\mathrm{OP}}(d)$ for `crystallographicCountOP d`, $C(d)$ for `crystallographicCount d`, and $C_{\mathrm{OP,only}}(d)$ for `crystallographicCountOPOnly d`. They count, respectively, orientation-preserving affine classes of all crystallographic groups, arbitrary affine classes of all crystallographic groups, and orientation-preserving affine classes within the all-elements-orientation-preserving subfamily. The sole goal is
$$
C_{\mathrm{OP}}(3)=230\quad\land\quad C(3)=219\quad\land\quad C_{\mathrm{OP,only}}(3)=65.
$$
This is the [exact benchmark conjunction](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), in its original order. None of its three components is optional, and they are not separate theorem targets. There are no milestones or auxiliary theorem items.
## Significance: exact cardinalities for the underlying groups
The result gives finite and exact answers for the specified spaces of symmetry types, while retaining the distinction between orientation of a coordinate change and orientation of every symmetry in a group. The difference between 230 and 219 reflects the identification of mirror-related types described in [Knill, §94](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); the 65 count answers a different question, concerning the restricted subfamily. Neither a single count nor a list that silently merges the equivalence conventions establishes the full assertion.
The formalization would add a proof connecting these numerical claims to the actual groups and class subsets specified in Lean. The [benchmark source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) currently supplies the statement with an unproved placeholder. This draft likewise supplies a statement, not a proof or a claim that the benchmark is solved.
## Difficulty: a catalog is not a completeness theorem
A finite catalog can have 230 entries without representing every crystallographic group, and different entries can still represent the same affine class. Thus checking the length of a catalog alone does not establish the [source’s cardinality assertion](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The difficulty is the mathematical connection between concrete descriptions and all groups admitted by the definitions, with precisely the required equivalence relations. The restricted 65-count must also respect the condition on every group element, rather than just a label attached to an example.
## Formalization scope: preserve the benchmark model
The Lean representation is `EuclideanSpace ℝ (Fin d)`, with affine isometries and affine equivalences from Mathlib. The [three source counting functions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) use `Set.encard` in the extended natural numbers $\mathbb N\cup\{\infty\}$. More precisely, each counts the set of subsets obtained as the class of some admissible group; it does not count representatives with multiplicity. Consequently, the displayed finite equalities include finiteness, which is not assumed beforehand.
One reusable definition bundle contains exactly the source’s model spaces, translation and discreteness predicates, crystallographic-group subtype, orientation predicate, two conjugacy relations, and three counting functions. Their declarations are preserved, including definitions for every natural dimension; only the theorem fixes $d=3$. Definitions for group actions, affine conjugation, and these class subsets can be used independently of this particular count. Contributions must establish the fixed goal with these meanings. Replacing the groups by a hard-coded finite type, defining a count to be its desired answer, or importing an unproved classification into the definition bundle would not establish this target.
## Selected references
- LeanEval contributors; problem submitted by Kim Morrison. *LeanEval v1: 230 space groups*, statement revision 1, 2026, repository commit `296b7491ec989d21bcf8636a9a69231a1e5d1d25`. [Exact Lean source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean); [manifest with historical bibliography](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml).
- Oliver Knill. *Some Fundamental Theorems in Mathematics*, author-hosted expository survey, July 22, 2018; updated June 25, 2023. §94, “Crystallography,” p. 41. [Full text](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). This provides background for the three counts; the exact formal conventions are those of LeanEval above.
Lagarias criterion is equivalent to RHResearch Paper
## Motivation
The **Riemann hypothesis** concerns the zeros of a complex analytic function, yet it admits an equivalent formulation involving only positive integers, finite sums, the real exponential, and the natural logarithm. Jeffrey C. Lagarias established this formulation in *An Elementary Problem Equivalent to the Riemann Hypothesis* ([Theorem 1.1](https://arxiv.org/abs/math/0008177v2)). It connects the distribution of divisors of an integer with the analytic behavior of the zeta function. For number theorists and formalizers, the interest lies in making that connection precise without confusing an elementary statement with an elementary proof.
The objective is the known equivalence selected by LeanEval v1, not a resolution of RH. Lagarias's paper builds on results of Guy Robin concerning large values of the divisor-sum function; those results remain substantial parts of the formalization workload ([Lagarias, §3](https://arxiv.org/abs/math/0008177v2)).
## Setting
For a positive integer $n$, its **divisor sum** is
$$\sigma(n)=\sum_{d\mid n}d,$$
where the sum runs over positive divisors, including $1$ and $n$. Its **harmonic number** is
$$H_n=\sum_{j=1}^{n}\frac1j.$$
All inequalities below are inequalities of real numbers. The symbols $\exp$ and $\log$ denote the real exponential and natural logarithm. The **Euler–Mascheroni constant** is $\gamma=\lim_{n\to\infty}(H_n-\log n)$.
The **Riemann zeta function** is obtained by analytic continuation of $\sum_{m=1}^{\infty}m^{-s}$ from $\operatorname{Re}(s)>1$. RH asserts that its nontrivial zeros have real part $1/2$. The **Lagarias elementary criterion** in this mission is the assertion that $\sigma(n)\le H_n+\exp(H_n)\log(H_n)$ for every positive integer $n$. These conventions agree with the arithmetic quantities in [Lagarias, Problem E](https://arxiv.org/abs/math/0008177v2), with the precise equality-clause distinction stated below.
## Formalization targets
### Main goal: the exact LeanEval equivalence
$$\mathrm{RH}\quad\Longleftrightarrow\quad
\forall n\in\mathbb N,\;n>0\Longrightarrow
\sigma(n)\le H_n+\exp(H_n)\log(H_n).$$
There are no hypotheses on the goal theorem. The quantifier ranges over all positive integers, not a bounded test set or an unspecified tail. The benchmark uses a non-strict inequality and does not include an equality characterization. Lagarias's Problem E additionally requires equality only at $n=1$; the proof of the reverse implication in [Theorem 1.1, p. 8](https://arxiv.org/abs/math/0008177v2) uses the non-strict inequality alone. The stronger source formulation is therefore not silently substituted for the benchmark.
### Supporting targets from the paper
The milestone list records the following source statements, with their thresholds unchanged:
* Lemma 3.1: for $n\ge3$,
$$e^\gamma n\log\log n\le\exp(H_n)\log(H_n).$$
* Lemma 3.2: for $n\ge20$,
$$H_n+\exp(H_n)\log(H_n)\le e^\gamma n\log\log n+\frac{7n}{\log n}.$$
* The finite check in the proof of Theorem 1.1: the criterion holds for $1\le n\le5040$, with equality exactly at $n=1$.
* Proposition 3.1, attributed to Robin: assuming RH, for $n\ge5041$,
$$\sigma(n)\le e^\gamma n\log\log n.$$
* Proposition 3.2, attributed to Robin: if RH is false, some fixed $0<\beta<1/2$ and $C>0$ satisfy
$$\sigma(n)\ge e^\gamma n\log\log n+
\frac{Cn\log\log n}{(\log n)^\beta}$$
for arbitrarily large integers $n$.
All five are taken from [Lagarias, §3, pp. 6–8](https://arxiv.org/abs/math/0008177v2); the finite check is explicitly an unnumbered step, not a newly attributed lemma.
## Significance
The result identifies an exact arithmetic reformulation of RH. It does not make either side unconditional. A proof of the equivalence gives a bridge between statements in different mathematical languages; it does not certify the universal inequality merely because many instances can be checked. This distinction is central to the interpretation of [Lagarias's theorem](https://arxiv.org/abs/math/0008177v2).
The formalization would connect existing Mathlib definitions of the zeta function, divisor sums, harmonic numbers, and Euler's constant through a machine-checked argument. Reusable outputs include explicit harmonic/exponential comparisons, certified finite real inequalities, and formal versions of Robin's conditional and oscillation results. The mathematical results are known; this proposal supplies open formalization targets, not completed proofs. No accepted LeanEval result is claimed by creating or launching the mission.
## Difficulty
The elementary appearance of the criterion hides its main analytic requirements. Bounding the divisor sum crudely, or checking any finite number of integers, cannot establish the universal equivalence. The conditional upper bound and especially the quantitative oscillation theorem connect zeta zeros with unusually large divisor sums. They must be proved, not packaged as definitions or presumed available because the paper cites them ([Lagarias, Propositions 3.1–3.2](https://arxiv.org/abs/math/0008177v2)).
The oscillation statement requires uniform positive constants and arbitrarily large indices. Replacing it with one counterexample loses essential information. The bounded computation also requires rigorous control of exponential and logarithmic values: an ordinary floating-point loop is not a Lean proof. Beyond the listed milestones, completion still requires standard growth comparisons, threshold bookkeeping, and assembly of the two implications. The short length of the source's final argument should not be read as an estimate of total formalization effort.
## Formalization scope
The goal is `LeanEval.NumberTheory.riemann_hypothesis_iff_lagarias_elementary_criterion`, with type `RiemannHypothesis ↔ LagariasElementaryCriterion`. The criterion definition is copied from the benchmark. `σ 1 n` is natural-valued and cast to the reals; `harmonic n` is rational-valued and cast to the reals. RH remains Mathlib's predicate on `riemannZeta`, excluding negative even trivial zeros and the point $s=1$. No replacement axiom, hidden RH assumption, altered zeta function, or circular child restatement is permitted.
The goal excludes $n=0$ and includes $n=1$. Thresholds ensure positive logarithm arguments in the analytic milestones. The oscillation milestone expresses an infinite subset of the naturals as an unbounded set, retaining $n\ge3$; deletion of the finitely many smaller indices does not change the source's infinitude claim. Its real exponent is represented by `Real.rpow`, not natural exponentiation. Constants are chosen before the arbitrary cutoff.
The benchmark pins Lean 4.33.0 and Mathlib `6f1ef4e5dd604a435bddba4747b13970cd65d2a1`. The proposal targets Prove2me's supported Lean 4.33.1 environment, Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`. These environments are distinct; eventual benchmark credit requires the benchmark's own validation. Contributions to analytic infrastructure, source-faithful supporting results, and certified finite inequalities are welcome. The five milestones are an initial source-backed structure, not a claim that all required infrastructure is already present.
## Selected references
* Jeffrey C. Lagarias, *An Elementary Problem Equivalent to the Riemann Hypothesis*, American Mathematical Monthly **109** (2002), 534–543. [arXiv:math/0008177v2](https://arxiv.org/abs/math/0008177v2), posted 6 May 2001. The theorem, proposition, equation, and page numbers in this proposal refer to this nine-page arXiv version.
* Guy Robin, *Grandes valeurs de la fonction somme des diviseurs et hypothèse de Riemann*, Journal de Mathématiques Pures et Appliquées **63** (1984), 187–213. [Bibliography entry [18] in Lagarias](https://arxiv.org/abs/math/0008177v2). The milestone formulations are those explicitly reproduced and attributed in Lagarias's Propositions 3.1 and 3.2.
Erdős Problems 97 and 96: Convex Point Sets and Unit DistancesOpen Problem
# Motivation
The mission is to prove the combined open goal
$$
\text{Problem 97} \;\land\; \text{Problem 96}
$$
for finite point sets in strictly convex position in the Euclidean plane.
## Why Problems 97 and 96 belong together
Problem 97 gives the local step needed for Problem 96. Assume Problem 97. Every
nonempty convex-independent finite set then has a vertex with at most three
neighbors at each positive radius, in particular at radius $1$. Delete that
vertex and preserve convex independence. Apply the same step to every subset
created by deletion until no points remain.
Charge each unordered unit-distance pair to the first endpoint deleted. Each
deleted vertex receives at most three charges, so an $n$-point set determines
at most $3n$ unordered unit-distance pairs. This gives the Problem 96 bound
and therefore $O(n)$. The package uses this one-way dependency; it does not
seek a reverse implication.
# Setting
Let $A\subset\mathbb R^2$ be finite. Strict convex position is represented by
the upstream predicate `EuclideanGeometry.ConvexIndep`: every point of $A$ is
an extreme point of the convex hull of $A$. For $p\in A$, the pinned
multiplicity at radius $r>0$ counts points $q\in A$ with
$\lVert p-q\rVert=r$. Problem 97 asks for a point where no radius has four
such other points. Problem 96 counts unordered pairs at distance $1$, then
takes the supremum over convex-independent $n$-point sets.
The historical progression is part of the setting. Erdős’s 1946 paper posed an
earlier three-neighbor version. His 1987 account reports Danzer’s convex
nonagon in which every vertex has three equidistant witnesses, and asks about
four witnesses. Fishburn and Reeds’s 1992 work gives a 20-vertex convex
configuration with the same unit distance at every vertex, placing the local
question beside the unit-distance problem.
# Target
The Problem 97 target is the canonical statement that every nonempty finite
convex-independent $A$ has no four-equidistant-point property:
$$
\forall A,\quad A\ne\varnothing\;\to\;\operatorname{ConvexIndep}(A)
\;\to\;\neg\operatorname{HasNEquidistantProperty}(4,A).
$$
The Problem 96 target is the canonical asymptotic statement
$$
U_c(n)=O(n),
$$
where $U_c(n)$ is the supremum of the unordered unit-distance counts
determined by convex-independent $n$-point sets. The bound is asymptotic;
the Problem 97 route would give the stronger explicit bound $U_c(n)\le3n$
for every natural number $n$.
# Significance
The package records a formal proof route joining a pinned geometric obstruction
to a global extremal bound. A successful Problem 97 proof would immediately
settle Problem 96 with the explicit constant $3$, while preserving the
combinatorial meaning of the count. It also separates the historical
three-neighbor constructions from the still-open four-neighbor assertion.
# Difficulty
The source proof reduces Problem 97 to strong induction on $|A|$. Its counting
engine follows Dumitrescu's 2006 isosceles-count method, with the cap-witness
refinements used in the source attributed to Nivasch--Pach--Pinchasi--Zerbib
(2013). This engine forces every counterexample to have at least nine points; a
finite geometric analysis excludes exactly nine points; and the remaining step must
produce a removable vertex for every larger minimal counterexample. The
removable-vertex statement carries the induction hypothesis that every
strictly smaller nonempty convex 4-equidistant set is contradictory. That
large-cardinality geometric step remains open, so both headline targets remain
open. Finite computational certificates can support local cases but do not
replace the universal geometric statement.
# Counterexample routes
Problem 97 is open, so the mission also records the parallel negative route.
The source formalization calls a nonempty convex-independent
finite set with the four-equidistant property a
[`Problem97.IsCounterexample`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/a46894f6078319d3001d06310531df50af0f6bbd/lean/Erdos9796Proof/P97/UniversalProblem97.lean#L24-L29).
Constructing one such set would refute Problem 97 and therefore refute the
mission's affirmative conjunction, regardless of whether Problem 96 remains
true. The counterexample milestone keeps this resolution path visible beside
the nonexistence proof. A successful witness must use exact coordinates or
exact algebraic data from which Lean verifies both strict convex position and
the four-equidistant property; a numerical approximation or a realizable
incidence pattern alone is insufficient.
Problem 96 has its own negative route. Because its claim is asymptotic, one
finite convex configuration cannot refute it. A counterexample must instead
give convex-independent point sets at arbitrarily large cardinalities whose
unit-distance counts exceed every proposed linear constant. The mission tracks
this superlinear-family statement separately, together with a reduction from
it to the exact negation of Problem 96. This keeps both possible outcomes
visible: a direct or Problem-97-derived linear upper bound, and an explicit
family proving that no such bound exists.
# Formalization scope
The canonical source is pinned at commit
`757d852766f377f7c1a0ffeeef6d3526bc0cb7a4`. Source-repository exports are
[`Problem97.erdos97_rhs`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/UpstreamBridge.lean#L30)
and [`Problem96.erdos96_rhs`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/UpstreamBridge.lean#L96).
The source repository reports closed proofs of the conditional bridge to the $3n$ bound
([`unit_distance_pairs_bound_of_erdos97`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P96/EuclideanPeeling.lean#L273)),
the $|A|\ge9$ counting milestone
([`counterexample_card_ge_nine`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/Counting.lean#L95)),
and the exact nine-point exclusion
([`FiniteN9Closure`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/N9Endpoint/Closure.lean#L56)).
The large-cardinality milestone is
[`RemovableVertexOfLarge`](https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/RemovableVertexAxiom/RemovableVertexOfLarge.lean#L50),
with its minimality hypothesis retained. The current platform draft contains
statement-level sketches and no imported source proofs. Its definitions make
convex independence and the positive-radius condition explicit; no theorem is
assumed inside a definition. Singletons and two-point sets are included in
Problem 97, while Problem 96's counting definitions also include the empty set.
The source repository uses Lean `v4.27.0`; these mission statements target the
platform's `v4.33.1`. Source-proof transfer and revalidation remain separate work.
The Lean declarations and proofs are this project's own formalization. The
Dumitrescu and Nivasch--Pach--Pinchasi--Zerbib citations record mathematical
provenance; they do not indicate that a paper proof was imported or
machine-checked directly.
These source results establish the intended dependency graph: the P97 universal
root feeds low-unit-degree extraction, strong induction, and then the P96
supremum bound. The platform mission records those contracts and milestones;
it does not claim to have transplanted their proof bodies.
Planned milestones are the two canonical roots, their conditional bridge, the
`|A| ≥ 9` count, the `n = 9` exclusion, the `|A| > 9` removable-vertex step,
the documented Danzer nine-point three-neighbor example, the parallel goal of
constructing a Problem 97 counterexample, and the superlinear-family route to
a counterexample to Problem 96.
# References
- Erdős, *On Sets of Distances of n Points* (1946), [DOI](https://doi.org/10.1080/00029890.1946.11991674).
- Erdős, *Some Combinatorial and Metric Problems in Geometry* (1987), [scan](https://www.renyi.hu/~p_erdos/1987-27.pdf).
- Fishburn–Reeds, *Unit Distances Between Vertices of a Convex Polygon* (1992), [publisher record](https://www.sciencedirect.com/science/article/pii/092577219290026O).
- Dumitrescu, *On Distinct Distances from a Vertex of a Convex Polygon* (2006), [Springer record](https://link.springer.com/article/10.1007/s00454-006-1262-y); provenance for the source counting method.
- Nivasch–Pach–Pinchasi–Zerbib, *The Number of Distinct Distances from a Vertex of a Convex Polygon* (2013), [arXiv:1207.1266](https://arxiv.org/abs/1207.1266); provenance for the cap-witness refinements used by the source formalization.
Equality case for compressed convex functional calculusOpen Problem
## Motivation and history
Compressing an operator to a closed subspace keeps the information visible within that subspace but can discard interactions with its orthogonal complement. The **compression-rigidity question** asks whether a particular equality detects that no such interactions were present. Its inputs are two commuting positive contractions and an ordinary strictly convex function of two real variables. The issue is the equality case, not the existence of a general operator inequality for every convex function.
The question was contributed by Boris Bilich to the CUHK-Shenzhen AI Math Problems collection and added on June 1, 2026. The [original problem](https://rybindmitry.github.io/problems/2.html) asks about operators on a Hilbert space without imposing finite dimension. The first formal target in this mission treated matrices with supplied joint spectral data. That finite-dimensional declaration has a verified proof on Prove2Me, but it does not settle the unrestricted Hilbert-space question. The September 2026 correction restores arbitrary complex Hilbert spaces as the main target and preserves the earlier result as a supporting artifact.
## Setting
Let $H$ be a complete complex Hilbert space, and let $\mathcal B(H)$ be its algebra of bounded complex-linear operators. The multiplication $AB$ means composition, with $B$ acting first, and $A^*$ denotes the adjoint. A **positive contraction** $A$ is self-adjoint, satisfies $\operatorname{Re}\langle v,Av\rangle\geq0$ for every $v\in H$, and has operator norm at most one. Both zero and the identity are permitted.
Write $S=[0,1]^2$. Let $X,Y\in\mathcal B(H)$ be positive contractions satisfying $XY=YX$. Their **joint continuous functional calculus** assigns an operator $g(X,Y)$ to each continuous real function $g$ on $S$. It is characterized as a continuous unital real star-algebra homomorphism from $C(S,\mathbb R)$ to $\mathcal B(H)$ that maps the two coordinate functions to $X$ and $Y$. The domain has the uniform norm and the codomain the operator norm. The existence and uniqueness of this calculus follow from the standard joint spectral theorem; the relevant source is [Dereziński, Lemma 6.6, printed page 43](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43).
An **orthogonal projection** is an operator $P$ satisfying $P^*=P$ and $P^2=P$. The compressed operators $PXP$ and $PYP$ are still viewed as operators on the original space $H$, not as operators on a separately chosen finite-dimensional range. The question includes the additional hypothesis that these compressed operators commute. The original commutation of $X$ and $Y$ does not remove the need to state this hypothesis.
## Formalization targets
The main target is the entire compression implication from the source. Let $f:S\to\mathbb R$ be continuous and **strictly convex**: for distinct $x,y\in S$ and $0<t<1$, its value at $tx+(1-t)y$ is strictly less than $t f(x)+(1-t)f(y)$. For $X,Y,P$ as above, the question is whether
$$
P f(X,Y)P=P f(PXP,PYP)P
\quad\Longrightarrow\quad
PX=XP\ \text{and}\ PY=YP.
$$
Both outer projections on the right are part of the original assertion. There is no hypothesis that $f(0,0)=0$. Commutation of $P$ with each coordinate operator is exactly the reducing-subspace conclusion asked for in the [source](https://rybindmitry.github.io/problems/2.html).
The accompanying standard infrastructure target asserts that, for every commuting pair of positive contractions on $H$,
$$
\exists!\,\Phi:C(S,\mathbb R)\longrightarrow\mathcal B(H),\qquad
\Phi(x\mapsto x_0)=X,\quad\Phi(x\mapsto x_1)=Y,
$$
where $\Phi$ is continuous, unital, real-linear, multiplicative and star-preserving. This is the unit-square, real-valued-function specialization of [Lemma 6.6](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43), not a claim that this known theorem is a new research conjecture. Its Lean proof is a separate supporting obligation. The earlier two-dimensional milestone and the proved finite-dimensional capstone remain available; neither replaces the new main target.
## Significance
A positive resolution would show that exact preservation of one strictly convex functional-calculus value, under the specified commuting-compression hypothesis, forces both operators to preserve the projection's range and its orthogonal complement. A negative resolution would require an actual Hilbert space, operators and strictly convex function satisfying every hypothesis while at least one of the two reducing identities fails.
The formal development separates this research question from the standard spectral infrastructure needed to express it. The new main declaration is an open proof obligation. The joint-calculus existence-and-uniqueness declaration is also unproved in this contribution, although mathematically standard. Local compilation and server publication check the declarations' well-formedness; they are not proofs of either statement. Only the earlier finite-dimensional result is being reported here as already proved.
## Difficulty
Arbitrary bounded commuting self-adjoint operators need not have a joint eigenbasis. Consequently a matrix formulation that records finitely many joint spectral atoms cannot serve as the general operator model. The compressed pair may also have different spectral data from the original pair. The equality involves these two different functional calculi, with a projection on either side of each value.
Strict convexity in this question is ordinary scalar strict convexity on the square. Operator convexity, finite rank of the projection, compactness of the coordinate operators, and a multivariable operator Jensen inequality are not additional assumptions. Introducing any of them would change the requested question. The general formulation must also retain boundary cases rather than exclude them to simplify an argument.
## Formalization scope
The Lean model uses actual bounded complex-linear maps on an arbitrary complete inner-product space. It imposes no finite-dimensionality, separability, common-eigenbasis or nonzero-space assumption. It includes $P=0$, $P=I_H$ and the zero Hilbert space. The scalar field convention is complex; a real-Hilbert-space transfer is not separately formalized here.
The function is stored on the ambient real plane, but continuity, strict convexity and evaluation use only its restriction to $S$. Values outside $S$ are irrelevant, and continuity outside the square is not required. Thus storing an ambient function does not exclude any continuous function originally defined only on the square.
Joint evaluation is a total definition. If a representing continuous unital real star-algebra homomorphism exists, it chooses one for the operator pair and then evaluates the supplied function. Otherwise it returns zero. The separate existence-and-uniqueness target establishes that this fallback is inapplicable to commuting positive contractions and that the choice is immaterial. No field in the model assumes the compression-rigidity conclusion. The supporting standard theorem must also apply to the compressed pair using the original projection and positivity hypotheses, without adding representation existence as a new restriction on the main question.
The replacement definition and both statements were built at Lean 4.30.0 with supported Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, and their final versions received independent blind readbacks. Published older declarations and their proof identities are preserved. They should be cited with their finite-dimensional scope, not described as a solution of the arbitrary-Hilbert-space target.
## Selected references
- Boris Bilich, *Equality case for compressed convex functional calculus*, CUHK-Shenzhen AI Math Problems, Problem 2, added June 1, 2026. [Original statement](https://rybindmitry.github.io/problems/2.html).
- Jan Dereziński, *Bounded operators*, Warsaw University lecture notes, January 2007, Lemma 6.6, printed page 43. [Joint continuous functional calculus](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43).
Positive definite matrix integral inequalityOpen Problem
# Motivation
The source defines a two-variable integral on strictly positive-definite real matrices. Its numerator is the absolute bilinear form of A minus B on two unit vectors, while the denominator uses the quadratic forms of A and B. The desired inequality says that componentwise matrix addition is nonexpansive for this quantity, with the larger of the two input distances controlling the output. The surface measure normalization is immaterial because the same constant multiplies every distance.
This mission turns CUHK-Shenzhen AI Math Problem 1, **Positive definite matrix integral inequality**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
For every positive dimension and every four positive-definite matrices A, B, C, and D, prove d(A+B,C+D) is at most max(d(A,C),d(B,D)). The first milestone fixes dimension one, where the sphere and every matrix entry can be analyzed explicitly.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in matrix analysis, positive definite matrices, integral inequality. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
The absolute value prevents a direct cancellation argument, and the denominators couple each integration variable to a different matrix. Positive definiteness gives pointwise positivity but does not immediately compare the ratios after addition. A successful proof must find a convexity, change-of-measure, or projective-metric mechanism that survives the double integral.
## Suggested attack route
Promising routes include reducing by congruence to normalized matrices, studying the scalar inequality on each pair of directions, and interpreting the denominator as a density change on the sphere. The dimension-one case should reveal the sharp scalar inequality. Numerical experiments in dimensions two and three may identify equality cases, but the Lean proof must ultimately derive every bound from positivity and measurable integration.
## Formalization scope
The Lean model uses finite matrices, Mathlib positive definiteness, the canonical sphere measure obtained from polar decomposition, and an explicit iterated integral. It does not assume symmetry through an unchecked flag: positive definiteness is the Mathlib predicate. Integrability obligations and zero-denominator issues must be proved from positive definiteness.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
## Milestones
Establish the dimension-one specialization, including any exact evaluation of the two-point sphere integral needed by the proof.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on May 28, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original CUHK-Shenzhen problem](https://rybindmitry.github.io/problems/1.html)
## Motivation
Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.
## Timeline
- **1963.** Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show *any* norm admits a dimension-dependent bound $2d$, setting the theme: how much of the dependence on dimension is real?
- **1981.** Beck and Fiala ([Discrete Appl. Math.](https://doi.org/10.1016/0166-218X(81)90022-6)) prove degree-$t$ set systems have discrepancy at most $2t - 1$, by the floating-colors argument, and conjecture $O(\sqrt{t})$.
- **1980s.** Komlós poses the vector form — unit $\ell^2$-norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's *Ten Lectures* (1987) as the central open problem of the area.
- **1985.** Spencer ([Trans. AMS](https://doi.org/10.1090/S0002-9947-1985-0784009-0)) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
- **1998.** Banaszczyk ([Random Struct. Algorithms](https://doi.org/10.1002/(SICI)1098-2418(199810)12:4%3C351::AID-RSA3%3E3.0.CO;2-S)) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
- **2010–2016.** The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg ([STOC 2016](https://arxiv.org/abs/1605.02882)) give a polynomial-time algorithm matching Banaszczyk's bound.
- **2023.** Kunisky ([SIAM J. Discrete Math.](https://arxiv.org/abs/2111.02974)) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
- **2025.** Bansal and Jiang ([arXiv:2508.03961](https://arxiv.org/abs/2508.03961)) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.
## Setting
Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$. A **sign vector** is an $\varepsilon \in \{-1, +1\}^n$: one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$-th coordinate of the vector $v_i$, the **discrepancy** of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$, the $\ell^\infty$ norm of the signed sum. The **Komlós property at constant $K$** — `KomlosBound K` — says that *every* such family, in every $n$ and every $m$, admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.
Set systems embed as the special case of $0/1$-incidence matrices: if $A$ is an $m \times n$ matrix of $0$s and $1$s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.
## Formalization targets
### Goal — the Komlós conjecture
$$\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.$$
The goal fixes no value of $K$: any finite universal constant settles it, so the statement survives every improvement in the constant.
### Milestones — the known ladder
Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree-$t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$"; Kunisky's lower bound $K \ge 1 + \sqrt{2}$; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$.
## Significance
The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.
None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.
## Difficulty
Random signs lose: they give $\Theta(\sqrt{n})$, not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.
## Formalization scope
The Lean model commits to: vectors as `EuclideanSpace ℝ (Fin m)`, whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads `‖v i‖ ≤ 1`); the $\ell^\infty$ conclusion written coordinatewise as `∀ j, |∑ i, ε i * v i j| ≤ K`, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with `ε i = 1 ∨ ε i = -1`; and set systems as matrices `A : Fin m → Fin n → ℝ` with an entrywise $0/1$ hypothesis and column-degree counted by `Set.ncard`. Quantifier order matters everywhere: in `KomlosBound K` the constant is fixed *before* $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In `beck_fiala` the hypothesis $t \ge 1$ is required (the degree-$0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$. In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$.
Welcome contributions: any milestone in any order — `beck_fiala` and `komlos_implies_beck_fiala` are self-contained finite arguments and the natural entry points; `spencer_six_deviations` and `banaszczyk_bound` each import a major technique; `komlos_lower_bound` needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.
## Selected references
- J. Beck, T. Fiala, *"Integer-making" theorems*, Discrete Applied Mathematics 3 (1981). [doi:10.1016/0166-218X(81)90022-6](https://doi.org/10.1016/0166-218X(81)90022-6)
- J. Spencer, *Six standard deviations suffice*, Trans. Amer. Math. Soc. 289 (1985). [doi:10.1090/S0002-9947-1985-0784009-0](https://doi.org/10.1090/S0002-9947-1985-0784009-0)
- W. Banaszczyk, *Balancing vectors and Gaussian measures of n-dimensional convex bodies*, Random Structures & Algorithms 12 (1998). [doi link](https://doi.org/10.1002/(SICI)1098-2418(199810)12:4%3C351::AID-RSA3%3E3.0.CO;2-S)
- N. Bansal, D. Dadush, S. Garg, *An algorithm for Komlós conjecture matching Banaszczyk's bound*, FOCS 2016 / SIAM J. Comput. [arXiv:1605.02882](https://arxiv.org/abs/1605.02882)
- N. Bansal, H. Jiang, *Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk*, 2025. [arXiv:2508.03961](https://arxiv.org/abs/2508.03961)
- D. Kunisky, *The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant*, SIAM J. Discrete Math. 37 (2023). [arXiv:2111.02974](https://arxiv.org/abs/2111.02974)
- B. Chazelle, *The Discrepancy Method*, Cambridge University Press, 2000. [author's page](https://www.cs.princeton.edu/~chazelle/pubs/book.pdf)
Existence of complete sets of mutually unbiased basesOpen Problem
# Motivation
Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.
This mission turns CUHK-Shenzhen AI Math Problem 16, **Existence of complete sets of mutually unbiased bases**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.
## Suggested attack route
Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.
## Formalization scope
The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
## Milestones
Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original problem](https://rybindmitry.github.io/problems/16.html)
- [Durt et al., review of MUBs](https://arxiv.org/abs/1004.3348)
First-passage time of Brownian motion to an exponentially decaying boundaryOpen Problem
> **Submission hold — source-fidelity repair (2026-09-04).** The public goal restricts answers to elementary expression trees and is only a stronger subquestion. It does not formalize the source's broader special-function closed-form question. The existing published target is preserved, with this scope warning. Do not confirm or submit this version as a faithful formalization of the full source. The legacy mathematical target below is retained for traceability while the replacement is prepared.
# Motivation
A standard Brownian motion starts below the exponentially decaying boundary b(t)=b0 exp(-ct). The first time it crosses the boundary has a continuous density characterized by a generalized Abel--Volterra integral equation. The source asks for an explicit distribution, motivated in part by neuronal threshold models with a decaying refractory boundary.
This mission turns CUHK-Shenzhen AI Math Problem 13, **First-passage time of Brownian motion to an exponentially decaying boundary**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
Construct one expression in a fixed elementary language whose evaluation is a continuous nonnegative density on positive times, solves the Abel equation, and integrates to one. The language contains real constants, rational constants, arithmetic, exp, log, square root, trigonometric functions, and the normal density. The first milestone drops elementary representability and normalization and asks for a continuous nonnegative Abel solution.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in Brownian motion, first-passage times, stochastic processes, Volterra integral equations. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
Moving-boundary first-passage laws rarely have elementary closed forms. The Abel kernel is singular at the upper endpoint, and showing that a candidate equation solution is the actual passage density requires uniqueness and probability normalization. The capstone may be false under the selected expression language; a non-elementarity theorem would be a legitimate disproof of this precise formal target.
## Suggested attack route
Formalize existence and uniqueness for the Volterra equation using weakly singular kernels, then connect it to Brownian first passage. Explore transformations suggested by the exponential boundary, Laplace transforms, and iterative resolvent kernels. Symbolic or numerical calculations may reveal special-function rather than elementary structure. If so, characterize the required extension of the expression language and prove why the current language is insufficient.
## Formalization scope
The already-published goal uses finite elementary-expression trees with arithmetic, exp/log/sqrt, sin/cos and normal density. The source explicitly permits standard special functions beyond this language. Accordingly the published declaration is a stronger elementary-only subquestion, not a faithful replacement for the full closed-form question. It is preserved as an existing result; its proof or disproof must not be reported as settling every special-function formula. The Abel-solution milestone asserts only existence of a continuous nonnegative solution; uniqueness, normalization, and identification with the first-passage density remain separate obligations. A complete source-faithful replacement needs an agreed formula class or a concrete proposed formula, not an unrestricted function renamed a closed form.
## Milestones
For each positive boundary height and decay parameter, there exists a continuous nonnegative solution of the stated Abel equation on positive times. This node asserts existence only, not uniqueness, unit mass, or an elementary closed form.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original CUHK-Shenzhen problem](https://rybindmitry.github.io/problems/13.html)
Zhang–Si–Si: Corrected Resonant Almost-Periodic Poincaré–Treshchev PersistenceResearch Paper
## Motivation
The classical persistence problem asks which invariant tori of an integrable Hamiltonian survive a small perturbation. A resonance makes some internal angular frequencies vanish, and an **almost-periodic perturbation** introduces infinitely many additional forcing frequencies. Zhang, Si, and Si state a Poincaré–Treshchev persistence theorem for this combined regime: most lower-dimensional resonant tori associated with nondegenerate relative equilibria persist as infinite-dimensional invariant tori [in Theorem 2.7](https://doi.org/10.3934/dcds.2026043). The formal mission targets that headline result in corrected form. It retains the paper’s nonresonance, spatial-shell, and averaged-critical-point hypotheses, while making explicit the full frequency twist and reduced-frequency parameter chart used later in the paper but absent from the printed theorem statement.
## Setting
Let $n,m>0$ and $d=n+m$. The internal variables are $x\in\mathbb T^d$ and $y\in G\subset\mathbb R^d$, where $G$ is bounded and closed. The external forcing angles and their conjugate actions are $\theta\in\mathbb T^{\mathbb Z}$ and $J\in\ell^1(\mathbb Z;\mathbb R)$. The **suspended Hamiltonian** is
$$
\mathcal H_\epsilon(\theta,J,x,y)=
\sum_{j\in\mathbb Z}\omega_jJ_j+N(y)+\epsilon P(\theta,x,y,\epsilon).
$$
Here $N$ is real analytic near $G$. A primitive rank-$m$ resonance lattice is represented by an integer matrix $K_0=(K_1,K_2)$ with $\det K_0=1$, where the last $m$ columns generate the lattice. The adapted angles are $(\psi,\phi)=K_0^{\mathsf T}x$, with $\psi\in\mathbb T^n$ and $\phi\in\mathbb T^m$. Writing $\nabla N$ for the actual derivative of $N$, define
$$
O(g,G)=\{y\in G:K_2^{\mathsf T}\nabla N(y)=0\},
\qquad \Omega(y)=K_1^{\mathsf T}\nabla N(y).
$$
The **averaged potential** $h_0(\phi,y)$ is the zero external and zero $\psi$ Fourier coefficient of $P$ at $\epsilon=0$. A pair $(\phi,y)$ is associated and nondegenerate when
$$
\nabla_\phi h_0(\phi,y)=0,
\qquad \det D_\phi^2h_0(\phi,y)\ne0.
$$
Let $O_0$ be the subset of $O(g,G)$ admitting such a $\phi$, let $\Omega_0=\Omega(O_0)$, and trim in reduced-frequency coordinates:
$$
\Omega_\xi=\{\eta\in\Omega_0:\operatorname{dist}(\eta,\partial\Omega_0)\ge\xi\},
\qquad O_\xi=O_0\cap\Omega^{-1}(\Omega_\xi).
$$
The perturbation has the paper’s **spatial-shell Fourier expansion** over finite shells $A$ in a spatial structure $\mathcal S$. With
$[A]=1+\sum_{j\in A}\log^{\varrho}(1+|j|)$ for $\varrho>2$, each shell has a uniform analytic Fourier bound $B_A$, and $\sum_AB_Ae^{s[A]}<\infty$ for some $s>0$. Every nonzero admissible finite external mode $k$ satisfies
$$
|\langle k,\omega\rangle|\ge
\frac{\gamma}{\Delta([[k]])\Delta(|k|_1)},
$$
where $\gamma>0$, $[[k]]$ is the minimum shell weight containing its support, and $\Delta$ is a nondecreasing approximation function with $\Delta(0)=1$, $\log\Delta(t)/t\downarrow0$, and $\int_0^\infty\log\Delta(t)t^{-2}\,dt<\infty$.
## Target
Assume that $O_0$ is nonempty. On every sufficiently small trim $O_\xi$, require compactness and positive $n$-dimensional measure in the $\Omega$ chart, injectivity of $D(\nabla N)(y)$, an analytic lower-Lipschitz diffeomorphism $\Omega:O_\xi\to\Omega_\xi$, and nondegeneracy of every averaged critical point retained by the conclusion. Then, for every $0<\xi\le\xi_*$, there are $0<\epsilon_0\le1$, a rate $c(\epsilon)\to0$ as $\epsilon\downarrow0$, and closed measurable nonempty sets $\Lambda_\epsilon\subset O_\xi$ for $0<\epsilon\le\epsilon_0$ such that
$$
\operatorname{vol}_n\bigl(\Omega(O_\xi\setminus\Lambda_\epsilon)\bigr)
\longrightarrow0\qquad(\epsilon\downarrow0).
$$
For every $y\in\Lambda_\epsilon$ and every associated nondegenerate $\phi$, construct a topological embedding
$$
\iota_{\epsilon,y,\phi}:\mathbb T^{\mathbb Z}\times\mathbb T^n
\longrightarrow
(\mathbb T^{\mathbb Z}\times\ell^1)\times
(\mathbb T^d\times\mathbb R^d)
$$
that is analytic almost periodic with the same shell structure, is the image of the standard resonant torus under a local canonical transformation, is $c(\epsilon)$-close to that torus, and is invariant under $\mathcal H_\epsilon$ with rotation vector $(\omega,\Omega(y))$.
## Significance
The result combines three features that are usually separated: a positive-rank internal resonance, an infinite external frequency vector, and persistence for an asymptotically full-measure parameter set. It identifies the surviving object in the full suspended phase, including the external actions, rather than only in the finite internal fibre. The paper contains a proof of its printed theorem; the mission’s open work is a Lean proof of the corrected target. The correction exposes the parameter twist and chart assumptions on which the reduction and measure assertion depend, so a completed formalization would distinguish the theorem’s stated content from hypotheses needed to make that content mathematically controlled.
## Difficulty
Finite-dimensional Diophantine notation does not control infinitely many external modes: admissibility, support weights, and the decay of $\Delta$ must interact without leaving an empty mode class. Resonance also removes $m$ internal frequencies and replaces the original parameter set by a lower-dimensional surface. Its ambient Euclidean boundary is therefore unsuitable for a positive trim, and ordinary ambient volume is unsuitable for the majority statement. Finally, persistence must be expressed simultaneously as an invariant solution of the actual Hamilton equations, an analytic almost-periodic embedding, and a canonical equivalence in the suspended phase; any one of these conditions alone admits objects that do not express the theorem.
## Formalization scope
The Lean representation uses finitely supported integer external modes, a covering spatial structure, the literal shell-indexed norm, complex-neighborhood coefficient analyticity, and a separate absolute-summability guard for every infinite Fourier sum. Unit modes are provably admissible. The averaged potential, its gradient and Hessian, the internal frequency $\nabla N$, the resonant set, and the reduced-frequency map are transparent definitions. Nonemptiness of $O_0$, positive volume of every allowed $\Omega_\xi$, and nonempty $\Lambda_\epsilon$ rule out empty-set and zero-measure trivializations.
The formal target strengthens the printed assumptions only where the source’s reduction requires missing control: $D(\nabla N)$ is injective on the retained trim, and $\Omega$ is an analytic diffeomorphism there with a uniform lower Lipschitz bound. The boundary distance and excluded volume are both taken in the $n$-dimensional reduced-frequency chart. The word “Cantor” is represented by closedness, measurability, nonemptiness, and asymptotically full measure; perfectness and total disconnectedness are not additional targets.
The torus lives in a genuine $\ell^1$ external-action space. Its action component has one weighted-$\ell^1$-valued shell expansion, and the Hamiltonian pairing and external action velocity carry convergence guards. A local conjugacy is a homeomorphism between open neighborhoods, fixes $\theta$, is differentiable along all $\ell^1$ action directions and finitely supported external-angle directions, and preserves $\sum_jd\theta_j\wedge dJ_j+\sum_i dx_i\wedge dy_i$ on those cylinder directions. Reusable contributions include spatial-shell Fourier classes, approximation functions, reduced-manifold measure interfaces, weighted infinite canonical forms, and coordinatewise Hamiltonian invariance.
## Selected references
- Yuan Zhang, Wen Si, and Jianguo Si, *Poincaré–Treshchev Mechanism in Integrable Hamiltonian Systems Under Almost-Periodic Perturbations*, Discrete and Continuous Dynamical Systems **52** (2026), 32–69. [DOI: 10.3934/dcds.2026043](https://doi.org/10.3934/dcds.2026043). Main result: Theorem 2.7, journal p. 39 (PDF p. 8); spatial and nonresonance definitions: Definitions 2.2–2.4 and equations (5)–(7), journal pp. 35–38 (PDF pp. 4–7); reduction exposing the additional twist and parameter-change requirements: Lemma 3.2, journal pp. 41–43 (PDF pp. 10–12).
Symplectic Modules Free over an Abelian NilradicalResearch Paper
## Motivation
Polynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$ that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of [Chen--Tan](https://doi.org/10.1016/j.jalgebra.2026.02.022).
The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family $\tau(C,\Phi)$ carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.
## Setting
Fix $\ell\ge2$ and the complex symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$. The relevant maximal parabolic subalgebra has an **abelian nilradical** $\mathfrak n$. Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free $U(\mathfrak n)$-module can consequently be modeled on that polynomial ring.
The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar $C\in\mathbb C$ and a polynomial parameter $\Phi$. Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family $\tau(C,\Phi)$ realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.
## Formalization targets
### Common polynomial-module family
Prove that for every $\ell\ge2$ there is one generator presentation and one family
$$
(C,\Phi)\longmapsto \tau(C,\Phi)
$$
of $\mathfrak{sp}_{2\ell}(\mathbb C)$-representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that $\tau(C,\Phi)$ is a weight module exactly when $\Phi$ is constant, and the stated simplicity criterion outside the exceptional arithmetic set
$$
\left\{\frac{\ell+1}{2}-\frac{n}{2}:n\in\mathbb Z_{>0}\right\}.
$$
For exceptional $C$, prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family $\tau$.
## Significance
The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.
Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.
## Difficulty
The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.
The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.
## Formalization scope
The mission works over $\mathbb C$ with natural rank $\ell\ge2$. The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.
The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family $\tau$. Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's `sorry`. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.
## Selected references
- Yang Chen and Haijun Tan, *Simple $\mathfrak{sp}_{2\ell}(\mathbb C)$-modules which are free over an abelian nilradical*, Journal of Algebra 697 (2026), 341--372, Theorems 1.1--1.3 (formal Theorems 3.7, 3.8, 4.7, 4.9, and 5.2). [DOI](https://doi.org/10.1016/j.jalgebra.2026.02.022)
- G. Shen, foundational work on mixed-product constructions for modules over Lie algebras of Cartan type, cited in the source paper for the Shen--Larsson functor.
Orders of Harmonic Maps into Euclidean BuildingsResearch Paper
## Motivation
Harmonic maps into singular nonpositively curved spaces arise in geometric analysis, rigidity theory, and the study of group actions on buildings. Near a point in the domain, their infinitesimal growth is measured by an **order**, obtained from an Almgren-type frequency quotient. For smooth targets that order is tied to familiar Taylor expansion data. Euclidean buildings are instead assembled from Euclidean apartments along reflection walls, so a map can branch through a singular link and a priori might exhibit a much less controlled spectrum of homogeneities. Breiner and Dees prove that, for maps from surfaces, this spectrum is discrete and is governed by the finite rotational Weyl group of the building. The mission formalizes their headline classification theorem, Theorem 1.1 of [Breiner--Dees](https://doi.org/10.1007/s00526-026-03375-5).
The discreteness matters because frequency information is a basic input to stratification and regularity arguments for singular harmonic maps. A finite list of possible denominators prevents homogeneities from accumulating arbitrarily and isolates rank-one behavior. The formal target makes explicit the nonconstant condition used by the source paper's tangent-map reduction. Without it, the usual numerator and denominator of the frequency quotient both vanish for a constant map, so its order is not defined.
## Setting
A **Euclidean Coxeter complex** consists of Euclidean space together with an affine reflection group. Taking the linear parts of its affine isometries produces a finite rotational reflection group $W$. A **Euclidean building of type $W$** is a complete metric space covered by isometric Euclidean apartments whose overlaps are related by elements of the affine Weyl group; the atlas is required to contain the relevant geodesic segments, rays, and lines and to be maximal with these compatibility properties.
The domain is a connected open subset $D$ of a complex one-dimensional manifold, hence a Riemann surface domain. The formalization uses a concrete Korevaar--Schoen-style metric Sobolev energy built from normalized local difference quotients and Lebesgue area in charts. A map $u:D\to X$ is harmonic when it has finite local energy and minimizes that energy against competitors with the same trace. For $x_0\in D$ and small radii $r$, the energy and boundary moment determine a frequency quotient. When its limit exists with positive denominator, that limit is the order $\operatorname{Ord}_u(x_0)$.
## Formalization targets
### Main classification
For a nonconstant energy-minimizing harmonic map $u:D\to X$ and any $x_0\in D$, prove that the order is defined and that there are positive integers $m,k$ such that
$$
\operatorname{Ord}_u(x_0)=\frac{m}{k},
\qquad k\mid |W|.
$$
If the building has rank one, prove the sharper form
$$
\operatorname{Ord}_u(x_0)=\frac{m}{2}
\qquad\text{for some integer }m\ge 2.
$$
The same theorem also records the small-scale energy and positive-boundary-moment facts needed for the order to be meaningful; these are conclusions, not assumptions supplied by a solver.
## Significance
The result identifies a purely algebraic constraint on an analytic singularity invariant: every denominator divides the order of the finite rotational Weyl group. In rank one, where the target is a tree or an $\mathbb R$-tree, it recovers the half-integer spectrum and its lower bound. This converts an apparently continuous local invariant into a discrete one determined by the building type.
Formalizing the theorem requires reusable infrastructure that is largely absent from current Mathlib: concrete Euclidean-building atlases, metric-valued Sobolev energy, trace and boundary-moment constructions, harmonic energy minimization, frequency quotients, and homogeneous tangent-map interfaces. The paper theorem is proved in ordinary mathematics; the open task is to replace the single `sorry` in the target with a machine-checked Lean proof. A completed development would provide components useful for other singular-target harmonic-map and CAT(0) formalizations.
## Difficulty
The target is not a direct consequence of treating the building as a Euclidean vector space. A harmonic map can cross apartment walls, and a single chart need not contain the image of a punctured neighborhood. The local problem must respect both metric energy and Weyl-group compatibility. Moreover, the frequency quotient is defined through limiting analytic quantities, while the conclusion is an exact rational arithmetic classification. Bridging those levels requires controlling tangent maps and the geometry of directions in the building rather than merely proving monotonicity of the frequency.
The rank-one clause is not obtained by substituting $|W|=2$ into the general statement alone: it also asserts $m\ge2$. The formal proof therefore must preserve the nonconstant hypothesis and the positivity information that rules out the degenerate zero-order case.
## Formalization scope
The Lean bundle fixes a complex one-dimensional manifold model for the source, a genuine complete metric target, a finite affine reflection group acting by Euclidean isometries, and an explicit building atlas. The rotational group $W$ is the image of the affine group under taking linear parts, so $|W|$ is not an arbitrary external number. The domain carries a point $x_0$ and is nonempty by construction. The map is required to be nonconstant on the domain; this is the necessary explicit repair of the printed headline, whose later reduction theorem uses the same condition.
Energy, trace, boundary moment, frequency, and order are transparent definitions tied to the supplied geometry. In particular, the caller cannot choose a zero measure or an unrelated predicate to make the target vacuous. The theorem must establish finite small-scale energy, positivity of the boundary moment, existence of the frequency limit, and its classification. Solvers may contribute supporting files for metric Sobolev estimates, tangent-map compactness, homogeneous harmonic-map classification, or finite-reflection-group lemmas, provided they preserve the exact conventions in the definition bundle.
## Selected references
- Christine Breiner and Ben K. Dees, *On the Possible Orders of Harmonic Maps into Euclidean Buildings*, Calculus of Variations and Partial Differential Equations, 2026, Theorem 1.1 and Sections 2--4. [DOI](https://doi.org/10.1007/s00526-026-03375-5)
- Mikhail Gromov and Richard Schoen, *Harmonic Maps into Singular Spaces and p-adic Superrigidity for Lattices in Groups of Rank One*, Publications Mathématiques de l'IHÉS 76 (1992), 165--246. [EuDML](https://eudml.org/doc/104049)
Arbitrary Torsion in Moment-Angle Homology and Loop HomologyResearch Paper
## Motivation
Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial $4$-sphere.
This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.
## Setting
Let $L$ be an abstract simplicial complex on a finite vertex set $[m]$. Its geometric realization $|L|$ is formed from probability vectors whose supports are faces of $L$. The condition that $L$ is a **simplicial $4$-sphere** means that this realization is homeomorphic to the unit sphere $S^4\subset\mathbb R^5$.
For each face $\sigma\in L$, assign a copy of the closed disk $D^2$ at vertices in $\sigma$ and the boundary circle $S^1$ at vertices outside $\sigma$. The associated moment-angle complex is
$$
\mathcal Z_L
=\bigcup_{\sigma\in L}
\prod_{i=1}^{m}Y_i(\sigma),
\qquad
Y_i(\sigma)=
\begin{cases}
D^2,&i\in\sigma,\\
S^1,&i\notin\sigma.
\end{cases}
$$
The all-ones point is a canonical basepoint. Write $\Omega\mathcal Z_L$ for the based loop space with the compact-open topology. For a space $X$, the mission uses total integral singular homology
$$
H_*(X;\mathbb Z)=\bigoplus_{q\ge0}H_q(X;\mathbb Z)
$$
as an additive abelian group. Saying that an abelian group $G$ is a subgroup means that there is an injective additive homomorphism $G\hookrightarrow H_*(X;\mathbb Z)$.
## Formalization targets
### Arbitrary torsion in one moment-angle manifold
For every finitely generated abelian group $G$, prove that there are an integer $m$ and a simplicial complex $L$ on `Fin m` such that $|L|\cong S^4$ and there are injective homomorphisms
$$
G\hookrightarrow H_*(\mathcal Z_L;\mathbb Z),
\qquad
G\hookrightarrow H_*(\Omega\mathcal Z_L;\mathbb Z).
$$
The quantifier order matters: the same $m$ and the same $L$ must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.
## Significance
The theorem gives a universality statement for moment-angle manifolds over simplicial $4$-spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single $L$ connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.
Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.
## Difficulty
The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.
There is also a substantial representation boundary between combinatorics and topology. The face data of $L$, the union of disk-circle products, the homeomorphism $|L|\cong S^4$, and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.
## Formalization scope
Lean represents $L$ using `AbstractSimplicialComplex (Fin m)`. Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit $4$-sphere.
The moment-angle space is a subtype of `(Fin m → ℂ)` defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is `singularHomologyFunctor` with coefficients in $\mathbb Z$, and total homology is a direct sum over all natural degrees.
The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain $G$ as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.
## Selected references
- Yang Han and Keke Li, *Moment Angle Manifolds Corresponding to $S^4$ Whose Homology and Loop Homology May Have Arbitrary Torsion*, International Mathematics Research Notices 2026(4), 1--7, 2026. [DOI](https://doi.org/10.1093/imrn/rnag024)
- A. Bahri, M. Bendersky, F. R. Cohen, and S. Gitler, *The polyhedral product functor: a method of decomposition for moment-angle complexes, arrangements and related spaces*, Advances in Mathematics 225(3), 2010, 1634--1668. [DOI](https://doi.org/10.1016/j.aim.2010.04.009)
## Motivation
The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a $d$-dimensional polytope with $n$ facets is at most $n - d$. Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the **polynomial Hirsch conjecture**: is the diameter bounded by a polynomial in $n$ and $d$?
## Timeline
- **1957.** Hirsch states the conjecture $\mathrm{diam} \le n - d$ in a letter to Dantzig, who publishes it in *Linear Programming and Extensions* (1963).
- **1964–1966.** Klee determines the exact maximum diameter of $3$-polytopes with $n$ facets, $\lfloor 2n/3\rfloor - 1$ — the Hirsch bound holds up to dimension three.
- **1967.** Klee and Walkup ([Acta Math.](https://doi.org/10.1007/BF02392971)) refute the *unbounded-polyhedron* version, prove the bounded conjecture for $n - d \le 5$, and reduce the general case to the **$d$-step conjecture** ($n = 2d$).
- **1970.** Larman ([Proc. LMS](https://doi.org/10.1112/plms/s3-20.2.249)) proves $\mathrm{diam} \le n\,2^{d-3}$ — linear in the number of facets for each fixed dimension, still the best bound of that shape.
- **1989.** Naddef ([Math. Programming](https://doi.org/10.1007/BF01589418)) proves $0/1$-polytopes satisfy the Hirsch bound, with diameter at most $d$.
- **1992.** Kalai and Kleitman ([Bull. AMS](https://arxiv.org/abs/math/9204233)) prove $\mathrm{diam} \le n^{\log_2 d + 2}$ in under a page — the quasi-polynomial barrier every later bound refines. The same year brings subexponential pivot rules (Kalai; Matoušek–Sharir–Welzl), the algorithmic counterpart.
- **2010.** Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR](https://doi.org/10.1287/moor.1100.0470)) show the known upper-bound arguments survive in a purely combinatorial abstraction — which admits almost-quadratic lower bounds, so a polynomial bound must use real geometry. Kalai launches **Polymath 3** on the polynomial version.
- **2010–2012.** Santos ([Annals of Math.](https://arxiv.org/abs/1006.2814)) disproves the Hirsch conjecture: a $43$-dimensional polytope with $86$ facets and diameter at least $44$, via spindles of large width.
- **2014–2019.** Todd ([SIAM J. Discrete Math.](https://arxiv.org/abs/1402.3579)) sharpens Kalai–Kleitman to $(n-d)^{\log_2 d}$; Sukegawa refines further. Matschke, Santos, and Weibel ([Proc. LMS 2015](https://arxiv.org/abs/1202.4701)) shrink the counterexample to dimension $20$ with $40$ facets and diameter $21$. All known violations remain constant-factor; all known bounds remain quasi-polynomial.
## Setting
Work in $\mathbb{R}^d$. An **H-polytope** is a set cut out by finitely many linear inequalities: given vectors $a_1, \dots, a_n \in \mathbb{R}^d$ and reals $b_1, \dots, b_n$, it is
$$P \;=\; \{\, x \in \mathbb{R}^d \mid \langle a_i, x\rangle \le b_i \text{ for } i = 1, \dots, n \,\},$$
where $\langle a_i, x\rangle = \sum_{j=1}^d a_{ij} x_j$ is the standard inner (dot) product — so each condition $\langle a_i, x\rangle \le b_i$ is one linear inequality, with normal vector $a_i$ and offset $b_i$. Throughout, $P$ is assumed nonempty and bounded. The parameter $n$ counts the inequalities in the given description; since every polytope with $f$ facets admits a description by exactly $f$ inequalities, bounds stated in terms of $n$ over all descriptions are equivalent to bounds in terms of facet counts.
A **vertex** of $P$ is an extreme point. Two vertices $u \ne v$ are **adjacent** when the segment $[u, v]$ is an extreme subset of $P$; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that $[u,v]$ is a one-dimensional face — an **edge**. The **combinatorial diameter** of $P$ is the diameter of the graph of vertices and edges. Throughout, "diameter at most $B$" is expressed as: every two vertices are joined by a walk of $B$ steps, each step staying put or crossing an edge — a form that is monotone in $B$ and asserts connectivity of the graph (Balinski's theorem) as part of the claim.
## Formalization targets
### Goal — the polynomial Hirsch conjecture
$$\exists\, c, k \in \mathbb{N}:\ \text{every nonempty bounded } P = \{x \in \mathbb{R}^d \mid \langle a_i, x \rangle \le b_i,\ i \le n\} \text{ has diameter} \le c\,(n + d)^k.$$
Every polynomial in $n$ and $d$ is dominated by some $c(n+d)^k$ and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.
### Milestones — the known ladder
Six classical results over the same definitions: the Hirsch bound $n - d$ in dimension $d \le 3$ (Klee; Klee–Walkup); Larman's bound $n \cdot 2^{d-3}$; Naddef's bound $d$ for $0/1$-polytopes; the Kalai–Kleitman bound $n^{\log_2 d + 2}$; Todd's bound $(n-d)^{\log_2 d}$ for full-dimensional $P$ with $n \ge d \ge 3$; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds $n - d$.
## Significance
A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR 2010](https://doi.org/10.1287/moor.1100.0470)) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.
None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.
## Difficulty
The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving *any* polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters *large* is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.
## Formalization scope
The Lean model commits to: ambient space `EuclideanSpace ℝ (Fin d)`; the polytope as `Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i}` for `a : Fin n → EuclideanSpace ℝ (Fin d)`, `b : Fin n → ℝ`, with nonemptiness and `Bornology.IsBounded` as explicit hypotheses (boundedness is essential: Klee–Walkup's *unbounded* counterexample would otherwise trivialize the Santos milestone); vertices as `Set.extremePoints ℝ`; adjacency as `u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v)`; and diameter bounds as the walk predicate `DiamLE`, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through `Real.logb` and the natural floor. In `larman_bound` and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all $n, d$ in scope. The dimension parameter $d$ is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with `todd_bound` requiring full-dimensionality (`(interior P).Nonempty`) as in its source.
Welcome contributions: any milestone in any order (`dimension_three_bound` for $d \le 1$ cases and structural lemmas about `Adj` and `DiamLE` are natural entry points, and `kalai_kleitman_bound` is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.
## Selected references
- V. Klee, D. Walkup, *The d-step conjecture for polyhedra of dimension d < 6*, Acta Math. 117 (1967). [doi:10.1007/BF02392971](https://doi.org/10.1007/BF02392971)
- D. Larman, *Paths on polytopes*, Proc. London Math. Soc. 20 (1970). [doi:10.1112/plms/s3-20.2.249](https://doi.org/10.1112/plms/s3-20.2.249)
- D. Naddef, *The Hirsch conjecture is true for (0,1)-polytopes*, Math. Programming 45 (1989). [doi:10.1007/BF01589418](https://doi.org/10.1007/BF01589418)
- G. Kalai, D. Kleitman, *A quasi-polynomial bound for the diameter of graphs of polyhedra*, Bull. AMS 26 (1992). [arXiv:math/9204233](https://arxiv.org/abs/math/9204233)
- F. Santos, *A counterexample to the Hirsch conjecture*, Annals of Mathematics 176 (2012). [arXiv:1006.2814](https://arxiv.org/abs/1006.2814)
- M. Todd, *An improved Kalai–Kleitman bound for the diameter of a polyhedron*, SIAM J. Discrete Math. 28 (2014). [arXiv:1402.3579](https://arxiv.org/abs/1402.3579)
- B. Matschke, F. Santos, C. Weibel, *The width of five-dimensional prismatoids*, Proc. London Math. Soc. 110 (2015). [arXiv:1202.4701](https://arxiv.org/abs/1202.4701)
- F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, *Diameter of polyhedra: limits of abstraction*, Math. Oper. Res. 35 (2010). [doi:10.1287/moor.1100.0470](https://doi.org/10.1287/moor.1100.0470)
- F. Santos, *Recent progress on the combinatorial diameter of polytopes and simplicial complexes*, TOP 21 (2013) (survey). [arXiv:1307.5900](https://arxiv.org/abs/1307.5900)
## Motivation
The $k$-server problem was introduced by Manasse, McGeoch, and Sleator ([STOC 1988 / J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) as a common generalization of paging, weighted caching, and related sequential decision problems, and their **$k$-server conjecture** has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on *every* metric space.
## Timeline
- **1985.** Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
- **1988–1990.** Manasse, McGeoch, and Sleator introduce the $k$-server problem ([STOC 1988; J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the **$k$-server conjecture**, in the symmetric finite setting of the paper.
- **1990.** Fiat, Rabani, and Ravid ([FOCS 1990](https://doi.org/10.1109/FSCS.1990.89566)) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space.
- **1991.** Chrobak, Karloff, Payne, and Vishwanathan ([SIAM J. Discrete Math.](https://doi.org/10.1137/0404017)) prove the conjecture on the real line via **Double Coverage**; Chrobak and Larmore ([SIAM J. Comput.](https://doi.org/10.1137/0220008)) extend it to all tree metrics.
- **1995.** Koutsoupias and Papadimitriou ([J. ACM](https://doi.org/10.1145/210118.210128)) prove the **Work Function Algorithm** is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: *for every metric space there is an online algorithm with competitive ratio $k$.*
- **1996.** The same authors verify the conjecture on spaces of $k+2$ points via the dual **2-evader problem** (Inf. Process. Lett. 57).
- **2004.** Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points.
- **2021.** Coester and Koutsoupias ([ICALP](https://arxiv.org/abs/2102.10474)) give a unifying potential for all known WFA analyses and push the frontier to the circle.
- **2023.** Bubeck, Coester, and Rabani ([STOC](https://arxiv.org/abs/2211.05753)) refute the *randomized* analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
## Setting
Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A **configuration** records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the **movement cost** is the total distance traveled,
$$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$
A **request sequence** is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).
A **deterministic online algorithm** $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the **initial configuration**, before any request arrives. Two points about this way of modeling an algorithm:
- *Online and deterministic, by construction.* The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
- *The service constraint.* Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$.
Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its **cost** is the total movement along this trajectory:
$$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$
For comparison, an **offline schedule** for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The **optimal offline cost** $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$.
Finally, $A$ is **$c$-competitive** if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with
$$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$
## Formalization targets
### Goal — the $k$-server conjecture
$$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$
The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.
### Milestones — the known ladder
The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm *itself* — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the *randomized* analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms.
## Significance
A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.
None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem.
## Difficulty
The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server *other than* the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$.
## Formalization scope
The Lean model commits to: configurations as functions `Fin k → M` (**labeled** servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions `List M → (Fin k → M)` with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in `ℝ` via `Metric.dist`; the offline optimum as an `sInf` over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as `∃ a, ∀ σ`.
Two conventions guard against trivialization. The additive constant is quantified *before* the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ *distinct* points (`Finset.card = k + 1`); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.
Three further definitional layers extend the model. The **work function** `workFunction C₀ σ C` is the `sInf` of (schedule cost + final move to `C`) over schedules serving `σ` from `C₀`, and the **Work Function Algorithm** `WFA` is defined on finite spaces with `k ≥ 1` servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A **tree** is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A **randomized algorithm** is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.
Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about `moveCost`, schedules, and work functions published as reusable platform theorems.
## Selected references
- M. Manasse, L. McGeoch, D. Sleator, *Competitive algorithms for server problems*, J. Algorithms 11 (1990). [doi:10.1016/0196-6774(90)90003-W](https://doi.org/10.1016/0196-6774(90)90003-W)
- A. Fiat, Y. Rabani, Y. Ravid, *Competitive k-server algorithms*, FOCS 1990. [doi:10.1109/FSCS.1990.89566](https://doi.org/10.1109/FSCS.1990.89566)
- M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, *New results on server problems*, SIAM J. Discrete Math. 4 (1991). [doi:10.1137/0404017](https://doi.org/10.1137/0404017)
- M. Chrobak, L. Larmore, *An optimal on-line algorithm for k servers on trees*, SIAM J. Comput. 20 (1991). [doi:10.1137/0220008](https://doi.org/10.1137/0220008)
- E. Koutsoupias, C. Papadimitriou, *On the k-server conjecture*, J. ACM 42 (1995). [doi:10.1145/210118.210128](https://doi.org/10.1145/210118.210128)
- E. Koutsoupias, C. Papadimitriou, *The 2-evader problem*, Inf. Process. Lett. 57(5) (1996), 249–252.
- C. Coester, E. Koutsoupias, *Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle*, ICALP 2021. [arXiv:2102.10474](https://arxiv.org/abs/2102.10474)
- S. Bubeck, C. Coester, Y. Rabani, *The randomized k-server conjecture is false!*, STOC 2023. [arXiv:2211.05753](https://arxiv.org/abs/2211.05753)
- E. Koutsoupias, *The k-server problem* (survey), Computer Science Review 3 (2009). [doi:10.1016/j.cosrev.2009.04.002](https://doi.org/10.1016/j.cosrev.2009.04.002)
## Motivation
The traveling salesman problem — visit $n$ cities by the cheapest round trip — is the most widely known problem in combinatorial optimization, and its central open question concerns a linear program. The **subtour-elimination relaxation** (the Held–Karp bound) replaces tours by fractional edge weights, and both in theory and in practice (it powers the lower bounds inside the Concorde solver) it is remarkably close to the true optimum. How close, in the worst case, is the **integrality gap** of the relaxation: the supremum of $\mathrm{OPT}/\mathrm{LP}$ over metric instances. Explicit instance families push the gap up to $4/3$; the best proven upper bound sits just barely below $3/2$. The **4/3 conjecture** — the gap is exactly $4/3$ — has been the benchmark question of approximation algorithms for four decades.
## Timeline
- **1954.** Dantzig, Fulkerson, and Johnson solve a 49-city instance by hand with the cutting planes that become the subtour-elimination LP.
- **1970–1971.** Held and Karp introduce the 1-tree/Lagrangian bound and show it equals the subtour LP value — since then, "the Held–Karp bound".
- **1976/1978.** Christofides, and independently Serdyukov, give the $3/2$-approximation: minimum spanning tree plus a matching on odd-degree vertices.
- **1980.** Wolsey ([Math. Prog. Study 13](https://doi.org/10.1007/BFb0120913)) shows Christofides' analysis goes through against the LP: $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, so the integrality gap is at most $3/2$. Shmoys and Williamson ([IPL 1990](https://doi.org/10.1016/0020-0190(90)90028-V)) rediscover this via a monotonicity property.
- **1995.** Goemans ([Math. Programming 69](https://doi.org/10.1007/BF01585563)) analyzes the worst-case ratios of TSP relaxations and states the $4/3$ conjecture explicitly; the $4/3$ lower-bound families (three parallel paths) are by then folklore.
- **2011–2014.** For **graph metrics** (shortest-path metrics of unweighted graphs) the barrier breaks: Oveis Gharan–Saberi–Singh and Mömke–Svensson beat $3/2$, and Sebő–Vygen ([Combinatorica 2014](https://arxiv.org/abs/1201.1870)) reach $7/5$ — the conjectured-optimal shape of progress, but only for a special class.
- **2020–2022.** Karlin, Klein, and Oveis Gharan prove a $3/2 - \varepsilon$ approximation for general metric TSP ([STOC 2021](https://arxiv.org/abs/2007.01409)) and then an integrality-gap bound $\gamma \le 3/2 - \varepsilon$ with $\varepsilon > 10^{-36}$ ([FOCS 2022](https://arxiv.org/abs/2105.10043)), via max-entropy sampling of spanning trees and strongly Rayleigh distributions — the first general improvement over Wolsey in forty years, by an astronomically small margin.
- **Today.** The gap between the $4/3$ lower bound and the $3/2 - 10^{-36}$ upper bound is the conjecture. For half-integral LP solutions — where the conjectured extremal instances live — the bound has been pushed to $1.4983$ (Gupta, Lee, Li, Mucha, Newman, and Sarkar, via matroid-based rounding).
## Setting
An **instance** on $n \ge 3$ cities is a cost function $c$ assigning to each ordered pair of cities $u, v$ a real cost $c(u,v)$, required to be a **metric cost**: symmetric ($c(u,v) = c(v,u)$), zero on the diagonal ($c(v,v) = 0$), and satisfying the triangle inequality $c(u,w) \le c(u,v) + c(v,w)$. Nonnegativity follows; distinct cities at distance zero are allowed, as usual for metric TSP.
A **tour** visits every city exactly once and returns to its start. Formally a tour is given by an ordering: a permutation $\pi$ of the cities, traversed as $\pi(0), \pi(1), \dots, \pi(n-1)$ and back to $\pi(0)$; its cost $\mathrm{tourCost}(c, \pi)$ is the sum of the costs of consecutive steps, and $\mathrm{OPT}(c)$ — written `tspOpt c` — is the minimum over all orderings.
The **subtour-elimination (Held–Karp) relaxation** replaces the tour by a fractional edge weight $x(u,v)$ for each pair of cities. A weight vector $x$ is **feasible** (`IsHeldKarp x`) when it is symmetric with zero diagonal, has entries in $[0,1]$, gives every city fractional degree two ($\sum_u x(v,u) = 2$), and crosses every nontrivial cut at least twice: for every set $S$ of cities other than $\emptyset$ and all cities, $\sum_{u \in S} \sum_{v \notin S} x(u,v) \ge 2$. The **Held–Karp bound** `hkValue c` is the infimum of $\frac{1}{2}\sum_u \sum_v c(u,v)\,x(u,v)$ over feasible $x$ (the double sum counts each edge twice, hence the $\frac12$). The incidence vector of any tour is feasible, so $\mathrm{LP} \le \mathrm{OPT}$ always.
## Formalization targets
### Goal — the 4/3 conjecture
$$\mathrm{OPT}(c) \;\le\; \tfrac{4}{3}\,\mathrm{LP}(c) \qquad \text{for every } n \ge 3 \text{ and every metric cost } c.$$
Together with the known lower-bound families this says the integrality gap is exactly $4/3$. The goal carries no algorithm and no constant to improve: it is the terminal statement of the ladder, open in both directions (a proof or a counterexample instance would each settle it).
### Milestones — the known ladder
Five results over the same definitions: the relaxation is valid ($\mathrm{LP} \le \mathrm{OPT}$); instance families force the gap arbitrarily close to $4/3$; tree doubling gives $\mathrm{OPT} \le 2\,\mathrm{LP}$; Wolsey's theorem gives $\mathrm{OPT} \le \frac{3}{2}\,\mathrm{LP}$, the classical upper bound; and the Karlin–Klein–Oveis Gharan record $\mathrm{OPT} \le (\frac{3}{2} - \varepsilon)\,\mathrm{LP}$ for some $\varepsilon > 10^{-36}$ (FOCS 2022). The last milestone is a statement-level target: its known proof (max-entropy sampling, strongly Rayleigh polynomials) is far beyond current formalization practice, so the mission's usable proving frontier remains Wolsey — the milestone records the state of the art as a formal statement.
## Significance
The 4/3 conjecture is the reference open problem of approximation algorithms: the quality of the subtour LP calibrates every algorithmic advance on TSP, and the conjectured extremal instances guide the search for better rounding schemes. The bound is also what practical solvers actually compute — branch-and-cut on this LP solves instances with tens of thousands of cities — so the conjecture is a statement about the observed tightness of the world's most-used combinatorial lower bound.
Nothing in this circle exists in any proof assistant: Mathlib has no TSP, no LP relaxations, no polyhedral combinatorics of tours. The mission's milestones force the base layer into existence — tours over `Equiv.Perm`, cut constraints over `Finset`, and, for the upper bounds, the parity and tree arguments (spanning trees against the LP, T-joins for the $3/2$ bound) whose infrastructure is reusable for matching theory and network design far beyond TSP.
## Difficulty
The naive plan — round the LP solution to a tour — has no known analysis losing less than $3/2$ in general, and the half-integral extremal instances show the hard cases are structured and simple-looking at once. Christofides' matching argument is provably stuck at $3/2$ against the LP; forty years of work moved the constant by $10^{-36}$, and that advance needed an entirely new probabilistic toolkit. On the other side, no instance family with ratio above $4/3$ has ever been found despite extensive computational search over small instances (Benoit–Boyd and successors). Both directions of the goal are genuinely open territory.
## Formalization scope
The Lean model commits to: cities `Fin n`; costs `c : Fin n → Fin n → ℝ` with `IsMetricCost` (symmetry, zero diagonal, triangle inequality — nonnegativity is derived, and semimetrics are included as in the standard statement of the conjecture); tours as orderings `π : Equiv.Perm (Fin n)` traversed cyclically via `finRotate`, so every permutation denotes a Hamiltonian cycle and every Hamiltonian cycle is denoted; both optimal values as `sInf` over nonempty, bounded-below sets of reals, so they are genuine minima for `n ≥ 3`. The hypothesis `3 ≤ n` is load-bearing: for `n ≤ 2` the degree-2 constraints are infeasible, `sInf ∅ = 0` by convention, and the bounds would be false — every theorem therefore carries it.
Welcome contributions: the milestones in any order — `held_karp_le_opt` is the natural entry point (the tour's incidence vector crosses every cut at least twice); `integrality_gap_lower_bound` needs the three-path instance family and a case analysis on its tours; `tree_doubling_bound` needs spanning trees against the LP; `wolsey_bound` adds the T-join/parity argument and is the summit. Reusable infrastructure — spanning tree polytopes, T-joins, Eulerian traversals, cut lemmas — is welcome as platform theorems. Graph-TSP ($7/5$), path TSP, and asymmetric TSP are deliberately left to future missions; the Karlin–Klein–Oveis Gharan bound is stated as a milestone, but its sampling machinery is expected to arrive, if ever, as shared infrastructure built over many contributions.
## Selected references
- G. Dantzig, R. Fulkerson, S. Johnson, *Solution of a large-scale traveling-salesman problem*, Oper. Res. 2 (1954).
- M. Held, R. Karp, *The traveling-salesman problem and minimum spanning trees*, Oper. Res. 18 (1970); Part II, Math. Programming 1 (1971).
- N. Christofides, *Worst-case analysis of a new heuristic for the travelling salesman problem*, CMU report (1976); A. Serdyukov, Upravlyaemye Sistemy 17 (1978).
- L. Wolsey, *Heuristic analysis, linear programming and branch and bound*, Math. Prog. Study 13 (1980). [doi:10.1007/BFb0120913](https://doi.org/10.1007/BFb0120913)
- D. Shmoys, D. Williamson, *Analyzing the Held-Karp TSP bound: a monotonicity property with application*, Inf. Process. Lett. 35 (1990). [doi:10.1016/0020-0190(90)90028-V](https://doi.org/10.1016/0020-0190(90)90028-V)
- M. Goemans, *Worst-case comparison of valid inequalities for the TSP*, Math. Programming 69 (1995). [doi:10.1007/BF01585563](https://doi.org/10.1007/BF01585563)
- A. Sebő, J. Vygen, *Shorter tours by nicer ears*, Combinatorica 34 (2014). [arXiv:1201.1870](https://arxiv.org/abs/1201.1870)
- A. Karlin, N. Klein, S. Oveis Gharan, *A (slightly) improved approximation algorithm for metric TSP*, STOC 2021. [arXiv:2007.01409](https://arxiv.org/abs/2007.01409)
- A. Karlin, N. Klein, S. Oveis Gharan, *A (slightly) improved bound on the integrality gap of the subtour LP for TSP*, FOCS 2022. [arXiv:2105.10043](https://arxiv.org/abs/2105.10043)
- V. Traub, J. Vygen, *Approximation Algorithms for Traveling Salesman Problems*, Cambridge University Press, 2024. [book page](https://www.or.uni-bonn.de/tspbook/book.pdf)
Erdős Problem 390: Exact Second-Order AsymptoticResearch Paper
Determine the exact second-order term in the least possible largest factor in a factorization of $n!$ into distinct integers exceeding $n$, with the proposed rational constant $4029639598/25970038185$.
Every even integer greater than $2$ is the sum of two primes. Christian Goldbach posed it in a 1742 letter to Euler, and it has resisted proof for nearly three centuries while being verified computationally up to $4\times10^{18}$ — making it one of the oldest and most famous open problems in all of mathematics. Its ternary sibling, the weak Goldbach conjecture, was settled by Helfgott in 2013, but the strong form stated here remains wide open: the circle method controls three-prime sums yet loses control at two. This headline mission hosts the conjecture as a machine-checked target for partial results, reductions between its variants, and any future attack.
No problem in mathematics carries more weight than the Riemann hypothesis. In his single eight-page paper of 1859, 'On the Number of Primes Less Than a Given Magnitude,' Bernhard Riemann linked the seemingly erratic distribution of the primes to the zeros of the analytic continuation of the zeta function ζ(s), and conjectured that every nontrivial zero lies exactly on the critical line where the real part equals 1/2. The truth of this statement would pin down the error term in the prime number theorem and tame the fluctuations of the primes around their expected count, and hundreds of theorems already stand proven only 'conditional on RH,' waiting for it to be settled. David Hilbert placed it in his eighth problem in 1900, alongside Goldbach and the twin primes; in 2000 the Clay Mathematics Institute named it one of the seven Millennium Prize Problems, with a million-dollar reward. G. H. Hardy proved in 1914 that infinitely many zeros lie on the critical line, and trillions more have since been verified by computation to do so — overwhelming evidence that is nonetheless not a proof. After more than 160 years it remains unresolved. This mission takes Mathlib's own definition of the hypothesis as its target.
Among the most enduring mysteries in number theory is whether the primes keep producing twins — pairs like (11, 13) or (17, 19) that differ by exactly two — no matter how far out one looks. The general form was set down by Alphonse de Polignac in 1849, and the first deep theorem came from Viggo Brun in 1915, who proved that the reciprocals of the twin primes converge to a finite value, now called Brun's constant; in doing so he invented modern sieve theory and showed that twins must thin out even if there are infinitely many. Hardy and Littlewood went further, conjecturing a precise density of about 2C₂·x/(ln x)² for the count of twins below x. For nearly a century the infinitude itself stood untouched, until Yitang Zhang's stunning announcement on 17 April 2013 that some gap below 70 million recurs infinitely often — the first finite bound ever proved. A Polymath collaboration led by Terence Tao, together with James Maynard's independent multidimensional sieve, soon drove that bound down to 246, where it still stands. Closing the gap all the way to 2 — the twin prime conjecture itself — remains open. This mission states it cleanly: the set of primes p for which p + 2 is also prime is infinite.