The Markov Chain Central Limit TheoremResearch Paper
Markov chain Monte Carlo turns hard integration problems into long simulations: to estimate an expectation $E_\pi f$ one runs a Markov chain with stationary distribution $\pi$ and reports the sample average $\bar f_n$. The ergodic theorem guarantees $\bar f_n \to E_\pi f$, but honest error bars require more: a central limit theorem $$\sqrt{n}(\bar f_n - E_\pi f) \to_d N(0, \sigma_f^2).$$ On general state spaces this is famously delicate - a merely ergodic chain with a square-integrable functional can fail the CLT, so the classical theory trades convergence rates (drift, minorization, geometric or polynomial total-variation rates) and mixing conditions ($\alpha$-, $\rho$-, $\varphi$-mixing) against moment conditions on $f$. This mission formalizes G. L. Jones's survey "On the Markov chain central limit theorem" (Probability Surveys, 2004): the drift-condition CLTs of Meyn-Tweedie and Jarner-Roberts, the classical mixing CLTs of Ibragimov-Linnik, Doukhan-Massart-Rio and Billingsley, the characterizations via uniform integrability and boundedness in probability, and their assembly into the summary theorem: six practically checkable regimes - from polynomial ergodicity with bounded functionals to uniform ergodicity with second moments - each of which guarantees the CLT for every initial distribution. The stationarity, total-variation and mixing infrastructure is general state space and reusable well beyond this mission.
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)
Vector Space Methods XII: Pontryagin Minimum PrincipleTextbook
## Motivation
[Pontryagin's principle as presented by Luenberger](https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf) is the decisive necessary condition in continuous-time optimal control. It converts an optimization over functions into a pointwise comparison of a Hamiltonian, coupled to the original state equation and a backward costate equation. Luenberger derives the minimum-Hamiltonian convention from vector-space multiplier ideas and a first-order comparison principle. Formalization is especially valuable here because the printed theorem contains a standard but consequential regularity oversight: it asserts a condition at every time even though controls are only piecewise continuous and the cost is an integral. This mission preserves the intended theorem while replacing that false pointwise claim by the mathematically canonical almost-everywhere statement.
## Setting
Fix `t₀ < t₁`, a finite-dimensional **Euclidean state space** `OCState n`, a Euclidean control space `OCControl m`, and a permitted-control set `Omega`. A state-control pair `(x,u)` is **admissible** when `x t₀ = xInit`, the state is **absolutely continuous** on the interval, the control is **almost everywhere strongly measurable** and lies in `Omega` almost everywhere, the differential equation `x' = F(x,u)` holds almost everywhere in the interior, and the running cost is interval integrable. An **optimal pair** globally minimizes the interval integral among all admissible pairs.
The dynamics `F` and running cost `ell` are continuous jointly in state and control and continuously differentiable in the state variable. Their state derivatives `Fx` and `ellx` vary continuously. A global Lipschitz estimate controls changes of `F` in both state and control. Because an a.e. measurable control need not be bounded, the optimal control is explicitly assumed to have an a.e. norm bound on the compact interval, matching the boundedness inherited from the source's piecewise-continuous model. The operator-valued paths `Fx (x₀ t) (u₀ t)` and `ellx (x₀ t) (u₀ t)` are also assumed interval integrable along the optimum. Together these hypotheses provide the measure-theoretic regularity needed for the adjoint and state perturbations. The Hamiltonian uses Luenberger's minimum convention,
$$
H(x,u,\lambda)=\langle \lambda,F(x,u)\rangle+\ell(x,u).
$$
## Formalization targets
The root `VectorSpaceOpt.pontryagin_minimum_principle` asserts the existence of an absolutely continuous costate `lambda` with terminal value `lambda t₁ = 0`. Almost everywhere it satisfies the weak inner-product form of
$$
-\dot\lambda(t)=D_xF(x₀(t),u₀(t))^*\lambda(t)+D_x\ell(x₀(t),u₀(t)),
$$
and almost everywhere on the control interval it satisfies
$$
H(x₀(t),u₀(t),\lambda(t))
\le H(x₀(t),v,\lambda(t))
\quad\text{for every }v\in\Omega.
$$
Two milestones capture source dependencies. `control_state_lipschitz_estimate` is the Grönwall stability estimate used on p. 263 to control the state response by the integral distance between controls; it explicitly assumes interval integrability of both the state-difference norm and the control-difference norm, so Mathlib's totalized integral cannot hide a nonintegrable input. `adjoint_lagrangian_comparison` formalizes §9.6, Proposition 1: under an implicit state equation, differentiability in the state, Lipschitz dependence of the state solution, and an adjoint identity, the objective difference agrees with a frozen-state Lagrangian difference up to an explicit filter-level little-o remainder.
## Significance
This is the flagship analytic mission of the continuation. It connects finite-dimensional differential calculus, Bochner integration, absolute continuity, ODE constraints, adjoints, and localized control variations in one reusable theorem. The definitions form a minimal control framework that can support terminal costs, endpoint constraints, and alternative maximum-principle conventions later. The corrected a.e. conclusion also demonstrates a central benefit of formalization: informal conventions about representatives of controls and isolated time values must be resolved before a theorem can be accepted.
The weak inner-product adjoint equation avoids introducing a coordinate transpose and remains invariant under the Euclidean-space representation. That choice makes the result immediately reusable in later vector-space treatments of transversality and endpoint multipliers.
## Difficulty
The difficulty is very high. Mathlib supplies finite-dimensional calculus, interval integration, absolute continuity, measure-theoretic almost-everywhere statements, and Grönwall tools, but not an assembled Pontryagin framework. The mission must coordinate a state-solution stability estimate, state differentiability of the dynamics and cost, existence and regularity of the backward costate, and Hamiltonian comparison against arbitrary admissible values. The control is measurable rather than globally continuous, so every pointwise expression must be placed under an a.e. quantifier where appropriate. The proposition milestone additionally requires a precise little-o interface instead of an unnamed asymptotic remainder.
## Formalization scope
The proposal covers §9.6, Proposition 1 and Theorem 1, with the regularity inherited from the surrounding discussion made explicit. Both the optimal state and the costate are absolutely continuous. Admissible controls are a.e. strongly measurable, which is a broader measure-theoretic proxy for the source's piecewise-continuous controls and is compatible with integral objectives; the root additionally requires the optimal control to be essentially norm bounded on `Icc t₀ t₁`, restoring the compact-interval boundedness used by the source. The maps `F`, `ell`, `Fx`, and `ellx` are jointly continuous; state derivatives are supplied by `HasFDerivAt`; a uniform Lipschitz bound is stated; and both derivative coefficients along the optimal path are interval integrable. The separate Grönwall milestone requires its state and control norm differences to be interval integrable. The interval is required to have positive length.
There is a documented source erratum. The sentence on printed p. 263 states Hamiltonian minimality for every `t`, while the proof on p. 264 chooses a neighborhood on which a purported strict violation persists. That step requires continuity at the selected time. Moreover, changing a piecewise-continuous control at a single isolated time changes neither its a.e. class, the state equation, nor the integral cost. Therefore no condition can be forced at an arbitrary jump value. The Lean root uses an a.e. conclusion on `Icc t₀ t₁`; an alternative source-faithful repair would assert the inequality at every continuity point of `u₀`. The mission does not claim existence of an optimal pair, compactness of `Omega`, endpoint constraints, nonsmooth dynamics, or a sufficiency theorem.
## Selected references
- David G. Luenberger, *Optimization by Vector Space Methods*, Wiley, 1969, Chapter 9, §9.6, Proposition 1 and Theorem 1, pp. 262–264, including the printed all-times wording and its proof context. Scan: https://sites.science.oregonstate.edu/~show/old/142_Luenberger.pdf
- Lean community, *Mathlib documentation*, continuously updated: https://leanprover-community.github.io/mathlib4_docs/ (interval integration, absolute continuity, Euclidean spaces, Fréchet derivatives, ODE estimates, and a.e. measurability).
## 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)
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.
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
# 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 Lean capstone focuses on the analytic density characterization and a deliberately auditable syntax of elementary functions. It does not yet construct Brownian motion or prove Durbin's derivation inside Lean. Real constants are allowed as expression leaves, so the substantive restriction is functional form, not the arithmetic nature of parameters. This interpretation must be considered when evaluating any impossibility claim.
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
Build a continuous nonnegative solution of the Abel equation, prove uniqueness and unit mass, and only then address elementary closed form.
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 CUHK-Shenzhen problem](https://rybindmitry.github.io/problems/13.html)
Davie–Stothers Fourth-Power Bound: omega < 2.3737Research Paper
## Motivation
The **matrix-multiplication exponent** $\omega$ measures the asymptotic arithmetic cost of multiplying square matrices. An upper bound $\omega<c$ means that, over the field under consideration, two $n\times n$ matrices can be multiplied using $O(n^{c+\varepsilon})$ field operations for every $\varepsilon>0$. It is a central benchmark in algebraic complexity and controls the exponent of many algorithms that use matrix multiplication as a subroutine.
Coppersmith and Winograd's 1990 analysis of the square of their tensor established $\omega<2.375477$. That number remained the record for roughly two decades. Stothers' 2010 thesis first obtained a smaller exponent by analyzing the fourth tensor power, and Davie and Stothers later supplied a self-contained journal treatment. Their Theorem 5.3 and numerical parameters give $\omega<2.373689703$; see [Davie--Stothers](https://www.maths.ed.ac.uk/~sandy/a11164.pdf), printed pp. 367--368. The result is the first historical step below the classical tensor-square barrier and is the natural next capstone after a formal proof of the $2.375477$ bound.
This mission formalizes the Davie--Stothers fourth-power argument at the exact rational endpoint $2.3737$. It concentrates on the new mathematical layer introduced by the fourth power: five non-matrix constituents, their recursive value estimates, and the two-dimensional same-marginal ambiguity in the final distribution count.
## Setting
For a field $K$, an order-three tensor represents a bilinear map. The **matrix-multiplication tensor**
$$
\langle a,b,c\rangle_K
=\sum_{i<a}\sum_{j<b}\sum_{k<c}
x_{ij}\otimes y_{jk}\otimes z_{ki}
$$
encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. Restrictions apply linear maps to the three tensor legs; degenerations permit polynomial families of maps. A direct sum of matrix-multiplication tensors has disjoint variable blocks and can be converted into an exponent inequality by Schönhage's asymptotic sum inequality.
The **Coppersmith--Winograd tensor** $CW_q$ has border rank at most $q+2$ and a three-class coordinate partition. Its square decomposes into fifteen coarse constituents $\varphi_{ijk}$ with $i+j+k=4$. Davie--Stothers square this decomposition again. The fourth power has forty-five constituents with indices summing to eight, grouped into ten symmetry classes represented by
$$
\varphi_{008},\ \varphi_{017},\ \varphi_{026},\ \varphi_{035},\ \varphi_{044},
\ \varphi_{116},\ \varphi_{125},\ \varphi_{134},\ \varphi_{224},\ \varphi_{233}.
$$
The first five classes are rectangular matrix-multiplication tensors. The last five require recursive value bounds. With $\rho\in[2,3]$, the paper writes
$$
E=(2q)^\rho,\qquad H=(q^2+2)^\rho,\qquad
L=4q^\rho(q^\rho+2),
$$
and states the five lower bounds in Lemma 5.1. The final fourth-power extraction assigns frequencies to the ten symmetry classes. Their coordinate marginals are encoded by the $9\times10$ matrix $Q$ in Equation (5.2); its kernel is the two-dimensional space $Y$ displayed immediately after that equation.
The paper's bounds are limiting exponential rates and may carry subexponential losses in their finite Salem--Spencer extractions. Prove2Me's `HasTauValueAtLeast` predicate instead records a constant-relative finite witness. The source-faithful formal statements therefore assert attainment of every fixed nonnegative base strictly below each displayed limiting rate, rather than unjustified attainment of the limiting endpoint itself. This downward-closed form retains the complete asymptotic conclusion and is exactly what the final strict numerical surplus needs.
## Formalization targets
### Goal: the Davie--Stothers fourth-power bound
For every field $K$,
$$
\operatorname{matMulExp}(K)<\frac{23737}{10000}=2.3737.
$$
The source's computed endpoint $2.373689703$ is strictly smaller, giving slack for an exact rational certificate. The Lean goal has exactly the same field quantification and `matMulExp` definition as the existing Coppersmith--Winograd mission; only the theorem identifier and endpoint change.
### Source-level milestones
The mission records the canonical nine-grading of $CW_6^{\otimes4}$ and the ten symmetry classes of Table 1. It formalizes all five clauses of Lemma 5.1 for $\varphi_{116}$, $\varphi_{125}$, $\varphi_{134}$, $\varphi_{224}$, and $\varphi_{233}$ in every-strict-lower-base form; Equation (5.2) and the stated basis of $\ker Q$; Lemma 5.2's entropy minimization along that kernel; Theorem 5.3's downward-closed fourth-power value inequality; and the Table 2 numerical specialization. The final milestones connect the resulting tau-value surplus to the border-rank budget and transfer the Strassen-preorder exponent bound to `matMulExp`.
## Significance
Mathematically, this theorem is the first improvement obtained by passing from the square to the fourth power of the Coppersmith--Winograd tensor. It establishes the recursive constituent pattern used by the later eighth-, sixteenth-, and higher-power analyses. In particular, the five formulas in Lemma 5.1 are the first complete catalogue of genuinely recursive fourth-power constituents.
For formalization, the mission creates a reusable representation of higher-power CW gradings and their symmetry orbits. It also forces a distinction between a locally chosen joint type and all other types with the same marginals. Lemma 5.2 is the exact finite-dimensional entropy correction needed when the marginal map has nontrivial kernel. That infrastructure can be reused by later refined-laser and complete-split missions.
The result is known mathematically. The open task is a machine-checked reconstruction. Prove2Me already contains the CW tensor, its characteristic-free border-rank degeneration, its canonical square grading and constituent restrictions, the Salem--Spencer layer, direct-sum tau-value witnesses, the asymptotic sum inequality, and the exponent bridge. The exact optimizer identity for the $\varphi_{116}$ profile is also proved. The remaining frontier is to connect the literal fourth-power constituents to finite direct-sum extractions, then assemble all five value estimates and the final kernel-corrected distribution count.
## Difficulty
The fourth power contains 225 ordered products before symmetry grouping. A formal proof must show that each claimed constituent is the literal block of $CW_q^{\otimes4}$ and that its recursive decomposition uses the correct variable spaces. Replacing a sum of overlapping blocks by an external direct sum would make the value bound artificially strong.
The five non-matrix classes have different feasible frequency polytopes. Their optimizer formulas are valid only after the corresponding nonnegativity and normalization conditions are checked. The $\varphi_{233}$ class already has a nontrivial same-marginal family. At the global level the map $Q$ has a two-dimensional kernel, so marginal counts alone do not determine a unique joint distribution. Ignoring that kernel removes the entropy penalty and invalidates Theorem 5.3.
Finally, Table 2 contains decimal witnesses obtained numerically. A formal proof must replace floating-point evaluation by exact rational parameters and certified bounds for logarithms and real powers, while retaining strict slack at $23737/10000$.
## Formalization scope
The development uses environment `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e` and the existing `TensorObj`, `MMObj`, restriction, degeneration, `HasTauValueAtLeast`, `tensorAsymptoticRank`, `matMulExp_strassen`, and `matMulExp` declarations. Top-level theorems quantify over an arbitrary field. Finite block indices and symmetry classes use finite types; frequency vectors and entropy inequalities use real numbers; exact finite profiles use natural numbers before passing to cofinal asymptotics.
The capstone specializes to $q=6$ and the fourth tensor power. Generic grading, orbit, multinomial, entropy, and optimizer lemmas are welcome when they shorten later missions. Every value theorem must ultimately be backed by restrictions or degenerations to direct sums of concrete matrix-multiplication tensors. An opaque value functional, a constituent definition that is an external sum rather than the source block, or a numerical hypothesis that assumes the desired endpoint is outside scope.
Contributions are welcome for the literal nine-grading, symmetry-orbit classification, the five constituent extractions, exact address factorizations, optimizer feasibility, the kernel calculation and Lemma 5.2, exact Table 2 arithmetic, and the final exponent assembly.
## Selected references
- A. M. Davie and A. J. Stothers, *Improved Bound for Complexity of Matrix Multiplication*, Proceedings of the Royal Society of Edinburgh Section A: Mathematics 143(2), 2013, pp. 351--369. [Author PDF](https://www.maths.ed.ac.uk/~sandy/a11164.pdf) and [DOI 10.1017/S0308210511001646](https://doi.org/10.1017/S0308210511001646).
- A. J. Stothers, *On the Complexity of Matrix Multiplication*, PhD thesis, University of Edinburgh, 2010. [Edinburgh Research Archive](https://era.ed.ac.uk/handle/1842/4734).
- Don Coppersmith and Shmuel Winograd, *Matrix Multiplication via Arithmetic Progressions*, Journal of Symbolic Computation 9, 1990, pp. 251--280. [DOI 10.1016/S0747-7171(08)80013-2](https://doi.org/10.1016/S0747-7171(08)80013-2).
- Arnold Schönhage, *Partial and Total Matrix Multiplication*, SIAM Journal on Computing 10(3), 1981, pp. 434--455. [DOI 10.1137/0210032](https://doi.org/10.1137/0210032).
Algorithmic Game Theory I: Existence of Nash EquilibriumTextbook
## Motivation
The strategic-form game is the basic object of noncooperative game theory, and the **Nash equilibrium** — a profile of randomized strategies from which no player benefits by deviating unilaterally — is its central solution concept. Nash proved in 1951 that every game with finitely many players and finite strategy sets has such an equilibrium ([Nash, *Non-cooperative games*, Ann. Math. 54 (1951)](https://doi.org/10.2307/1969529)); this single existence theorem is the reason the concept organizes the rest of the field, from the computational complexity of finding equilibria to the price of anarchy. The theorem is stated as Theorem 1.8 of Nisan–Roughgarden–Tardos–Vazirani (eds.), *Algorithmic Game Theory* (Cambridge, 2007), the source text of this mission series, whose first chapter (Tardos–Vazirani) also treats the two special cases that admit direct algorithmic proofs: two-person zero-sum games, where equilibria are exactly the optimal solutions of a dual pair of linear programs (von Neumann 1928; Theorem 1.11), and a simple linear market, where equilibrium prices are computed by an ascending tight-set algorithm (Theorem 1.17).
A timeline of the existence theorem: von Neumann (1928) proved the minimax theorem for two-person zero-sum games; Nash (1950, 1951) extended existence to arbitrary finite games, first via Kakutani's fixed-point theorem and then via Brouwer's. All known proofs of the general theorem pass through a fixed-point principle, and this is not an artifact: computing a Nash equilibrium is PPAD-complete (Daskalakis–Goldberg–Papadimitriou 2009; Chen–Deng–Teng 2009), and PPAD is precisely the complexity class of the fixed-point arguments.
## Setting
A **finite strategic-form game** consists of a finite set $\iota$ of players, for each player $i$ a finite nonempty set $S_i$ of **pure strategies**, and for each player a **payoff function** $u_i : \prod_j S_j \to \mathbb{R}$; all players are utility maximizers. A **mixed strategy** for player $i$ is a probability distribution on $S_i$, represented as a weight function $\sigma_i : S_i \to \mathbb{R}$ with $\sigma_i \ge 0$ and $\sum_{s} \sigma_i(s) = 1$ (a **lottery**). Players randomize independently, so a **mixed profile** $\sigma = (\sigma_i)_{i}$ induces the product distribution on pure strategy vectors, and player $i$'s **expected payoff** is
$$U_i(\sigma) \;=\; \sum_{s \in \prod_j S_j} \Big(\prod_j \sigma_j(s_j)\Big)\, u_i(s).$$
A mixed profile $\sigma$ is a **(mixed) Nash equilibrium** if for every player $i$ and every lottery $\tau$ on $S_i$, replacing $\sigma_i$ by $\tau$ does not increase $U_i$.
A **two-person zero-sum game** is given by a matrix $A \in \mathbb{R}^{m \times n}$: the row player picks a row distribution $p$, the column player a column distribution $q$, and the column player pays the row player $p^{\mathsf T} A q$ in expectation.
The market of §1.8.1 of the source has finitely many divisible **goods**, good $a$ in $s_a$ units, and finitely many **buyers**, buyer $j$ bringing budget $m_j > 0$ and interested in a nonempty set of goods; utilities are linear 0/1, so a buyer wants any goods from her interest set and none other. **Market-clearing prices** are positive prices under which each buyer can spend her whole budget on cheapest goods in her interest set while every good sells out exactly.
## Formalization targets
### Goal (capstone) — Theorem 1.8
$$\text{Every finite strategic-form game has a mixed Nash equilibrium.}$$
Stated for an arbitrary finite family of finite nonempty strategy types; no bound on the number of players, no genericity assumptions.
### Supporting — Brouwer fixed-point theorem
$$K \subseteq E \text{ nonempty compact convex},\ E \text{ finite-dimensional},\ f : K \to K \text{ continuous} \implies \exists x,\ f(x) = x.$$
Mathlib currently has no form of Brouwer's theorem; every known proof of Theorem 1.8 needs it (or an equivalent), so it enters the mission as an explicit milestone rather than an assumed library fact.
### Theorem 1.11 — zero-sum games
$$\exists\, p^\ast, q^\ast:\quad \forall p,\ p^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q^\ast, \quad \forall q,\ {p^\ast}^{\mathsf T} A q^\ast \le {p^\ast}^{\mathsf T} A q, \quad\text{and}\quad (p^\ast, q^\ast) \text{ is a mixed Nash equilibrium}$$
of the explicit two-player game with payoffs $A_{xy}$ to the row player and $-A_{xy}$ to the column player. The source states the result as: optimal solutions of a dual pair of LPs form a Nash equilibrium of the zero-sum game; the first two conjuncts are the saddle point that LP optimality amounts to, and the third states the Nash-equilibrium clause against the mission's own game vocabulary, so "zero-sum" is formal (the two payoffs sum to zero) rather than implicit in the shape of the statement.
### Theorem 1.17 (existence form)
$$\text{The 0/1-utilities linear market admits market-clearing prices and allocations.}$$
The source proves this by an ascending-price algorithm and also bounds its running time; the complexity half has no formal counterpart in this mission.
## Significance
The capstone is the foundation of the whole mission series: correlated equilibria, price-of-anarchy bounds, and mechanism-design characterizations in later missions all quantify over or compare against Nash equilibria, and the series inherits its game vocabulary (`IsLottery`, `IsMixedProfile`, `expectedPayoff`, `IsMixedNash`) from this mission.
Formalizing it produces the first Brouwer fixed-point theorem in this environment — a well-known gap in mathlib with reuse value far beyond game theory (every degree-theoretic and equilibrium-existence argument needs it). The zero-sum milestone yields the minimax theorem, reusable for the learning-dynamics mission that follows. All results here are classical and proved on paper; the work requested is machine-checked proof, not new mathematics.
## Difficulty
The central difficulty is Brouwer. The standard routes are (i) Sperner's lemma plus a limit argument, which needs a formal theory of simplicial subdivisions that does not exist in mathlib; (ii) algebraic topology (no retraction of the ball onto the sphere), for which mathlib has singular homology but not yet the homology of spheres in usable form; (iii) analytic proofs (Milnor–Rogers). None is short; the milestone is deliberately stated for a general nonempty compact convex set in a finite-dimensional normed space so that any route serves, and so the lemma lands in reusable generality.
Given Brouwer, Theorem 1.8 still requires Nash's gain-function construction on the product of simplices and the verification that fixed points are equilibria — bookkeeping-heavy but standard. Theorem 1.11 does not need Brouwer: mathlib's Sion minimax theorem (`Mathlib.Topology.Sion`) applies to the bilinear payoff on the product of standard simplices, or one can argue by LP duality directly. Theorem 1.17 needs the tight-set/max-flow argument of Lemmas 1.15–1.16 or any direct construction of the equilibrium.
## Formalization scope
Games are presented concretely: players form a finite index type, strategies a finite type per player, payoffs are functions into $\mathbb{R}$; mixed strategies are weight functions with a `IsLottery` predicate, not measure-theoretic distributions. Deviations in the equilibrium definition range over all lotteries (not only pure strategies): the pure-deviation reduction is a lemma a solver may prove, not part of the definition. Strategy sets are assumed nonempty in the capstone; the player set need not be. In the zero-sum milestone both dimensions are positive (`Fin (m+1)`, `Fin (n+1)`), payoffs flow from the column player to the row player, `stdSimplex` plays the role of the mixed-strategy space, and the Nash-equilibrium conjunct is stated for the Boolean-indexed two-player game built by `matrixGameStrat`/`zeroSumPayoff`/`matrixGameProfile` from the definitions bundle. In the market milestone all supplies and budgets are positive, every buyer's interest set is nonempty, and every good has an interested buyer, matching the standing assumptions of §1.8.1; allocations are recorded as money spent, so the clearing condition is $\sum_j x_{ja} = p_a s_a$ with no division anywhere.
Trivializing readings are ruled out: the empty simplex has no lotteries, so nonemptiness hypotheses appear exactly where their absence would make an existence claim false (Brouwer on the empty set, games with an empty strategy set, zero-dimensional matrix games).
## Selected references
- J. F. Nash, *Non-cooperative games*, Annals of Mathematics 54 (1951), 286–295. [DOI](https://doi.org/10.2307/1969529)
- J. von Neumann, *Zur Theorie der Gesellschaftsspiele*, Mathematische Annalen 100 (1928), 295–320. [DOI](https://doi.org/10.1007/BF01448847)
- N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), *Algorithmic Game Theory*, Cambridge University Press, 2007, Chapter 1. [DOI](https://doi.org/10.1017/CBO9780511800481)
- C. Daskalakis, P. W. Goldberg, C. H. Papadimitriou, *The complexity of computing a Nash equilibrium*, SIAM J. Computing 39 (2009), 195–259. [DOI](https://doi.org/10.1137/070699652)
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).
Cubic Congruence for the q-Secant Inversion EnumeratorResearch Paper
## Motivation
Alternating permutations are a classical meeting point of enumerative combinatorics, permutation statistics, and special functions. An up--down permutation alternates between rises and falls, and their ordinary counts are the Euler secant and tangent numbers. Refining this count by the inversion statistic produces the $q$-secant polynomial $E_{2n}(q)$. Its values and congruences retain information that disappears after setting $q=1$: they distinguish how the alternating permutations are distributed by inversion number and reveal cancellation at roots such as $q=-1$. Ji-Cai Liu's article isolates the next nontrivial term in the $(1+q)$-adic expansion of this polynomial, strengthening an earlier Andrews--Foata congruence. The mission formalizes the article's main result, Theorem 1.1, as an exact polynomial-divisibility statement.
## Setting
For $n\ge 0$, let $A(2n)$ be the set of permutations $\sigma=(\sigma_1,\ldots,\sigma_{2n})$ of $\{1,\ldots,2n\}$ satisfying
$$
\sigma_1<\sigma_2>\sigma_3<\sigma_4>\cdots<\sigma_{2n}.
$$
The empty permutation is the unique member of $A(0)$. The inversion number is
$$
\operatorname{inv}(\sigma)
=\#\{(i,j):1\le i<j\le 2n,\ \sigma_i>\sigma_j\}.
$$
The $q$-secant inversion enumerator is the integer polynomial
$$
E_{2n}(q)=\sum_{\sigma\in A(2n)}q^{\operatorname{inv}(\sigma)}\in\mathbb Z[q].
$$
Congruence modulo $(1+q)^3$ means divisibility in $\mathbb Z[q]$: two polynomials $F$ and $G$ are congruent precisely when $(1+q)^3$ divides $F-G$. This formulation avoids evaluation at a single number and records the first three orders of behavior at $q=-1$.
In Lean, a permutation is represented as an equivalence of `Fin (2*n)`. The alternating inequalities and inversion number are finite predicates and counts on this zero-based type. The polynomial variable is the canonical indeterminate in `Polynomial ℤ`.
## Formalization targets
### Cubic congruence
For every integer $n\ge0$, prove
$$
E_{2n}(q)\equiv
q^{2n(n-1)}-\binom n2(1+q)^2
\pmod{(1+q)^3}.
$$
Equivalently,
$$
(1+q)^3\mid
E_{2n}(q)-
\left(q^{2n(n-1)}-\binom n2(1+q)^2\right)
\quad\text{in }\mathbb Z[q].
$$
The boundary value $n=0$ is included. With the empty-permutation convention and natural-number truncated subtraction in the exponent, both sides reduce correctly, so the formal target does not hide a separate exceptional case.
## Significance
The theorem identifies the exact quadratic correction to the highest-inversion monomial near $q=-1$. It therefore explains why the prior congruence modulo $(1+q)^2$ does not generally lift unchanged to the cubic modulus. Specializing at $q=1$ also yields the corresponding refinement modulo $8$ for the ordinary secant numbers. More broadly, the statement is a compact test case for formal reasoning that combines finite permutations, order predicates, inversion statistics, generating polynomials, binomial coefficients, and divisibility in a polynomial ring.
A machine-checked proof would contribute reusable infrastructure for permutation enumerators and polynomial congruences. The published article supplies a human proof; the Prove2me goal is the formal reconstruction of its theorem in Lean. The mission does not encode a proof certificate, an orbit count, or the desired divisibility inside a definition. A successful submission must derive the divisibility from the concrete finite definitions.
The result also gives a useful interface between two styles of formal combinatorics. On one side, alternating permutations are finite objects that can be enumerated, mapped, and partitioned. On the other, their aggregate is an algebraic object in $\mathbb Z[q]$ whose divisibility can be studied without referring to individual permutations. Infrastructure connecting these levels can be reused for other $q$-Euler numbers, descent and major-index enumerators, and congruences obtained from finite weighted actions. The mission keeps that infrastructure general-purpose by making the final target an equality in a quotient of the polynomial ring rather than a specialized computational procedure.
## Difficulty
Direct expansion of $E_{2n}(q)$ is factorial in $n$ and gives no uniform explanation of divisibility by a third power. Divisibility by $(1+q)^3$ is stronger than merely checking the value at $q=-1$: it simultaneously constrains the value and the first two formal orders there. A formal solution must control the entire finite family of alternating permutations while preserving exact inversion exponents and polynomial coefficients. Index conventions are also delicate, because the paper numbers positions and values from $1$, whereas Lean uses `Fin` indices from $0$.
The source argument introduces combinatorial structure beyond the bare statement. Formalizers may contribute reusable lemmas about switching consecutive values, invariance of alternation under permitted switches, inversion-number changes, finite group actions, and divisibility of orbit enumerators. Those are natural milestones, but the present root goal deliberately remains the stable polynomial congruence rather than committing to one decomposition.
## Formalization scope
The mission fixes the coefficient ring to $\mathbb Z$ and uses exact polynomial divisibility. It does not replace congruence by coefficientwise arithmetic modulo $8$, evaluation at $q=-1$, or a numerical check for bounded $n$. `UpDown` is defined directly on permutations of `Fin (2*n)`, `invNumber` counts ordered index pairs with the required inequality, and `qSecant` is the finite sum of monomials $q^{\operatorname{inv}(\sigma)}$.
The formal statement quantifies over every natural number. The conventions at $n=0$ and $n=1$ are part of the same theorem and have been audited explicitly. The uploaded definition bundle is transparent and sorry-free; the only admitted declaration is the mission theorem itself. Useful contributions include general lemmas about polynomial divisibility, finite involutions and orbit sums, or bridges between one-based paper notation and Lean's finite types.
## Selected references
- Ji-Cai Liu, *A Combinatorial Proof of a Cubic Congruence for the $q$-Secant Inversion Enumerator*, Electronic Journal of Combinatorics 33(3), P3.10, 2026. [DOI](https://doi.org/10.37236/15666)
## 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)
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.
Congruent Numbers — Tunnell's Criterion (Even Case)Open Problem
Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the even case: for squarefree even n, the representation-count identity 2|C_n| = |D_n| — where C_n and D_n count integer solutions of n = 8x² + 2y² + 64z² and n = 8x² + 2y² + 16z² — implies that n is a congruent number.
Congruent Numbers — Tunnell's Criterion (Odd Case)Open Problem
Which whole numbers are the area of a right triangle with rational sides? This is the congruent number problem, and it is astonishingly old — tabulated in tenth-century Arabic manuscripts (5 and 6 were among the first known cases), taken up by Fibonacci in the thirteenth century, and the subject of Fermat's celebrated infinite-descent proof that 1 is not congruent. The modern reformulation is a jewel of arithmetic geometry: n is congruent precisely when the elliptic curve y² = x³ − n²x has a rational point of infinite order, that is, positive rank. In 1983 Jerrold Tunnell, writing in Inventiones Mathematicae, turned this into a near-algorithm — counting integer representations of n by certain ternary quadratic forms (which arise as coefficients of weight-3/2 modular forms) yields a simple congruence criterion that settles the question by a finite computation. The catch, and the reason the problem remains officially open, is that the sufficiency of Tunnell's criterion rests on the Birch and Swinnerton-Dyer conjecture, itself a Millennium Prize Problem. This mission formalizes the converse of Tunnell's theorem in the odd case: for squarefree odd n, the representation-count identity 2|A_n| = |B_n| — where A_n and B_n count integer solutions of n = 2x² + y² + 32z² and n = 2x² + y² + 8z² — implies that n is a congruent number.
That the prime numbers, thinning out as they climb yet never quite vanishing, should nonetheless contain arithmetic progressions of every finite length is one of the most celebrated discoveries of twenty-first-century mathematics. Ben Green and Terence Tao proved it in 2004 (published in the Annals of Mathematics in 2008), resolving a question whose roots reach back to Lagrange and Waring around 1770 and which had crystallized in the Erdős–Turán conjecture. The primes have density zero, so Szemerédi's theorem — which guarantees long progressions only in positive-density sets — does not apply directly; the genius of the proof was a transference principle extending Szemerédi's theorem to sets sitting densely inside a 'pseudorandom' host, built from the sieve ideas of Goldston, Pintz, and Yıldırım. The result was a centerpiece of the citation for Tao's 2006 Fields Medal and opened a whole industry, including the Tao–Ziegler extension to polynomial progressions. Unusually for a headline problem, this theorem is already proved — which makes it an ideal flagship formalization mission: a deep, decomposable argument whose pieces, from Szemerédi's theorem to the transference principle, the community can rebuild and verify in Lean.
In a 1999 Vienna doctoral thesis, Gerhard Zauner conjectured that in every finite dimension d one can find d² unit vectors in complex d-space that are mutually as spread out as possible — any two sharing the same squared overlap 1/(d+1). Such a configuration, a symmetric informationally complete positive operator-valued measure (SIC-POVM), is the optimal minimal measurement for reconstructing an unknown quantum state, which is why the idea was rediscovered and named by Renes, Blume-Kohout, Scott, and Caves in 2004 and became central to quantum tomography, quantum cryptography, and the QBist reading of quantum mechanics. Geometrically these are maximal sets of complex equiangular lines; physically they are the most efficient quantum measurements; and, remarkably, they appear to be governed by deep number theory — recent work by Appleby, Flammia, Kopp, and others ties exact SICs to Stark units and Hilbert's twelfth problem on explicit class field theory. Exact solutions have been hand-built in scores of dimensions and numerical ones found in every dimension checked, yet a general existence proof remains out of reach. Formalizing Zauner's conjecture gives this problem — straddling quantum information, geometry, and algebraic number theory — a precise shared target.
A Hadamard matrix is a square array of +1s and −1s whose rows are mutually orthogonal — equivalently, one whose determinant attains the absolute maximum that Jacques Hadamard proved in 1893 any ±1 matrix can reach. The story opens earlier, with James Joseph Sylvester's 1867 doubling construction producing such matrices in every power-of-two order; Hadamard himself added orders 12 and 20. The conjecture bearing his name asserts that a Hadamard matrix exists for every order divisible by four. Raymond Paley's 1933 construction from finite fields settled vast new families, and computer searches filled stubborn gaps — beginning with order 92 at JPL in 1962 and reaching order 428 only in 2005, after which 668 became the smallest order whose existence is still unknown. Far from a curiosity, these matrices are workhorses of applied mathematics, underpinning error-correcting codes (the Reed–Muller code that sharpened Mariner spacecraft imagery), spread-spectrum and CDMA signal design, optimal statistical designs of experiments, and coded-aperture spectroscopy. Settling the conjecture would close a 130-year-old gap where combinatorics, number theory, and design theory meet.
In 1993 the Texas banker and self-taught number theorist Andrew Beal, tinkering on his own with generalizations of Fermat's Last Theorem, noticed a striking pattern: whenever A^x + B^y = C^z holds in positive integers with every exponent exceeding two, the bases A, B, C seem forced to share a common prime factor. Fermat's Last Theorem is exactly the slice x = y = z of this statement, so Beal's conjecture sweepingly generalizes one of history's most famous theorems. Beal backed his question with money, raising the prize from $5,000 in 1997 to $1,000,000, now held in trust by the American Mathematical Society. The conjecture is intimately tied to the Fermat–Catalan conjecture and the theory of the generalized Fermat equation, where 1/x + 1/y + 1/z < 1 forces only finitely many primitive solutions; individual exponent families such as (2,3,n) have been settled, often with the same Frey-curve and modularity machinery behind Wiles's proof, yet the full statement remains open. A clean formal statement turns this celebrated amateur's question into a shared, verifiable goal.