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.
Positive definite matrix integral inequalityOpen Problem
# Motivation
The source defines a two-variable integral on strictly positive-definite real matrices. Its numerator is the absolute bilinear form of A minus B on two unit vectors, while the denominator uses the quadratic forms of A and B. The desired inequality says that componentwise matrix addition is nonexpansive for this quantity, with the larger of the two input distances controlling the output. The surface measure normalization is immaterial because the same constant multiplies every distance.
This mission turns CUHK-Shenzhen AI Math Problem 1, **Positive definite matrix integral inequality**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
For every positive dimension and every four positive-definite matrices A, B, C, and D, prove d(A+B,C+D) is at most max(d(A,C),d(B,D)). The first milestone fixes dimension one, where the sphere and every matrix entry can be analyzed explicitly.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in matrix analysis, positive definite matrices, integral inequality. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
The absolute value prevents a direct cancellation argument, and the denominators couple each integration variable to a different matrix. Positive definiteness gives pointwise positivity but does not immediately compare the ratios after addition. A successful proof must find a convexity, change-of-measure, or projective-metric mechanism that survives the double integral.
## Suggested attack route
Promising routes include reducing by congruence to normalized matrices, studying the scalar inequality on each pair of directions, and interpreting the denominator as a density change on the sphere. The dimension-one case should reveal the sharp scalar inequality. Numerical experiments in dimensions two and three may identify equality cases, but the Lean proof must ultimately derive every bound from positivity and measurable integration.
## Formalization scope
The Lean model uses finite matrices, Mathlib positive definiteness, the canonical sphere measure obtained from polar decomposition, and an explicit iterated integral. It does not assume symmetry through an unchecked flag: positive definiteness is the Mathlib predicate. Integrability obligations and zero-denominator issues must be proved from positive definiteness.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
## Milestones
Establish the dimension-one specialization, including any exact evaluation of the two-point sphere integral needed by the proof.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on May 28, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original CUHK-Shenzhen problem](https://rybindmitry.github.io/problems/1.html)
Orders of Harmonic Maps into Euclidean BuildingsResearch Paper
## Motivation
Harmonic maps into singular nonpositively curved spaces arise in geometric analysis, rigidity theory, and the study of group actions on buildings. Near a point in the domain, their infinitesimal growth is measured by an **order**, obtained from an Almgren-type frequency quotient. For smooth targets that order is tied to familiar Taylor expansion data. Euclidean buildings are instead assembled from Euclidean apartments along reflection walls, so a map can branch through a singular link and a priori might exhibit a much less controlled spectrum of homogeneities. Breiner and Dees prove that, for maps from surfaces, this spectrum is discrete and is governed by the finite rotational Weyl group of the building. The mission formalizes their headline classification theorem, Theorem 1.1 of [Breiner--Dees](https://doi.org/10.1007/s00526-026-03375-5).
The discreteness matters because frequency information is a basic input to stratification and regularity arguments for singular harmonic maps. A finite list of possible denominators prevents homogeneities from accumulating arbitrarily and isolates rank-one behavior. The formal target makes explicit the nonconstant condition used by the source paper's tangent-map reduction. Without it, the usual numerator and denominator of the frequency quotient both vanish for a constant map, so its order is not defined.
## Setting
A **Euclidean Coxeter complex** consists of Euclidean space together with an affine reflection group. Taking the linear parts of its affine isometries produces a finite rotational reflection group $W$. A **Euclidean building of type $W$** is a complete metric space covered by isometric Euclidean apartments whose overlaps are related by elements of the affine Weyl group; the atlas is required to contain the relevant geodesic segments, rays, and lines and to be maximal with these compatibility properties.
The domain is a connected open subset $D$ of a complex one-dimensional manifold, hence a Riemann surface domain. The formalization uses a concrete Korevaar--Schoen-style metric Sobolev energy built from normalized local difference quotients and Lebesgue area in charts. A map $u:D\to X$ is harmonic when it has finite local energy and minimizes that energy against competitors with the same trace. For $x_0\in D$ and small radii $r$, the energy and boundary moment determine a frequency quotient. When its limit exists with positive denominator, that limit is the order $\operatorname{Ord}_u(x_0)$.
## Formalization targets
### Main classification
For a nonconstant energy-minimizing harmonic map $u:D\to X$ and any $x_0\in D$, prove that the order is defined and that there are positive integers $m,k$ such that
$$
\operatorname{Ord}_u(x_0)=\frac{m}{k},
\qquad k\mid |W|.
$$
If the building has rank one, prove the sharper form
$$
\operatorname{Ord}_u(x_0)=\frac{m}{2}
\qquad\text{for some integer }m\ge 2.
$$
The same theorem also records the small-scale energy and positive-boundary-moment facts needed for the order to be meaningful; these are conclusions, not assumptions supplied by a solver.
## Significance
The result identifies a purely algebraic constraint on an analytic singularity invariant: every denominator divides the order of the finite rotational Weyl group. In rank one, where the target is a tree or an $\mathbb R$-tree, it recovers the half-integer spectrum and its lower bound. This converts an apparently continuous local invariant into a discrete one determined by the building type.
Formalizing the theorem requires reusable infrastructure that is largely absent from current Mathlib: concrete Euclidean-building atlases, metric-valued Sobolev energy, trace and boundary-moment constructions, harmonic energy minimization, frequency quotients, and homogeneous tangent-map interfaces. The paper theorem is proved in ordinary mathematics; the open task is to replace the single `sorry` in the target with a machine-checked Lean proof. A completed development would provide components useful for other singular-target harmonic-map and CAT(0) formalizations.
## Difficulty
The target is not a direct consequence of treating the building as a Euclidean vector space. A harmonic map can cross apartment walls, and a single chart need not contain the image of a punctured neighborhood. The local problem must respect both metric energy and Weyl-group compatibility. Moreover, the frequency quotient is defined through limiting analytic quantities, while the conclusion is an exact rational arithmetic classification. Bridging those levels requires controlling tangent maps and the geometry of directions in the building rather than merely proving monotonicity of the frequency.
The rank-one clause is not obtained by substituting $|W|=2$ into the general statement alone: it also asserts $m\ge2$. The formal proof therefore must preserve the nonconstant hypothesis and the positivity information that rules out the degenerate zero-order case.
## Formalization scope
The Lean bundle fixes a complex one-dimensional manifold model for the source, a genuine complete metric target, a finite affine reflection group acting by Euclidean isometries, and an explicit building atlas. The rotational group $W$ is the image of the affine group under taking linear parts, so $|W|$ is not an arbitrary external number. The domain carries a point $x_0$ and is nonempty by construction. The map is required to be nonconstant on the domain; this is the necessary explicit repair of the printed headline, whose later reduction theorem uses the same condition.
Energy, trace, boundary moment, frequency, and order are transparent definitions tied to the supplied geometry. In particular, the caller cannot choose a zero measure or an unrelated predicate to make the target vacuous. The theorem must establish finite small-scale energy, positivity of the boundary moment, existence of the frequency limit, and its classification. Solvers may contribute supporting files for metric Sobolev estimates, tangent-map compactness, homogeneous harmonic-map classification, or finite-reflection-group lemmas, provided they preserve the exact conventions in the definition bundle.
## Selected references
- Christine Breiner and Ben K. Dees, *On the Possible Orders of Harmonic Maps into Euclidean Buildings*, Calculus of Variations and Partial Differential Equations, 2026, Theorem 1.1 and Sections 2--4. [DOI](https://doi.org/10.1007/s00526-026-03375-5)
- Mikhail Gromov and Richard Schoen, *Harmonic Maps into Singular Spaces and p-adic Superrigidity for Lattices in Groups of Rank One*, Publications Mathématiques de l'IHÉS 76 (1992), 165--246. [EuDML](https://eudml.org/doc/104049)
Arbitrary Torsion in Moment-Angle Homology and Loop HomologyResearch Paper
## Motivation
Moment-angle complexes are central objects in toric topology. They convert the combinatorics of a simplicial complex into a topological space assembled from disks and circles, allowing face structure to influence homotopy and homology. When the simplicial complex triangulates a sphere, the resulting space is a moment-angle manifold. Torsion in the integral homology of these manifolds is difficult to realize in low simplicial dimension, and torsion in the homology of their based loop spaces is even more constrained. Yang Han and Keke Li's Theorem 1.7 asserts that dimension four is already universal: every finitely generated abelian group can occur as a subgroup of both homology theories for one and the same simplicial $4$-sphere.
This mission formalizes that headline existence statement. It is not restricted to a chosen finite list of groups or primes, and it requires a common simplicial sphere rather than permitting separate witnesses for ordinary and loop homology.
## Setting
Let $L$ be an abstract simplicial complex on a finite vertex set $[m]$. Its geometric realization $|L|$ is formed from probability vectors whose supports are faces of $L$. The condition that $L$ is a **simplicial $4$-sphere** means that this realization is homeomorphic to the unit sphere $S^4\subset\mathbb R^5$.
For each face $\sigma\in L$, assign a copy of the closed disk $D^2$ at vertices in $\sigma$ and the boundary circle $S^1$ at vertices outside $\sigma$. The associated moment-angle complex is
$$
\mathcal Z_L
=\bigcup_{\sigma\in L}
\prod_{i=1}^{m}Y_i(\sigma),
\qquad
Y_i(\sigma)=
\begin{cases}
D^2,&i\in\sigma,\\
S^1,&i\notin\sigma.
\end{cases}
$$
The all-ones point is a canonical basepoint. Write $\Omega\mathcal Z_L$ for the based loop space with the compact-open topology. For a space $X$, the mission uses total integral singular homology
$$
H_*(X;\mathbb Z)=\bigoplus_{q\ge0}H_q(X;\mathbb Z)
$$
as an additive abelian group. Saying that an abelian group $G$ is a subgroup means that there is an injective additive homomorphism $G\hookrightarrow H_*(X;\mathbb Z)$.
## Formalization targets
### Arbitrary torsion in one moment-angle manifold
For every finitely generated abelian group $G$, prove that there are an integer $m$ and a simplicial complex $L$ on `Fin m` such that $|L|\cong S^4$ and there are injective homomorphisms
$$
G\hookrightarrow H_*(\mathcal Z_L;\mathbb Z),
\qquad
G\hookrightarrow H_*(\Omega\mathcal Z_L;\mathbb Z).
$$
The quantifier order matters: the same $m$ and the same $L$ must support both embeddings. The target concerns additive subgroups of total graded homology; it does not require the two embeddings to land in the same degree or to preserve multiplicative structures.
## Significance
The theorem gives a universality statement for moment-angle manifolds over simplicial $4$-spheres. It says that no classification by a bounded list of torsion primes or exponents can describe all such homology and loop-homology groups. Requiring both embeddings for a single $L$ connects the ordinary topology of the manifold to its based-loop topology rather than proving two unrelated existence results.
Formalizing the theorem requires reusable foundations in several areas: finite abstract simplicial complexes, geometric realization, polyhedral products, based loop spaces, integral singular homology, graded direct sums, and additive embeddings. The published article presents a human proof; this mission records its intended main theorem as an open Lean target. The definitions do not assume the existence of the required sphere or embeddings, so a solver must supply the mathematical construction and all homological consequences.
## Difficulty
The assertion ranges over arbitrary finitely generated abelian groups, including free parts and prime-power torsion of unbounded exponent. A finite check of selected groups cannot establish the target. The same finite simplicial object must simultaneously control two different homology theories, one of which is applied to an infinite-dimensional function space. Standard library support is strongest for singular homology as a functor, while concrete calculations for moment-angle spaces and loop spaces require additional bridges.
There is also a substantial representation boundary between combinatorics and topology. The face data of $L$, the union of disk-circle products, the homeomorphism $|L|\cong S^4$, and the induced maps on homology must all refer to compatible spaces and basepoints. A formal solution cannot replace “simplicial sphere” by a mere Boolean flag or replace homology by an arbitrary group-valued field.
## Formalization scope
Lean represents $L$ using `AbstractSimplicialComplex (Fin m)`. Because Mathlib's structure includes singleton faces automatically, the auxiliary face predicate explicitly restores the conventional empty face where the moment-angle union needs it. The geometric realization is the standard support-restricted probability simplex, and the sphere condition is an actual homeomorphism to the Euclidean unit $4$-sphere.
The moment-angle space is a subtype of `(Fin m → ℂ)` defined by the literal disk/circle coordinate condition. The loop space consists of based continuous paths with matching endpoints and carries the compact-open topology inherited from Mathlib's path construction. Homology is `singularHomologyFunctor` with coefficients in $\mathbb Z$, and total homology is a direct sum over all natural degrees.
The statement permits the two embeddings to occupy different degrees and makes no ring-embedding claim; these choices match the source phrase “contain $G$ as a subgroup.” It rules out vacuity by requiring an actual simplicial complex, an actual sphere homeomorphism, and injective additive maps. Contributions that isolate degree-specific refinements, compute homology of standard polyhedral products, or formalize reusable loop-space equivalences are welcome, provided they reconnect to the stated root theorem.
## Selected references
- Yang Han and Keke Li, *Moment Angle Manifolds Corresponding to $S^4$ Whose Homology and Loop Homology May Have Arbitrary Torsion*, International Mathematics Research Notices 2026(4), 1--7, 2026. [DOI](https://doi.org/10.1093/imrn/rnag024)
- A. Bahri, M. Bendersky, F. R. Cohen, and S. Gitler, *The polyhedral product functor: a method of decomposition for moment-angle complexes, arrangements and related spaces*, Advances in Mathematics 225(3), 2010, 1634--1668. [DOI](https://doi.org/10.1016/j.aim.2010.04.009)
## Motivation
The simplex method walks along edges of a polytope from vertex to vertex. Whether any pivot rule could ever make that walk short in the worst case is governed by a prior, purely geometric question: how far apart, in the edge graph, can two vertices of a polytope be? Warren Hirsch conjectured in 1957 that the diameter of a $d$-dimensional polytope with $n$ facets is at most $n - d$. Half a century of upper bounds stalled at quasi-polynomial, and Santos disproved the conjecture itself in 2012 — but only by a constant factor. The surviving question, the subject of the Polymath 3 project, is the **polynomial Hirsch conjecture**: is the diameter bounded by a polynomial in $n$ and $d$?
## Timeline
- **1957.** Hirsch states the conjecture $\mathrm{diam} \le n - d$ in a letter to Dantzig, who publishes it in *Linear Programming and Extensions* (1963).
- **1964–1966.** Klee determines the exact maximum diameter of $3$-polytopes with $n$ facets, $\lfloor 2n/3\rfloor - 1$ — the Hirsch bound holds up to dimension three.
- **1967.** Klee and Walkup ([Acta Math.](https://doi.org/10.1007/BF02392971)) refute the *unbounded-polyhedron* version, prove the bounded conjecture for $n - d \le 5$, and reduce the general case to the **$d$-step conjecture** ($n = 2d$).
- **1970.** Larman ([Proc. LMS](https://doi.org/10.1112/plms/s3-20.2.249)) proves $\mathrm{diam} \le n\,2^{d-3}$ — linear in the number of facets for each fixed dimension, still the best bound of that shape.
- **1989.** Naddef ([Math. Programming](https://doi.org/10.1007/BF01589418)) proves $0/1$-polytopes satisfy the Hirsch bound, with diameter at most $d$.
- **1992.** Kalai and Kleitman ([Bull. AMS](https://arxiv.org/abs/math/9204233)) prove $\mathrm{diam} \le n^{\log_2 d + 2}$ in under a page — the quasi-polynomial barrier every later bound refines. The same year brings subexponential pivot rules (Kalai; Matoušek–Sharir–Welzl), the algorithmic counterpart.
- **2010.** Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR](https://doi.org/10.1287/moor.1100.0470)) show the known upper-bound arguments survive in a purely combinatorial abstraction — which admits almost-quadratic lower bounds, so a polynomial bound must use real geometry. Kalai launches **Polymath 3** on the polynomial version.
- **2010–2012.** Santos ([Annals of Math.](https://arxiv.org/abs/1006.2814)) disproves the Hirsch conjecture: a $43$-dimensional polytope with $86$ facets and diameter at least $44$, via spindles of large width.
- **2014–2019.** Todd ([SIAM J. Discrete Math.](https://arxiv.org/abs/1402.3579)) sharpens Kalai–Kleitman to $(n-d)^{\log_2 d}$; Sukegawa refines further. Matschke, Santos, and Weibel ([Proc. LMS 2015](https://arxiv.org/abs/1202.4701)) shrink the counterexample to dimension $20$ with $40$ facets and diameter $21$. All known violations remain constant-factor; all known bounds remain quasi-polynomial.
## Setting
Work in $\mathbb{R}^d$. An **H-polytope** is a set cut out by finitely many linear inequalities: given vectors $a_1, \dots, a_n \in \mathbb{R}^d$ and reals $b_1, \dots, b_n$, it is
$$P \;=\; \{\, x \in \mathbb{R}^d \mid \langle a_i, x\rangle \le b_i \text{ for } i = 1, \dots, n \,\},$$
where $\langle a_i, x\rangle = \sum_{j=1}^d a_{ij} x_j$ is the standard inner (dot) product — so each condition $\langle a_i, x\rangle \le b_i$ is one linear inequality, with normal vector $a_i$ and offset $b_i$. Throughout, $P$ is assumed nonempty and bounded. The parameter $n$ counts the inequalities in the given description; since every polytope with $f$ facets admits a description by exactly $f$ inequalities, bounds stated in terms of $n$ over all descriptions are equivalent to bounds in terms of facet counts.
A **vertex** of $P$ is an extreme point. Two vertices $u \ne v$ are **adjacent** when the segment $[u, v]$ is an extreme subset of $P$; for a polytope the convex extreme subsets are exactly the faces, so this says precisely that $[u,v]$ is a one-dimensional face — an **edge**. The **combinatorial diameter** of $P$ is the diameter of the graph of vertices and edges. Throughout, "diameter at most $B$" is expressed as: every two vertices are joined by a walk of $B$ steps, each step staying put or crossing an edge — a form that is monotone in $B$ and asserts connectivity of the graph (Balinski's theorem) as part of the claim.
## Formalization targets
### Goal — the polynomial Hirsch conjecture
$$\exists\, c, k \in \mathbb{N}:\ \text{every nonempty bounded } P = \{x \in \mathbb{R}^d \mid \langle a_i, x \rangle \le b_i,\ i \le n\} \text{ has diameter} \le c\,(n + d)^k.$$
Every polynomial in $n$ and $d$ is dominated by some $c(n+d)^k$ and conversely, so this is exactly polynomiality, with no committed degree — the form that survives any future sharpening of constants or exponents.
### Milestones — the known ladder
Six classical results over the same definitions: the Hirsch bound $n - d$ in dimension $d \le 3$ (Klee; Klee–Walkup); Larman's bound $n \cdot 2^{d-3}$; Naddef's bound $d$ for $0/1$-polytopes; the Kalai–Kleitman bound $n^{\log_2 d + 2}$; Todd's bound $(n-d)^{\log_2 d}$ for full-dimensional $P$ with $n \ge d \ge 3$; and — in the other direction — the Santos counterexample: a nonempty bounded H-polytope whose diameter exceeds $n - d$.
## Significance
A polynomial diameter bound is necessary for any pivot rule of the simplex method to run in polynomial time in the worst case: if vertices can be super-polynomially far apart, no edge-following algorithm can connect them quickly. A refutation would close off one of the main hoped-for routes to a strongly polynomial linear programming algorithm (Smale's ninth problem). The conjecture is also the test question of polyhedral graph theory: the Kalai–Kleitman argument uses so little about polytopes that it holds for far more general set systems, and Eisenbrand, Hähnle, Razborov, and Rothvoß ([Math. OR 2010](https://doi.org/10.1287/moor.1100.0470)) showed such abstractions admit almost-quadratic lower bounds — so a proof of the conjecture must use geometry the abstract setting lacks, and a disproof must beat the abstraction barrier's constructions with actual polytopes.
None of these results has been formalized in any proof assistant; Mathlib has extreme points and faces of convex sets, but no polytope combinatorics — no vertex-edge graph, no diameter, no facet counting. This mission builds that layer: an H-polytope model, adjacency via faces, and walk-based diameter bounds, against which both the upper-bound ladder and the Santos disproof can be machine-checked. The Kalai–Kleitman proof is one page from first principles and is the natural summit; the Santos construction is a concrete finite object whose verification is a different, computational kind of challenge.
## Difficulty
The naive approach — walk toward the target vertex by always improving some linear objective — is exactly the simplex method, and proving *any* polynomial bound on such walks is open for every known pivot rule; monotone variants of the diameter question have exponential lower bounds. The obvious inductive strategy (bound the diameter by recursing on facets) is precisely what Kalai–Kleitman optimizes, and it provably cannot go below quasi-polynomial without using metric or topological properties of actual polytopes, by the abstraction lower bound above. On the other side, making diameters *large* is blocked by the wedge/spindle calculus only producing constant-factor violations. The problem sits in a genuine gap: no technique on either side is known to reach polynomial.
## Formalization scope
The Lean model commits to: ambient space `EuclideanSpace ℝ (Fin d)`; the polytope as `Hpoly a b = {x | ∀ i, ⟪a i, x⟫ ≤ b i}` for `a : Fin n → EuclideanSpace ℝ (Fin d)`, `b : Fin n → ℝ`, with nonemptiness and `Bornology.IsBounded` as explicit hypotheses (boundedness is essential: Klee–Walkup's *unbounded* counterexample would otherwise trivialize the Santos milestone); vertices as `Set.extremePoints ℝ`; adjacency as `u ≠ v ∧ IsExtreme ℝ P (segment ℝ u v)`; and diameter bounds as the walk predicate `DiamLE`, whose stationary steps make it monotone in the bound. Real-exponent bounds enter through `Real.logb` and the natural floor. In `larman_bound` and the two Hirsch-form bounds the subtraction is natural-number (truncated) subtraction, which only weakens nothing: the stated forms are true as written for all $n, d$ in scope. The dimension parameter $d$ is the ambient dimension; lower-dimensional polytopes are included, and every milestone is stated so as to remain true for them, with `todd_bound` requiring full-dimensionality (`(interior P).Nonempty`) as in its source.
Welcome contributions: any milestone in any order (`dimension_three_bound` for $d \le 1$ cases and structural lemmas about `Adj` and `DiamLE` are natural entry points, and `kalai_kleitman_bound` is the summit); reusable infrastructure — polytopes have finitely many extreme points, faces of H-polytopes, Balinski connectivity — published as platform theorems; and, as a separate expedition, the explicit Santos or Matschke–Santos–Weibel polytope. Statements about unbounded polyhedra, the simplex method itself, and subexponential pivot rules are left to future missions.
## Selected references
- V. Klee, D. Walkup, *The d-step conjecture for polyhedra of dimension d < 6*, Acta Math. 117 (1967). [doi:10.1007/BF02392971](https://doi.org/10.1007/BF02392971)
- D. Larman, *Paths on polytopes*, Proc. London Math. Soc. 20 (1970). [doi:10.1112/plms/s3-20.2.249](https://doi.org/10.1112/plms/s3-20.2.249)
- D. Naddef, *The Hirsch conjecture is true for (0,1)-polytopes*, Math. Programming 45 (1989). [doi:10.1007/BF01589418](https://doi.org/10.1007/BF01589418)
- G. Kalai, D. Kleitman, *A quasi-polynomial bound for the diameter of graphs of polyhedra*, Bull. AMS 26 (1992). [arXiv:math/9204233](https://arxiv.org/abs/math/9204233)
- F. Santos, *A counterexample to the Hirsch conjecture*, Annals of Mathematics 176 (2012). [arXiv:1006.2814](https://arxiv.org/abs/1006.2814)
- M. Todd, *An improved Kalai–Kleitman bound for the diameter of a polyhedron*, SIAM J. Discrete Math. 28 (2014). [arXiv:1402.3579](https://arxiv.org/abs/1402.3579)
- B. Matschke, F. Santos, C. Weibel, *The width of five-dimensional prismatoids*, Proc. London Math. Soc. 110 (2015). [arXiv:1202.4701](https://arxiv.org/abs/1202.4701)
- F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, *Diameter of polyhedra: limits of abstraction*, Math. Oper. Res. 35 (2010). [doi:10.1287/moor.1100.0470](https://doi.org/10.1287/moor.1100.0470)
- F. Santos, *Recent progress on the combinatorial diameter of polytopes and simplicial complexes*, TOP 21 (2013) (survey). [arXiv:1307.5900](https://arxiv.org/abs/1307.5900)
## Motivation
The $k$-server problem was introduced by Manasse, McGeoch, and Sleator ([STOC 1988 / J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) as a common generalization of paging, weighted caching, and related sequential decision problems, and their **$k$-server conjecture** has since become the central open question of competitive analysis. The conjecture asserts that a single ratio — exactly $k$ — governs deterministic online server management on *every* metric space.
## Timeline
- **1985.** Sleator and Tarjan introduce competitive analysis — an online algorithm judged against the offline optimum on every input — for list update and paging, and ask for a theory of such guarantees.
- **1988–1990.** Manasse, McGeoch, and Sleator introduce the $k$-server problem ([STOC 1988; J. Algorithms 1990](https://doi.org/10.1016/0196-6774(90)90003-W)) and settle its extremes: no deterministic algorithm beats ratio $k$ on any space with more than $k$ points (Corollary 7), two servers admit a $2$-competitive algorithm (Theorem 5, algorithm RES), and $k$ servers on $k+1$ points admit a $k$-competitive one (Theorem 4, algorithm BAL). Section 8 poses the **$k$-server conjecture**, in the symmetric finite setting of the paper.
- **1990.** Fiat, Rabani, and Ravid ([FOCS 1990](https://doi.org/10.1109/FSCS.1990.89566)) give the first competitive ratio depending on $k$ alone — exponential in $k$, but finite on every metric space.
- **1991.** Chrobak, Karloff, Payne, and Vishwanathan ([SIAM J. Discrete Math.](https://doi.org/10.1137/0404017)) prove the conjecture on the real line via **Double Coverage**; Chrobak and Larmore ([SIAM J. Comput.](https://doi.org/10.1137/0220008)) extend it to all tree metrics.
- **1995.** Koutsoupias and Papadimitriou ([J. ACM](https://doi.org/10.1145/210118.210128)) prove the **Work Function Algorithm** is $(2k-1)$-competitive on every metric space — the breakthrough, and still the best general bound. Their Conjecture 1.1 fixes the conjecture's modern form: *for every metric space there is an online algorithm with competitive ratio $k$.*
- **1996.** The same authors verify the conjecture on spaces of $k+2$ points via the dual **2-evader problem** (Inf. Process. Lett. 57).
- **2004.** Bartal and Koutsoupias prove the WFA itself is $k$-competitive on the line, weighted stars, and all spaces of $k+2$ points.
- **2021.** Coester and Koutsoupias ([ICALP](https://arxiv.org/abs/2102.10474)) give a unifying potential for all known WFA analyses and push the frontier to the circle.
- **2023.** Bubeck, Coester, and Rabani ([STOC](https://arxiv.org/abs/2211.05753)) refute the *randomized* analogue: no $o(\log^2 k)$-competitive randomized algorithm exists in general. The deterministic conjecture — this mission's goal — survives as the central open question, with the gap between $k$ and $2k-1$ unmoved since 1995.
## Setting
Fix a metric space $M$ with distance function $d$, and a number of servers $k \ge 1$. A **configuration** records where the $k$ servers stand: it is a function $C$ assigning to each server $i \in \{1, \dots, k\}$ a point $C(i) \in M$. Moving the servers from configuration $C$ to configuration $C'$ means server $i$ travels from $C(i)$ to $C'(i)$; the **movement cost** is the total distance traveled,
$$\mathrm{moveCost}(C, C') \;=\; \sum_{i=1}^{k} d\bigl(C(i),\, C'(i)\bigr).$$
A **request sequence** is a finite list $\sigma = (r_1, \dots, r_n)$ of points of $M$, presented one at a time; write $\sigma_{\le j} = (r_1, \dots, r_j)$ for the list of the first $j$ requests (so $\sigma_{\le 0}$ is the empty list).
A **deterministic online algorithm** $A$ is a rule that, for every finite request sequence $\ell$, specifies a configuration $A(\ell)$ — where the servers stand after serving the requests of $\ell$ in order. In particular $A(\text{empty list})$ is the **initial configuration**, before any request arrives. Two points about this way of modeling an algorithm:
- *Online and deterministic, by construction.* The configuration after $j$ requests is $A(\sigma_{\le j})$, a function of those first $j$ requests only — the algorithm cannot see the future, and makes no random choices.
- *The service constraint.* Whenever a request sequence ends with a request $r$, some server must stand at $r$ immediately after: for every list $\ell$ and every point $r$, the configuration reached after serving $\ell$ followed by $r$ places at least one server at the point $r$.
Running $A$ on $\sigma = (r_1, \dots, r_n)$ produces the configurations $A(\sigma_{\le 0}),\, A(\sigma_{\le 1}),\, \dots,\, A(\sigma_{\le n})$, and its **cost** is the total movement along this trajectory:
$$\mathrm{cost}_A(\sigma) \;=\; \sum_{j=1}^{n} \mathrm{moveCost}\bigl(A(\sigma_{\le j-1}),\, A(\sigma_{\le j})\bigr).$$
For comparison, an **offline schedule** for $\sigma$ starting at a configuration $C_0$ is any sequence of configurations $S_0 = C_0, S_1, \dots, S_n$ in which $S_j$ places a server at the request $r_j$, for each $j$ — chosen with the whole of $\sigma$ known in advance. The **optimal offline cost** $\mathrm{OPT}(C_0, \sigma)$ is the infimum, over all such schedules, of the total movement $\sum_{j=1}^{n} \mathrm{moveCost}(S_{j-1}, S_j)$.
Finally, $A$ is **$c$-competitive** if there is a constant $a$ — depending on the algorithm, hence possibly on the metric space and the initial configuration, but never on the request sequence — with
$$\mathrm{cost}_A(\sigma) \;\le\; c \cdot \mathrm{OPT}\bigl(A(\text{empty list}),\, \sigma\bigr) + a \qquad \text{for every request sequence } \sigma.$$
## Formalization targets
### Goal — the $k$-server conjecture
$$\text{For every } k \ge 1,\ \text{every metric space } M,\ \text{and every initial configuration } C_0:\ \exists\, A \text{ starting at } C_0 \text{ that is } k\text{-competitive.}$$
The goal fixes no algorithm: any $k$-competitive construction settles it. This is the weakest stable form of the conjecture — it survives every improvement in constants or techniques short of a disproof.
### Milestones — the known ladder
The milestones are the classical results between the trivial and the conjectured, each an existence or impossibility statement over the same definitions: the lower bound $c \ge k$ on any space with at least $k+1$ points; the conjecture for $k = 2$; for spaces of exactly $k+1$ points; for the real line; the $(2k-1)$ upper bound of the Work Function Algorithm on every space; the conjecture for spaces of exactly $k+2$ points; the conjecture for three servers in the Manhattan plane $(\mathbb{R}^2, \ell^1)$ — the one settled case over a genuinely two-dimensional continuum (Bein–Chrobak–Larmore 2002; reproved by the unifying potential of Coester–Koutsoupias 2021); Coester–Koutsoupias's 2021 result that the Work Function Algorithm *itself* — not just some algorithm — is $3$-competitive for three servers on trees, stated over an explicit formalization of the WFA; and the 2023 Bubeck–Coester–Rabani refutation of the *randomized* analogue: there are $(k+1)$-point spaces on which every randomized algorithm is $\Omega(\log^2 k)$-competitive, stated over a mixed-strategy model of randomized online algorithms.
## Significance
A proof of the conjecture would close the founding problem of competitive analysis and pin down the exact power of determinism in online optimization over arbitrary metrics; a disproof would separate general metric spaces from every special class where the ratio $k$ is known tight. Either outcome recalibrates the field's standard model of adversarial request sequences.
None of these results — not even the lower bound — has a machine-checked proof, and online algorithms as a subject are absent from Mathlib. This mission builds the base layer: a faithful model of online service systems (configurations, online algorithms as prefix functions, offline schedules, competitiveness), the classical possibility and impossibility results over it, and, at the top, the Koutsoupias–Papadimitriou bound, whose potential-function argument is self-contained but delicate. The model is reusable for paging, weighted caching, metrical task systems, and the randomized $k$-server problem.
## Difficulty
The obvious first idea — the greedy algorithm, moving the nearest server to each request — is not competitive for any constant, already on three points of the line: two nearby points can ping-pong one server forever while a server parked slightly farther away never moves. Every known competitive algorithm must sometimes move a server *other than* the nearest one, and the whole difficulty of the conjecture is quantifying exactly how much such foresight-free hedging can achieve. The Work Function Algorithm's analysis via a potential over offline work functions loses a factor of two for reasons nobody has been able to remove; on the lower-bound side, no metric space is known where the deterministic ratio exceeds $k$.
## Formalization scope
The Lean model commits to: configurations as functions `Fin k → M` (**labeled** servers — equivalent in cost to the unlabeled multiset model, since offline can permute labels for free); algorithms as total functions `List M → (Fin k → M)` with the service constraint, so a step may move several servers (the standard laziness reduction makes this equivalent to one-move-per-request); costs in `ℝ` via `Metric.dist`; the offline optimum as an `sInf` over schedules, which agrees with the attained minimum on finite spaces; and the additive-constant form of competitiveness, quantified as `∃ a, ∀ σ`.
Two conventions guard against trivialization. The additive constant is quantified *before* the request sequence — allowing it to depend on $\sigma$ would make every algorithm $1$-competitive. And the lower-bound milestone requires $k+1$ *distinct* points (`Finset.card = k + 1`); on spaces with at most $k$ points the conjecture is trivially true and the lower bound false.
Three further definitional layers extend the model. The **work function** `workFunction C₀ σ C` is the `sInf` of (schedule cost + final move to `C`) over schedules serving `σ` from `C₀`, and the **Work Function Algorithm** `WFA` is defined on finite spaces with `k ≥ 1` servers: after each request it moves to a configuration containing the request minimizing (movement cost) + (work function of the history including the request), a minimizer existing by finiteness and ties broken by a fixed arbitrary choice — matching the standard definition with its "ties broken arbitrarily" (our fixed choice is one admissible instance). A **tree** is a finite metric space carrying a tree graph whose weighted path lengths realize the metric — exactly "the set of vertices of a tree" of the sources. A **randomized algorithm** is a mixed strategy: a probability measure over an index type together with a deterministic algorithm per outcome and measurable per-sequence cost; its expected cost is a lower Lebesgue integral in $[0,\infty]$, and $c$-competitiveness from $C_0$ demands every outcome start at $C_0$ and one additive constant work for all request sequences.
Welcome contributions: proofs of any milestone in any order (the lower bound and the $(k+1)$-point case are the natural entry points); alternative algorithms for milestones already closed; and infrastructure lemmas about `moveCost`, schedules, and work functions published as reusable platform theorems.
## Selected references
- M. Manasse, L. McGeoch, D. Sleator, *Competitive algorithms for server problems*, J. Algorithms 11 (1990). [doi:10.1016/0196-6774(90)90003-W](https://doi.org/10.1016/0196-6774(90)90003-W)
- A. Fiat, Y. Rabani, Y. Ravid, *Competitive k-server algorithms*, FOCS 1990. [doi:10.1109/FSCS.1990.89566](https://doi.org/10.1109/FSCS.1990.89566)
- M. Chrobak, H. Karloff, T. Payne, S. Vishwanathan, *New results on server problems*, SIAM J. Discrete Math. 4 (1991). [doi:10.1137/0404017](https://doi.org/10.1137/0404017)
- M. Chrobak, L. Larmore, *An optimal on-line algorithm for k servers on trees*, SIAM J. Comput. 20 (1991). [doi:10.1137/0220008](https://doi.org/10.1137/0220008)
- E. Koutsoupias, C. Papadimitriou, *On the k-server conjecture*, J. ACM 42 (1995). [doi:10.1145/210118.210128](https://doi.org/10.1145/210118.210128)
- E. Koutsoupias, C. Papadimitriou, *The 2-evader problem*, Inf. Process. Lett. 57(5) (1996), 249–252.
- C. Coester, E. Koutsoupias, *Towards the k-server conjecture: a unifying potential, pushing the frontier to the circle*, ICALP 2021. [arXiv:2102.10474](https://arxiv.org/abs/2102.10474)
- S. Bubeck, C. Coester, Y. Rabani, *The randomized k-server conjecture is false!*, STOC 2023. [arXiv:2211.05753](https://arxiv.org/abs/2211.05753)
- E. Koutsoupias, *The k-server problem* (survey), Computer Science Review 3 (2009). [doi:10.1016/j.cosrev.2009.04.002](https://doi.org/10.1016/j.cosrev.2009.04.002)
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.
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$.
Lagarias criterion is equivalent to RHResearch Paper
## Motivation
The **Riemann hypothesis** concerns the zeros of a complex analytic function, yet it admits an equivalent formulation involving only positive integers, finite sums, the real exponential, and the natural logarithm. Jeffrey C. Lagarias established this formulation in *An Elementary Problem Equivalent to the Riemann Hypothesis* ([Theorem 1.1](https://arxiv.org/abs/math/0008177v2)). It connects the distribution of divisors of an integer with the analytic behavior of the zeta function. For number theorists and formalizers, the interest lies in making that connection precise without confusing an elementary statement with an elementary proof.
The objective is the known equivalence selected by LeanEval v1, not a resolution of RH. Lagarias's paper builds on results of Guy Robin concerning large values of the divisor-sum function; those results remain substantial parts of the formalization workload ([Lagarias, §3](https://arxiv.org/abs/math/0008177v2)).
## Setting
For a positive integer $n$, its **divisor sum** is
$$\sigma(n)=\sum_{d\mid n}d,$$
where the sum runs over positive divisors, including $1$ and $n$. Its **harmonic number** is
$$H_n=\sum_{j=1}^{n}\frac1j.$$
All inequalities below are inequalities of real numbers. The symbols $\exp$ and $\log$ denote the real exponential and natural logarithm. The **Euler–Mascheroni constant** is $\gamma=\lim_{n\to\infty}(H_n-\log n)$.
The **Riemann zeta function** is obtained by analytic continuation of $\sum_{m=1}^{\infty}m^{-s}$ from $\operatorname{Re}(s)>1$. RH asserts that its nontrivial zeros have real part $1/2$. The **Lagarias elementary criterion** in this mission is the assertion that $\sigma(n)\le H_n+\exp(H_n)\log(H_n)$ for every positive integer $n$. These conventions agree with the arithmetic quantities in [Lagarias, Problem E](https://arxiv.org/abs/math/0008177v2), with the precise equality-clause distinction stated below.
## Formalization targets
### Main goal: the exact LeanEval equivalence
$$\mathrm{RH}\quad\Longleftrightarrow\quad
\forall n\in\mathbb N,\;n>0\Longrightarrow
\sigma(n)\le H_n+\exp(H_n)\log(H_n).$$
There are no hypotheses on the goal theorem. The quantifier ranges over all positive integers, not a bounded test set or an unspecified tail. The benchmark uses a non-strict inequality and does not include an equality characterization. Lagarias's Problem E additionally requires equality only at $n=1$; the proof of the reverse implication in [Theorem 1.1, p. 8](https://arxiv.org/abs/math/0008177v2) uses the non-strict inequality alone. The stronger source formulation is therefore not silently substituted for the benchmark.
### Supporting targets from the paper
The milestone list records the following source statements, with their thresholds unchanged:
* Lemma 3.1: for $n\ge3$,
$$e^\gamma n\log\log n\le\exp(H_n)\log(H_n).$$
* Lemma 3.2: for $n\ge20$,
$$H_n+\exp(H_n)\log(H_n)\le e^\gamma n\log\log n+\frac{7n}{\log n}.$$
* The finite check in the proof of Theorem 1.1: the criterion holds for $1\le n\le5040$, with equality exactly at $n=1$.
* Proposition 3.1, attributed to Robin: assuming RH, for $n\ge5041$,
$$\sigma(n)\le e^\gamma n\log\log n.$$
* Proposition 3.2, attributed to Robin: if RH is false, some fixed $0<\beta<1/2$ and $C>0$ satisfy
$$\sigma(n)\ge e^\gamma n\log\log n+
\frac{Cn\log\log n}{(\log n)^\beta}$$
for arbitrarily large integers $n$.
All five are taken from [Lagarias, §3, pp. 6–8](https://arxiv.org/abs/math/0008177v2); the finite check is explicitly an unnumbered step, not a newly attributed lemma.
## Significance
The result identifies an exact arithmetic reformulation of RH. It does not make either side unconditional. A proof of the equivalence gives a bridge between statements in different mathematical languages; it does not certify the universal inequality merely because many instances can be checked. This distinction is central to the interpretation of [Lagarias's theorem](https://arxiv.org/abs/math/0008177v2).
The formalization would connect existing Mathlib definitions of the zeta function, divisor sums, harmonic numbers, and Euler's constant through a machine-checked argument. Reusable outputs include explicit harmonic/exponential comparisons, certified finite real inequalities, and formal versions of Robin's conditional and oscillation results. The mathematical results are known; this proposal supplies open formalization targets, not completed proofs. No accepted LeanEval result is claimed by creating or launching the mission.
## Difficulty
The elementary appearance of the criterion hides its main analytic requirements. Bounding the divisor sum crudely, or checking any finite number of integers, cannot establish the universal equivalence. The conditional upper bound and especially the quantitative oscillation theorem connect zeta zeros with unusually large divisor sums. They must be proved, not packaged as definitions or presumed available because the paper cites them ([Lagarias, Propositions 3.1–3.2](https://arxiv.org/abs/math/0008177v2)).
The oscillation statement requires uniform positive constants and arbitrarily large indices. Replacing it with one counterexample loses essential information. The bounded computation also requires rigorous control of exponential and logarithmic values: an ordinary floating-point loop is not a Lean proof. Beyond the listed milestones, completion still requires standard growth comparisons, threshold bookkeeping, and assembly of the two implications. The short length of the source's final argument should not be read as an estimate of total formalization effort.
## Formalization scope
The goal is `LeanEval.NumberTheory.riemann_hypothesis_iff_lagarias_elementary_criterion`, with type `RiemannHypothesis ↔ LagariasElementaryCriterion`. The criterion definition is copied from the benchmark. `σ 1 n` is natural-valued and cast to the reals; `harmonic n` is rational-valued and cast to the reals. RH remains Mathlib's predicate on `riemannZeta`, excluding negative even trivial zeros and the point $s=1$. No replacement axiom, hidden RH assumption, altered zeta function, or circular child restatement is permitted.
The goal excludes $n=0$ and includes $n=1$. Thresholds ensure positive logarithm arguments in the analytic milestones. The oscillation milestone expresses an infinite subset of the naturals as an unbounded set, retaining $n\ge3$; deletion of the finitely many smaller indices does not change the source's infinitude claim. Its real exponent is represented by `Real.rpow`, not natural exponentiation. Constants are chosen before the arbitrary cutoff.
The benchmark pins Lean 4.33.0 and Mathlib `6f1ef4e5dd604a435bddba4747b13970cd65d2a1`. The proposal targets Prove2me's supported Lean 4.33.1 environment, Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`. These environments are distinct; eventual benchmark credit requires the benchmark's own validation. Contributions to analytic infrastructure, source-faithful supporting results, and certified finite inequalities are welcome. The five milestones are an initial source-backed structure, not a claim that all required infrastructure is already present.
## Selected references
* Jeffrey C. Lagarias, *An Elementary Problem Equivalent to the Riemann Hypothesis*, American Mathematical Monthly **109** (2002), 534–543. [arXiv:math/0008177v2](https://arxiv.org/abs/math/0008177v2), posted 6 May 2001. The theorem, proposition, equation, and page numbers in this proposal refer to this nine-page arXiv version.
* Guy Robin, *Grandes valeurs de la fonction somme des diviseurs et hypothèse de Riemann*, Journal de Mathématiques Pures et Appliquées **63** (1984), 187–213. [Bibliography entry [18] in Lagarias](https://arxiv.org/abs/math/0008177v2). The milestone formulations are those explicitly reproduced and attributed in Lagarias's Propositions 3.1 and 3.2.
Ordinary p-adic L-functions: Mazur–Tate–Teitelbaum interpolationResearch Paper
## Why construct a p-adic L-function?
A modular form has a complex L-function whose critical values carry arithmetic information. To compare those values in p-adic families, their transcendental period factors must first be removed. The remaining algebraic numbers can then be embedded into a p-adic field. The result sought here is a single bounded measure encoding the critical values of all twists by characters of p-power conductor. This is the existence and interpolation theorem underlying the cyclotomic p-adic L-function (one of the most fundamental objects of Iwasawa theory).
The reference is the famous paper of Mazur, Tate and Teitelbaum, Chapter I, especially §§10–14 ([MTT](https://doi.org/10.1007/BF01388731)); but for simplicity we are treating only the ordinary case here (not the more general finite-slope case), and not attacking the results later in MTT (exceptional-zero conjectures, etc).
## Modular forms, periods, and measures
Fix a prime $p$, a positive integer $N$, and a weight $k\ge2$. Let $f$ be a normalized cuspidal Hecke eigenform of weight $k$ on $\Gamma_1(N)$ with nebentypus $\epsilon$ and Fourier coefficients $a_n$ (necessarily algebraic). Fix embeddings $\iota_\infty:\overline{\mathbb Q}\hookrightarrow\mathbb C$ and $\iota_p:\overline{\mathbb Q}\hookrightarrow\mathbb C_p$. No condition $p\nmid N$ is imposed. The character $\epsilon$ is extended by zero on nonunits modulo $N$.
The form is **ordinary** when $|\iota_p(a_p)|_p=1$. The **ordinary root** $\alpha$ is the root of
$$X^2-\iota_p(a_p)X+\iota_p(\epsilon(p))p^{k-1}$$
with $|\alpha|_p=1$. This convention also covers the $U_p$ case: if $p\mid N$, then $\epsilon(p)=0$ and the unit root is $\iota_p(a_p)$ ([MTT I.§12](https://doi.org/10.1007/BF01388731)).
A **measure** means a continuous $\mathbb C_p$-linear functional on the continuous functions $C(\mathbb Z_p^\times,\mathbb C_p)$. It is a bounded p-adic measure, rather than a positive real-valued measure. The Lean representation is Mathlib's `AbstractMeasure` on `(PadicInt p)ˣ`.
The two **periods** $\Omega^+$ and $\Omega^-$ normalize the signed modular integrals. Write
$$\Phi_j(r)=2\pi\int_0^\infty f(r+it)(r+it)^j\,dt,$$
and use $(\Phi_j(r)+s(-1)^j\Phi_j(-r))/2$ for sign $s\in\{+1,-1\}$. A period system specifies nonzero periods, algebraic normalized values for $0\le j\le k-2$, and finite generation over $\mathbb Z$ of the lattice generated by these values. Period rationality and finite generation are separate mathematical obligations, combining Manin–Shimura rationality with the module-of-values construction in [MTT I.§2](https://doi.org/10.1007/BF01388731); see also the explicit treatment of general eigenforms in [Williams, §11.7](https://warwick.ac.uk/fac/sci/maths/people/staff/cwilliams/lecturenotes/lecture_notes_part_ii.pdf).
## Formalization targets
The goal is to construct an ordinary root, a period system, and a measure $\mu$ with the following interpolation property. Let $\chi$ be a primitive Dirichlet character of conductor $m=p^n$, where $n\ge0$, and let $0\le j\le k-2$. Put $s=\chi(-1)(-1)^j$. With the positive-exponential Gauss sum $\tau(\chi)=\sum_{a\bmod m}\chi(a)e^{2\pi ia/m}$, define the algebraic number $A_{\chi,j}$ by
$$\iota_\infty(A_{\chi,j})=
\frac{m^{j+1}j!}{(-2\pi i)^j\tau(\chi^{-1})\Omega^s}
L(f_{\chi^{-1}},j+1).$$
The required identity is
$$\int_{\mathbb Z_p^\times}\iota_p(\chi(x))x^j\,d\mu(x)
=e_p(\alpha,\chi,j)\,\iota_p(A_{\chi,j}),$$
where all algebraic character values in the following expression are transported by $\iota_p$:
$$e_p(\alpha,\chi,j)=\alpha^{-n}
\left(1-\frac{\iota_p(\chi^{-1}(p)\epsilon(p))p^{k-2-j}}{\alpha}\right)
\left(1-\frac{\iota_p(\chi(p))p^j}{\alpha}\right).$$
This is the scalar period-normalized form of [MTT I.§14](https://doi.org/10.1007/BF01388731). At $n>0$ both character values at $p$ vanish, leaving $\alpha^{-n}$. At $n=0$ the primitive character is the character of modulus one, and both Euler factors remain. The latter case is included explicitly.
Seven milestones isolate period rationality and its finite lattice; existence and uniqueness of the ordinary root; the distribution relation for polynomial disk moments; uniform boundedness of constant disk masses; unique extension to a measure with every critical polynomial moment; the complex Birch–Mellin identity; and the deduction of interpolation from the two signed measures. Their source locations are recorded individually. The period milestone combines two standard inputs; the boundedness and extension milestones specialize the MTT construction to slope zero.
## What the formalization supplies
The result supplies the analytic input for studying p-adic special values and their variation. It also supplies reusable infrastructure for normalized modular integrals, rational period systems, finite-order twists, and bounded measures on p-adic units. The classical existence theorem is known. The work proposed here is to prove the stated Lean theorems and connect the existing Mathlib analytic and algebraic infrastructure. Local compilation establishes that the declarations are well-typed; the mission statements remain unproved targets.
## Where the difficulty lies
Listing algebraic critical values does not establish that one bounded measure interpolates them. Values on nested residue disks must satisfy compatibility, and ordinary boundedness must control the extension to continuous functions. Polynomial moments of positive degree must agree with that same extension. The unramified character requires its own Euler-factor calculation; simply applying the ramified formula at conductor one loses factors. On the complex side, rationality requires genuine periods of the modular form, not arbitrary chosen scaling constants. These are the obligations represented by the milestones.
## Formalization scope and conventions
The cusp form is Mathlib's analytic `CuspForm`, with Fourier coefficients tied to its width-one q-expansion. The nebentypus transformation law and every prime Hecke eigenvalue equation are written explicitly. The prime Hecke operator includes both its translated sum and its second term; when the prime divides the level, the second term vanishes. The complex twist is the finite-translate expression for $f_{\chi^{-1}}$, and its critical L-value is defined by the actual Mellin integral. Neither an arbitrary L-value table nor the desired measure is an input assumption.
The embeddings share the abstract algebraic closure of $\mathbb Q$; there is no asserted continuous map from $\mathbb C$ to $\mathbb C_p$. The algebraic bridge in each interpolation identity is existential and constrained by a complex equality. Test functions are existential continuous maps constrained pointwise to equal the specified character or disk function; this makes their continuity part of the conclusion instead of an unproved definition. All primes, including $2$, are allowed. Natural-number subtractions occur only in theorem contexts with $k\ge2$ and $j\le k-2$.
The signed projections use a factor of $1/2$. Their normalized measures are added, and the period sign is $\chi(-1)(-1)^j$. These conventions fix the powers, sign, Gauss sum, and periods in the displayed interpolation formula. Periods are not asserted to be canonical integral periods; rescaling by algebraic constants changes the normalization. Exceptional-zero derivative formulas, positive-slope distributions, tame-conductor twists, and Iwasawa main conjectures are outside this mission.
## Selected references
- B. Mazur, J. Tate and J. Teitelbaum, *On p-adic analogues of the conjectures of Birch and Swinnerton-Dyer*, Inventiones Mathematicae 84 (1986), 1–48, Chapter I, §§1–4 and 7–14. [DOI](https://doi.org/10.1007/BF01388731); [digitized original](https://gdz.sub.uni-goettingen.de/download/pdf/PPN356556735_0084/LOG_0007.pdf).
- G. Shimura, *On the periods of modular forms*, Mathematische Annalen 229 (1977), 211–221. [DOI](https://doi.org/10.1007/BF01391466).
- C. Williams, *An introduction to p-adic L-functions II: Modular forms*, lecture notes, §§11.6–11.8, particularly Proposition 11.21, for period normalization of general eigenforms. [Author's notes](https://warwick.ac.uk/fac/sci/maths/people/staff/cwilliams/lecturenotes/lecture_notes_part_ii.pdf).
## Motivation
Discrepancy theory asks how evenly a collection of objects can be split into two parts. Its central open question is a conjecture of Komlós, first circulated in the 1980s: any finite family of vectors of Euclidean length at most one can be signed $\pm 1$ so that the signed sum is bounded in every coordinate by a universal constant — independent of how many vectors there are and of the dimension they live in.
## Timeline
- **1963.** Steinitz-type vector balancing questions circulate; Bárány and Grinberg later (1981) show *any* norm admits a dimension-dependent bound $2d$, setting the theme: how much of the dependence on dimension is real?
- **1981.** Beck and Fiala ([Discrete Appl. Math.](https://doi.org/10.1016/0166-218X(81)90022-6)) prove degree-$t$ set systems have discrepancy at most $2t - 1$, by the floating-colors argument, and conjecture $O(\sqrt{t})$.
- **1980s.** Komlós poses the vector form — unit $\ell^2$-norm columns, constant $\ell^\infty$ discrepancy — which implies the Beck–Fiala conjecture; it circulates through Spencer's *Ten Lectures* (1987) as the central open problem of the area.
- **1985.** Spencer ([Trans. AMS](https://doi.org/10.1090/S0002-9947-1985-0784009-0)) proves "six standard deviations suffice": discrepancy $6\sqrt{n}$ for $n$ sets on $n$ points, beating random signing via the partial-coloring method.
- **1998.** Banaszczyk ([Random Struct. Algorithms](https://doi.org/10.1002/(SICI)1098-2418(199810)12:4%3C351::AID-RSA3%3E3.0.CO;2-S)) proves the Komlós bound $O(\sqrt{\log n})$ by a recursive Gaussian-measure argument over convex bodies.
- **2010–2016.** The constructive era: Bansal (2010) makes Spencer algorithmic by SDP random walks, Lovett and Meka (2012) simplify, and Bansal, Dadush, and Garg ([STOC 2016](https://arxiv.org/abs/1605.02882)) give a polynomial-time algorithm matching Banaszczyk's bound.
- **2023.** Kunisky ([SIAM J. Discrete Math.](https://arxiv.org/abs/2111.02974)) constructs instances from unsatisfiable formulas with discrepancy approaching $1+\sqrt{2}$ — the strongest lower bound on the conjectured constant.
- **2025.** Bansal and Jiang ([arXiv:2508.03961](https://arxiv.org/abs/2508.03961)) break the Banaszczyk barrier: $\tilde{O}((\log n)^{1/4})$ for Komlós, and the Beck–Fiala conjecture resolved for $t \ge \log^2 n$ — the first movement in nearly thirty years. The gap between $2.414\ldots$ and $\tilde{O}((\log n)^{1/4})$ is the conjecture.
## Setting
Fix $n$ vectors $v_1, \dots, v_n \in \mathbb{R}^m$ with Euclidean norm $\lVert v_i \rVert_2 \le 1$. A **sign vector** is an $\varepsilon \in \{-1, +1\}^n$: one sign $\varepsilon_i \in \{\pm 1\}$ per vector. Writing $v_{ij}$ for the $j$-th coordinate of the vector $v_i$, the **discrepancy** of the family under $\varepsilon$ is the largest coordinate, in absolute value, of the signed sum $\sum_i \varepsilon_i v_i$ — that is, $\max_{j \le m} \lvert \sum_{i \le n} \varepsilon_i v_{ij} \rvert$, the $\ell^\infty$ norm of the signed sum. The **Komlós property at constant $K$** — `KomlosBound K` — says that *every* such family, in every $n$ and every $m$, admits a sign vector with every coordinate of the signed sum at most $K$ in absolute value.
Set systems embed as the special case of $0/1$-incidence matrices: if $A$ is an $m \times n$ matrix of $0$s and $1$s in which every column has at most $t$ ones (every element lies in at most $t$ sets), the columns scaled by $1/\sqrt{t}$ have norm at most one, so the Komlós property gives discrepancy $K\sqrt{t}$ — the Beck–Fiala conjecture.
## Formalization targets
### Goal — the Komlós conjecture
$$\exists\, K \in \mathbb{R}: \quad \text{every } v_1, \dots, v_n \in \mathbb{R}^m \text{ with } \lVert v_i\rVert_2 \le 1 \text{ admits } \varepsilon \in \{\pm 1\}^n \text{ with } \max_j \Big|\sum_i \varepsilon_i v_{ij}\Big| \le K.$$
The goal fixes no value of $K$: any finite universal constant settles it, so the statement survives every improvement in the constant.
### Milestones — the known ladder
Eight results over the same definitions: Beck–Fiala's $2t - 1$ for degree-$t$ set systems; Spencer's $6\sqrt{n}$ for $n$ sets on $n$ points; Banaszczyk's $O(\sqrt{\log n})$ for the Komlós setting; its corollary $O(\sqrt{t \log n})$ for set systems; the reduction "Komlós at $K$ implies Beck–Fiala at $K\sqrt{t}$"; Kunisky's lower bound $K \ge 1 + \sqrt{2}$; and the two 2025 Bansal–Jiang breakthroughs — $\tilde{O}((\log n)^{1/4})$ for the Komlós setting, and the Beck–Fiala conjecture's bound $O(\sqrt{t})$ in the regime $t = \Omega(\log^2 n)$.
## Significance
The conjecture is the meeting point of the two main techniques of discrepancy theory — partial coloring and the Gaussian/convex-geometric method — and each further improvement has forced a new technique into existence. A proof would resolve the Beck–Fiala conjecture in full and sharpen the hereditary-discrepancy landscape; a disproof would break the widely-shared expectation that vector balancing is dimension-free. The problem is also a benchmark for algorithmic discrepancy: every known bound now has a polynomial-time counterpart, and the constructive tools built for it (random-walk roundings, spectral partial colorings) are used across approximation algorithms and ranging into differential privacy.
None of this literature is formalized anywhere; Mathlib has no discrepancy theory at all. The definitions here are elementary — finite sums, absolute values, one norm hypothesis — so the mission's entry cost is unusually low for an open-problem mission: the Beck–Fiala theorem and the scaling reduction are self-contained finite combinatorics, while Spencer and Banaszczyk each force a genuinely new proof technique (pigeonhole partial coloring; Gaussian measure on convex bodies) into Lean.
## Difficulty
Random signs lose: they give $\Theta(\sqrt{n})$, not a constant, so the naive probabilistic argument is ruled out from the start. The Beck–Fiala argument caps discrepancy by degree, not by norm, and provably cannot be pushed below $2t - O(1)$ by its own bookkeeping. Partial coloring alone loses a logarithm through its iteration, and Banaszczyk's method is blocked at $\sqrt{\log n}$ by the Gaussian measure of the cube. The 2025 advance decouples the two methods but still pays iterated polylogarithmic factors. Nothing currently known contracts the remaining gap to a constant, and the lower bound says the constant, if it exists, is at least $1 + \sqrt{2}$ — so any proof must handle instances strictly harder than the set-system case.
## Formalization scope
The Lean model commits to: vectors as `EuclideanSpace ℝ (Fin m)`, whose norm is the $\ell^2$ norm (the hypothesis $\lVert v_i \rVert \le 1$ reads `‖v i‖ ≤ 1`); the $\ell^\infty$ conclusion written coordinatewise as `∀ j, |∑ i, ε i * v i j| ≤ K`, avoiding any auxiliary sup-norm structure; sign vectors as real vectors with `ε i = 1 ∨ ε i = -1`; and set systems as matrices `A : Fin m → Fin n → ℝ` with an entrywise $0/1$ hypothesis and column-degree counted by `Set.ncard`. Quantifier order matters everywhere: in `KomlosBound K` the constant is fixed *before* $n$ and $m$ — a $K$ depending on $n$ would make the statement the trivial $\sqrt{n}$ bound. In `beck_fiala` the hypothesis $t \ge 1$ is required (the degree-$0$ system has discrepancy $0 > 2t-1$ otherwise); the Banaszczyk-form bounds use $\log(n+2)$ so that the bound is positive already at $n \le 1$. In the Bansal–Jiang milestones the asymptotic $\tilde{O}$ and $\Omega$ are rendered by existential constants quantified before all instances: the hidden $\mathrm{poly}(\log\log n)$ factor becomes $(\log\log(n+8))^{\gamma}$ for some fixed $\gamma > 0$ (the inner shift $+8$ keeps the iterated logarithm positive), and the threshold $t = \Omega(\log^2 n)$ becomes $C_0 \log^2(n+2) \le t$ for some fixed $C_0 > 0$.
Welcome contributions: any milestone in any order — `beck_fiala` and `komlos_implies_beck_fiala` are self-contained finite arguments and the natural entry points; `spencer_six_deviations` and `banaszczyk_bound` each import a major technique; `komlos_lower_bound` needs an explicit construction and a case analysis over all sign vectors. Reusable infrastructure — partial colorings, Gaussian measure bounds for convex bodies, hereditary discrepancy — is welcome as platform theorems. The matrix Spencer conjecture, prefix discrepancy, and the Steinitz problem are related but deliberately left to future missions.
## Selected references
- J. Beck, T. Fiala, *"Integer-making" theorems*, Discrete Applied Mathematics 3 (1981). [doi:10.1016/0166-218X(81)90022-6](https://doi.org/10.1016/0166-218X(81)90022-6)
- J. Spencer, *Six standard deviations suffice*, Trans. Amer. Math. Soc. 289 (1985). [doi:10.1090/S0002-9947-1985-0784009-0](https://doi.org/10.1090/S0002-9947-1985-0784009-0)
- W. Banaszczyk, *Balancing vectors and Gaussian measures of n-dimensional convex bodies*, Random Structures & Algorithms 12 (1998). [doi link](https://doi.org/10.1002/(SICI)1098-2418(199810)12:4%3C351::AID-RSA3%3E3.0.CO;2-S)
- N. Bansal, D. Dadush, S. Garg, *An algorithm for Komlós conjecture matching Banaszczyk's bound*, FOCS 2016 / SIAM J. Comput. [arXiv:1605.02882](https://arxiv.org/abs/1605.02882)
- N. Bansal, H. Jiang, *Decoupling via affine spectral-independence: Beck–Fiala and Komlós bounds beyond Banaszczyk*, 2025. [arXiv:2508.03961](https://arxiv.org/abs/2508.03961)
- D. Kunisky, *The discrepancy of unsatisfiable matrices and a lower bound for the Komlós conjecture constant*, SIAM J. Discrete Math. 37 (2023). [arXiv:2111.02974](https://arxiv.org/abs/2111.02974)
- B. Chazelle, *The Discrepancy Method*, Cambridge University Press, 2000. [author's page](https://www.cs.princeton.edu/~chazelle/pubs/book.pdf)
Existence of complete sets of mutually unbiased basesOpen Problem
# Motivation
Two orthonormal bases of C^d are mutually unbiased when every transition amplitude has squared modulus 1/d. At most d+1 such bases can coexist, and complete families are known in prime-power dimensions through finite-field constructions. Dimension six is the smallest famous composite case where existence of the complete seven-base family remains unknown.
This mission turns CUHK-Shenzhen AI Math Problem 16, **Existence of complete sets of mutually unbiased bases**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
Construct seven 6 by 6 unitary-column matrices whose every distinct pair has all transition amplitudes of squared modulus 1/6. The baseline milestone constructs three pairwise mutually unbiased bases, a known lower bound that tests all matrix conventions.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in quantum information theory, mutually unbiased bases, finite fields, Hilbert spaces. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
The equations are a large coupled system of polynomial equalities over complex phases, modulo substantial gauge symmetry. Numerical near-solutions do not certify exact existence, while nonexistence would require a global obstruction beyond currently known bounds. Dimension six lacks the finite-field structure that supplies complete prime-power constructions.
## Suggested attack route
Formalize standard gauge reductions: fix the first basis to the identity and dephase transition Hadamard matrices. Verify a three-basis tensor-product construction. Then encode additional bases through complex Hadamard matrices and study algebraic constraints, Gröbner-style eliminations, semidefinite bounds, or exact certificates. Computational searches may guide conjectures, but uploaded proofs must convert numerical evidence to exact algebraic identities or certified inequalities.
## Formalization scope
The Lean target is exact: column orthonormality is U-adjoint times U equals identity, and mutual unbiasedness uses Mathlib complex norm squared. Seven bases are indexed by Fin 7. No quotient by phase, permutation, or global unitary is built into the statement, since these symmetries preserve the predicate and can be used within proofs.
The natural-language source remains authoritative for motivation, while the Lean declaration is authoritative for what Prove2Me will verify. The mission description calls out restrictions where the current formal target is a finite-dimensional core, a fixed interpretation of informal terminology, or one sharpened subquestion from a broader classification problem. Those restrictions should not be silently generalized in a proof claim.
## Milestones
Publish an exact three-basis construction in dimension six, then formalize dephasing and obstruction lemmas for extending a partial family.
The capstone is marked as the mission's main item and is never duplicated as a milestone. Definitions precede theorem statements in the proposal order. A milestone is considered complete only when its own exact statement is proved; proving a nearby theorem with stronger-looking prose but mismatched quantifiers, signs, supports, dimensions, or asymptotic constants does not complete it.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original problem](https://rybindmitry.github.io/problems/16.html)
- [Durt et al., review of MUBs](https://arxiv.org/abs/1004.3348)
First-passage time of Brownian motion to an exponentially decaying boundaryOpen Problem
> **Submission hold — source-fidelity repair (2026-09-04).** The public goal restricts answers to elementary expression trees and is only a stronger subquestion. It does not formalize the source's broader special-function closed-form question. The existing published target is preserved, with this scope warning. Do not confirm or submit this version as a faithful formalization of the full source. The legacy mathematical target below is retained for traceability while the replacement is prepared.
# Motivation
A standard Brownian motion starts below the exponentially decaying boundary b(t)=b0 exp(-ct). The first time it crosses the boundary has a continuous density characterized by a generalized Abel--Volterra integral equation. The source asks for an explicit distribution, motivated in part by neuronal threshold models with a decaying refractory boundary.
This mission turns CUHK-Shenzhen AI Math Problem 13, **First-passage time of Brownian motion to an exponentially decaying boundary**, into an auditable Lean campaign. The objective is not merely to transcribe notation: it is to expose the mathematical model, the capstone, and a smaller attack surface as separate artifacts that other formalizers can inspect and reuse.
## Setting
Construct one expression in a fixed elementary language whose evaluation is a continuous nonnegative density on positive times, solves the Abel equation, and integrates to one. The language contains real constants, rational constants, arithmetic, exp, log, square root, trigonometric functions, and the normal density. The first milestone drops elementary representability and normalization and asks for a continuous nonnegative Abel solution.
## Significance
Solving this target would settle the precise finite or analytic core represented by the Lean statement and would create reusable infrastructure in Brownian motion, first-passage times, stochastic processes, Volterra integral equations. Even a rigorous disproof is valuable: several entries in this collection deliberately ask whether an attractive extrapolation is true, and Lean forces a counterexample to satisfy every side condition. The mission therefore treats theorem proving and model criticism as equally legitimate research outcomes.
## Difficulty
Moving-boundary first-passage laws rarely have elementary closed forms. The Abel kernel is singular at the upper endpoint, and showing that a candidate equation solution is the actual passage density requires uniqueness and probability normalization. The capstone may be false under the selected expression language; a non-elementarity theorem would be a legitimate disproof of this precise formal target.
## Suggested attack route
Formalize existence and uniqueness for the Volterra equation using weakly singular kernels, then connect it to Brownian first passage. Explore transformations suggested by the exponential boundary, Laplace transforms, and iterative resolvent kernels. Symbolic or numerical calculations may reveal special-function rather than elementary structure. If so, characterize the required extension of the expression language and prove why the current language is insufficient.
## Formalization scope
The already-published goal uses finite elementary-expression trees with arithmetic, exp/log/sqrt, sin/cos and normal density. The source explicitly permits standard special functions beyond this language. Accordingly the published declaration is a stronger elementary-only subquestion, not a faithful replacement for the full closed-form question. It is preserved as an existing result; its proof or disproof must not be reported as settling every special-function formula. The Abel-solution milestone asserts only existence of a continuous nonnegative solution; uniqueness, normalization, and identification with the first-passage density remain separate obligations. A complete source-faithful replacement needs an agreed formula class or a concrete proposed formula, not an unrestricted function renamed a closed form.
## Milestones
For each positive boundary height and decay parameter, there exists a continuous nonnegative solution of the stated Abel equation on positive times. This node asserts existence only, not uniqueness, unit mass, or an elementary closed form.
## Timeline and literature status
The CUHK-Shenzhen AI Math Problems page added this problem on June 23, 2026. At the drafting date, August 31, 2026, the status and target corrections described above were checked against the source page and the cited primary material.
## Acceptance criteria
A contribution may prove the displayed theorem or refute it by constructing data satisfying every Lean hypothesis while negating the conclusion. Informal changes of model do not count: any proposed correction must be submitted as a separately reviewed statement with an explanation of which source ambiguity or false implication it repairs. Definitions must remain computational or mathematically constrained; fields that simply assume the desired conclusion are not acceptable. Every proof must compile against the mission's pinned Mathlib revision, use no `sorry`, and expose a top-level `theorem solution` when submitted to Prove2Me.
The main theorem is intentionally separated from a smaller milestone. Contributors should preserve that dependency order, publish reusable lemmas rather than monolithic tactics, and report whether a lemma is analytic, algebraic, combinatorial, or infrastructure-only. Numerical evidence, external computer algebra, and exhaustive search are welcome for discovery, but a final certificate must be replayable by Lean. If an external result is invoked, its hypotheses must be represented in the formal statement or proved in the dependency tree.
## Formal verification policy
The files were built locally with Lean 4.30.0 and Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, the supported Prove2Me environment at drafting time. The mission definition file is ordered before all theorem files, and each theorem imports exactly that public definition module or Mathlib. Independent blind read-backs accompany the draft items so reviewers can compare what the Lean code literally says with this mathematical description. Human confirmation remains required before the public proposal can be submitted for moderation.
## Selected references
- [Original CUHK-Shenzhen problem](https://rybindmitry.github.io/problems/13.html)
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.
Quadratic forms and Sobolev spaces of fractional orderResearch Paper
## Motivation
Nonlocal operators — generators of jump processes, fractional Laplacians, and the
Dirichlet forms attached to them — are studied through the quadratic form they define
rather than through the operator itself. For the fractional Laplacian $(-\Delta)^{\alpha/2}$
that form is the **Gagliardo seminorm**, and the natural function space is the fractional
Sobolev space $H^{\alpha/2}$. A recurring question is how far the kernel may degenerate
before the associated form stops being comparable to the Gagliardo seminorm — that is,
before the form's natural domain stops being $H^{\alpha/2}$.
Bux, Kassmann and Schulze, *Quadratic forms and Sobolev spaces of fractional order*
([arXiv:1707.09277](https://arxiv.org/abs/1707.09277), Proc. Roy. Soc. Edinburgh 2020),
give a strikingly permissive answer: the kernel may vanish outside a **double cone** at
every point, and the cone's axis may vary arbitrarily from point to point, provided its
opening angle stays bounded below. Earlier results in this direction assumed the jump
directions were comparable to a fixed set; the point here is that no such uniformity is
needed.
## Setting
Fix $d \ge 1$. A **double cone** $V(v,\vartheta) \subseteq \mathbb{R}^d$ is determined by a
unit **axis** $v$ and an **apex angle** $\vartheta \in (0, \pi/2]$: it is the set of
non-zero $h$ whose angle to the line $\mathbb{R}v$ is less than $\vartheta$. It is
symmetric, $h \in V \iff -h \in V$, and never contains the origin.
A **configuration** $\Gamma$ assigns a double cone $\Gamma(x)$ to every point
$x \in \mathbb{R}^d$; write $V^\Gamma[x] = x + \Gamma(x)$ for that cone translated to $x$.
The configuration is **$\vartheta$-bounded** when every apex angle is at least $\vartheta$.
No continuity, and no relation between the axes at different points, is assumed.
For a measurable $\Omega \subseteq \mathbb{R}^d$, a symmetric kernel
$k : \mathbb{R}^d \times \mathbb{R}^d \to [0,\infty]$ and $f : \mathbb{R}^d \to \mathbb{R}$, put
$$\mathcal{E}_\Omega[k,f] \;=\; \int_\Omega\!\!\int_\Omega (f(y)-f(x))^2\,k(x,y)\,dy\,dx,
\qquad
|f|^2_{H^{\alpha/2}(\Omega)} \;=\; \mathcal{E}_\Omega\!\left[\,\|x-y\|^{-d-\alpha},\,f\,\right].$$
The kernels of interest satisfy the two-sided bound
$$\Lambda^{-1}\,\frac{\mathbf 1_{V^\Gamma[x]}(y) + \mathbf 1_{V^\Gamma[y]}(x)}{\|x-y\|^{d+\alpha}}
\;\le\; k(x,y) \;\le\; \frac{\Lambda}{\|x-y\|^{d+\alpha}},$$
so $k$ is allowed to vanish entirely off the cones, and is bounded above by the
$\alpha$-stable kernel.
## Formalization targets
### Goal — Theorem 1.1
For all $\vartheta > 0$, $\Lambda \ge 1$ and $\alpha \in (0,2)$ there is $c \ge 1$,
depending on those and $d$ alone, such that for every $\vartheta$-admissible $\Gamma$,
every $k$ obeying the bounds above, every ball $B = B(x_0,R)$ and every $f \in L^2(B)$,
$$|f|^2_{H^{\alpha/2}(B)} \;\le\; c\,\mathcal{E}_{B}[k,f].$$
Both forms are over the **same** ball; there is no enlargement on the right. The reverse
inequality is immediate from the upper bound on $k$, so this direction carries the content.
The uniformity is the claim: $c$ does not depend on $\Gamma$, on $k$, on the centre, on the
radius, or on $f$.
### The discrete counterpart — Theorem 1.3
The same comparison on $\mathbb{Z}^d \cap B$, with sums over lattice pairs separated by more
than $R_0$ and an enlargement $B \to \kappa B$ on the right. This is the combinatorial heart
and is **fully proved** in this development.
## Significance
Comparability identifies the form's domain: it gives $H_k(\Omega) = H^{\alpha/2}(\Omega)$
with equivalent seminorms, so the whole $H^{\alpha/2}$ toolkit — embeddings, trace and
extension theorems, compactness — transfers to operators whose jumps are confined to
wildly varying cones. Without it, each such operator's domain must be analysed separately.
What this mission adds on top of the paper is a machine-checked account of exactly which
parts are established. That distinction is not cosmetic here. The discrete theorem
(Theorem 1.3) and its supporting chain — the continuum connectivity theorem 4.1, the
renormalization of §5, the path-assembly of Theorem 5.15 — are proved, sorry-free, and are
uploaded as this mission's supporting graph. The continuous Theorem 1.1 is **not**: §3.2's
passage to the limit needs a finiteness hypothesis the paper does not state, and Lemma A.1's
step from a ball to a bounded Lipschitz domain quotes a Whitney decomposition and Dyda's
inequality rather than proving them.
Three concrete corrections came out of the formalization and have been reported to the
authors: the apex-shrinking constant of Lemma 5.9 must be $(\sqrt d + 1)/\sin(\vartheta/2)$
rather than the paper's $3\sqrt d/(2\sin\vartheta)$, which is too small; the thin-cone lemma
3.3 is false as stated in dimension one, at the radius $r=\sqrt d$ at which Proposition 3.5
invokes it — the counterexample is `QFS.lemma_new_config_false_dim_one`, uploaded with this
mission; and the paper's tiles are half-closed where the
text reads as closed.
## Difficulty
The obvious approach to the continuous theorem is to prove it on a lattice and pass to the
limit, and that is the paper's approach. The difficulty is that the cone directions are
uncontrolled: two nearby points may admit no common jump direction at all, so a "straight"
path between them need not exist, and the chain of jumps that does exist may be long. The
combinatorial content is that a bounded number of cone types can be routed around this,
which is what the renormalization and path-assembly machinery delivers in the discrete
setting.
What remains open is the transfer of that control to the continuum without an a priori
finiteness assumption. In the plane the obstruction disappears — two double cones of
positive aperture in $\mathbb{R}^2$ always overlap after one intersection — and Theorem 1.1
is proved here unconditionally for $d = 2$. In every dimension it is proved for cones of
apex angle exceeding $\pi/4$, for configurations whose axes have angular spread below
$2\vartheta$, for pairwise overlapping families of cone types, and for locally dominated
configurations. The general case reduces to a single integrability condition against an
explicit measurable domination radius, and that reduction is the mission's frontier.
## Formalization scope
Both forms are **lower Lebesgue integrals valued in $[0,\infty]$**, so they are defined
without assuming the integrand measurable, and no statement asserts either side is finite:
where the right-hand side is infinite the inequality is automatic. Sums over lattice pairs
are over **ordered** pairs, so each unordered pair contributes twice.
Two measurability conditions appear and are not interchangeable. `CondM` is the paper's
condition (M): measurability of $\{(x,y) : y - x \in \Gamma(x)\}$. `CondMeas` is the
strictly stronger statement that $\{x : V \subseteq \Gamma(x)\}$ is measurable for **every**
subset $V$ — the conclusion the paper draws from (M) via Debreu's theorem, carried here as
an explicit hypothesis. Results are stated under whichever they actually use.
A trivializing reading is ruled out: since every double cone carries apex angle at most
$\pi/2$, no configuration is $\vartheta$-bounded for $\vartheta > \pi/2$, so the content
lies in $0 < \vartheta \le \pi/2$, matching the paper's parameter space
$\mathcal{V} = (0,\pi/2] \times \mathbb{P}^{d-1}_{\mathbb{R}}$.
The development is Lean 4 / Mathlib. Contributions closing the frontier milestone, or
replacing the two quoted inputs of Lemma A.1 with proofs, are the most valuable; the cone
geometry, the lattice-counting lemmas and the Vitali-type covering arguments are reusable
beyond this mission.
## Selected references
- K.-U. Bux, M. Kassmann, T. Schulze, *Quadratic forms and Sobolev spaces of fractional
order*, Proc. Roy. Soc. Edinburgh Sect. A 150 (2020), 1–27.
[arXiv:1707.09277](https://arxiv.org/abs/1707.09277)
- E. Di Nezza, G. Palatucci, E. Valdinoci, *Hitchhiker's guide to the fractional Sobolev
spaces*, Bull. Sci. Math. 136 (2012), 521–573.
[arXiv:1104.4345](https://arxiv.org/abs/1104.4345)
- B. Dyda, *A fractional order Hardy inequality*, Illinois J. Math. 48 (2004), 575–588.
[doi:10.1215/ijm/1258138400](https://doi.org/10.1215/ijm/1258138400)
Smooth 4-dimensional Poincaré conjecture: foundations and reductionsOpen Problem
## Motivation
The **smooth four-dimensional Poincaré conjecture** asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of *K3 — A New Problem List in Low-Dimensional Topology*. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. [Baykur–Kirby–Ruberman, Problem 4.1](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf)
### Historical landmarks
- **1961:** Smale proved that a closed smooth manifold homotopy equivalent to a sphere of dimension at least five is homeomorphic to that sphere. This is not a theorem that all such smooth manifolds are diffeomorphic to the standard sphere. [Smale, Theorem A](https://www.math.uchicago.edu/~shmuel/tom-readings/Smale,%20PC.pdf)
- **1982:** Freedman established the topological four-dimensional Poincaré theorem: a topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to it. [Freedman, Theorem 1.6](https://www.maths.gla.ac.uk/~mpowell/1982_The%20topology%20of%20four-dimensional%20manifolds.pdf)
- **2026:** The *K3* problem list continues to distinguish this established topological result from the open smooth sphere problem. [Problem 4.1, pp. 191–192](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf)
## Setting
Let $S^4$ be the unit sphere in $ℝ^5$, with its standard stereographic smooth structure. A **homeomorphism** is a continuous bijection with continuous inverse; a **diffeomorphism** is a smooth bijection with smooth inverse. A **smooth atlas** is a collection of local Euclidean coordinates whose transition maps are smooth.
The manifold $M$ is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on $ℝ^4$. The given atlas is arbitrary: it is not defined by transporting the standard structure from $S^4$.
For a homeomorphism $e:N\to S^4$, let $\mathcal A_e$ denote the atlas transported from the standard sphere along $e$. A **structomorphism** for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate $\mathsf{SPC4Pullback}$ requires, for every given smooth atlas $\mathcal A$ on such an $N$ and every such $e$, a structomorphism between $(N,\mathcal A)$ and $(N,\mathcal A_e)$. It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, *SPC4.lean*, lines 53–81 and 211–221]
## Formalization targets
### Main open goal
For every manifold $M$ with the preceding hypotheses, the goal is
$$
M\cong_{\mathrm{Top}}S^4
\quad\Longrightarrow\quad
M\cong_{\mathrm{Diff}}S^4.
$$
This is the source predicate $\mathsf{SPC4}$. Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.
### Structural and literature milestones
The atlas formulation has the exact equivalence
$$
\mathsf{SPC4}\quad\Longleftrightarrow\quad\mathsf{SPC4Pullback}.
$$
The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence
$$
\operatorname{Structomorph}(\mathcal G^{\infty},M,N)
\simeq \operatorname{Diff}^{\infty}(M,N),
$$
where $\mathcal G^{\infty}$ is the smooth coordinate-change groupoid for the common model. [Shin, *SPC4.lean*, lines 334–365; *Bridge.lean*]
Write $F_4$ for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:
$$
M\simeq S^4\quad\Longrightarrow\quad M\cong_{\mathrm{Top}}S^4,
$$
where $\simeq$ denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If $\mathsf{SPC4Homotopy}$ denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:
$$
F_4\quad\Longrightarrow\quad
(\mathsf{SPC4}\Longleftrightarrow\mathsf{SPC4Homotopy}).
$$
Explicit standard-disk foundations form another track. For every $m\geq0$, they concern the manifold-with-boundary structure on $\overline B^{m+1}$, its boundary set $S^m$, and the smooth collar
$$
c:S^m\times[0,1]\longrightarrow\overline B^{m+1},
\qquad c(u,t)=(1-t/2)u.
$$
The collar is a closed embedding, has image
$$
\{z\in\overline B^{m+1}:\|z\|\geq1/2\},
$$
and satisfies $c(u,0)=u$, using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a $C^k$ map from a $C^k$ manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is $C^k$. These targets concern the actual disk smooth structure. [Shin, *Disk.lean*, lines 1076–1141 and 1263–1318]
## Significance
A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.
The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and the topological theorem remains unproved in this formal development despite its published mathematical proof.
Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by [wamlart](https://prove2.me/users/70d2064f-6b47-4a3f-bb90-74e71a55cbb7): [orbit augmentation](https://prove2.me/theorems/85478003-b7db-44ef-be81-1c0fc5d7a8b4), [region homology budgets](https://prove2.me/theorems/e3d78c98-ef71-4b2a-a04a-7fd93fe9246f), [two-corner homology budgets](https://prove2.me/theorems/f6cc0221-29eb-4e8a-9649-8856b2954f2a), [the Laurent mass threshold](https://prove2.me/theorems/2d22450e-c4ce-4a0c-8829-b51d65e80eb5), and [mass-two positivity](https://prove2.me/theorems/988bc029-7a8a-43d7-9413-9e9cc3f86c24). No theorem currently connects their completion to a proof or disproof of $\mathsf{SPC4}$. They are exploratory tools, not established milestones in a proof of the main goal.
## Difficulty
A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.
Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a gluing theorem, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.
## Formalization scope
The sphere goal quantifies over `Type` in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order $\infty$. Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.
The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every $m\geq0$, so their dimensions are $m+1\geq1$. The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.
The separate source assertion `SPC4Ball` is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product construction is deferred, not a current target. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.
## Selected references
- R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., *K3 — A New Problem List in Low-Dimensional Topology*, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. [Author PDF](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf).
- Michael Hartley Freedman, *The topology of four-dimensional manifolds*, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. [DOI](https://doi.org/10.4310/jdg/1214437136); [primary-article scan](https://www.maths.gla.ac.uk/~mpowell/1982_The%20topology%20of%20four-dimensional%20manifolds.pdf).
- Stephen Smale, *Generalized Poincaré's Conjecture in Dimensions Greater Than Four*, Annals of Mathematics 74 (1961), 391–406, Theorem A. [DOI](https://doi.org/10.2307/1970239); [primary-article scan](https://www.math.uchicago.edu/~shmuel/tom-readings/Smale,%20PC.pdf).
- Ryan Shin, *SPC4.lean*, *Bridge.lean* and *Disk.lean*, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: `b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc`, `e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302`, `889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e`.
Strong Whitney embedding in dimension 2nResearch Paper
## Motivation: an intrinsic manifold in a fixed Euclidean space
A **smooth manifold** is a space that can be described locally by real coordinates, even when no single coordinate chart describes the whole space. Differential geometry works with these local descriptions, whereas an embedding realizes the entire space inside one Euclidean space without losing either its topology or its infinitesimal geometry. The **strong Whitney embedding theorem** supplies a dimension bound depending only on the dimension of the manifold. This mission targets the precise version selected by [LeanEval v1](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean), rather than a substitute formulation.
The benchmark attributes the strong result to Hassler Whitney's 1944 paper and distinguishes it from the earlier bound of $2n+1$. The result is a known mathematical theorem; the remaining task here is its formal proof in Lean. The exact benchmark declaration is authoritative for the target and its hypotheses, not a reconstruction from the historical literature ([source and attribution](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/whitney_embedding.toml)).
## Setting: topology, smoothness, and the differential
Let $n$ be a natural number satisfying $1\le n$. Let $M$ carry a topology and a smooth atlas modeled on $\mathbb R^n$, with the usual model having no boundary. The topology is **Hausdorff**: distinct points admit disjoint neighborhoods. It is **second countable**: there is a countable collection of open sets from which every open set can be assembled as a union. These are explicit hypotheses, alongside the chosen charted-space and smooth-manifold structures, in the [Lean statement](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
A **topological embedding** is a map that is a homeomorphism onto its image, where the image has the subspace topology inherited from the codomain. An **immersion** has an injective differential at every point. For a smooth map $e$, write $d e_x$ for the induced linear map on tangent spaces at $x$. These are separate requirements: the target asks for global topological embedding and pointwise injectivity of the differential together, as well as infinite differentiability. Their precise Lean meanings are the existing Mathlib predicates used directly by the benchmark, not new mission-specific definitions.
## Formalization target: the single root theorem
For every $n\ge1$ and every $M$ with the structures and hypotheses just stated, establish
$$
\exists e:M\longrightarrow\mathbb R^{2n},\qquad
e\in C^\infty(M,\mathbb R^{2n})
\ \land\ e\text{ is a topological embedding}
\ \land\ \forall x\in M,\ d e_x\text{ is injective}.
$$
The codomain has dimension exactly $2n$. The quantifier ranges over all such manifolds, including noncompact ones. There is exactly one goal theorem and no auxiliary theorem items, definition items, or milestones. The declaration is `LeanEval.Geometry.WhitneyEmbeddingProblem.whitney_embedding`, with the binders and conclusion preserved from the [benchmark source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
## Significance: the full theorem rather than an easier restriction
The result realizes the given manifold in a Euclidean space with a uniform dimension bound. Its value in this formulation is the simultaneous control of topology, smoothness, and the differential, without a compactness assumption. Replacing the image-topology condition with mere injectivity would omit part of the requested conclusion; replacing $2n$ with an unspecified dimension would omit the quantitative constraint. Both distinctions are explicit in the [benchmark's explanation](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean).
A completed formalization would supply a reusable strong embedding theorem on top of Mathlib's manifold language. This is a long-term infrastructure task, not a claim that a short proof is available. The September 5, 2026 LeanEval v1 snapshot supplied for this task records no accepted benchmark credit for this target. That dated benchmark status is not a claim about all formalization projects, and preparing an open theorem statement does not establish the theorem or earn benchmark credit.
## Difficulty: the dimension bound and the noncompact scope
The existing compact embedding result discussed by the benchmark provides an embedding into some finite-dimensional Euclidean space. That does not settle the present goal: it assumes compactness and does not supply the $2n$ bound. Consequently, simply invoking that result cannot discharge the unrestricted benchmark statement. The source identifies substantial differential-topological infrastructure behind the strong theorem; this proposal does not advertise an easy proof or prescribe a decomposition ([benchmark discussion](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean)).
All positive dimensions remain in scope, including $n=1$ and $n=2$. Noncompactness is not a later extension or optional strengthening. The absence of an assumption must not be replaced by an implicit restriction in a new definition or an easier surrogate theorem.
## Formalization scope: unchanged Mathlib predicates
The source model is `EuclideanSpace ℝ (Fin n)`, and the target is `EuclideanSpace ℝ (Fin (2 * n))`. Smoothness is expressed by `ContMDiff (𝓡 n) (𝓡 (2 * n)) ∞ e`; the other two conjuncts are `IsEmbedding e` and pointwise `Function.Injective` of `mfderiv`. The type $M$ remains universe-polymorphic. No compactness, connectedness, orientability, or nonemptiness hypothesis is added. The empty manifold is included; dimension zero is excluded. Neither properness nor closedness of the image is demanded by the conclusion ([exact declaration](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean)).
Mathlib already provides the vocabulary needed to state the goal: Euclidean spaces, charts, manifold smoothness, topological embeddings, and manifold derivatives. No custom definition item is necessary. Future proof work may develop reusable infrastructure, but this draft contains only the root theorem and intentionally imposes no supporting targets. A proof must establish that exact statement, not the compact-only, immersion-only, or weak $2n+1$ alternative.
## Selected references
- LeanEval contributors, *Whitney embedding theorem (strong form, sharp dimension 2n)*, LeanEval v1 source declaration and manifest, statement revision 1, [pinned source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/WhitneyEmbedding.lean) and [manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/whitney_embedding.toml). These specify the exact formal target.
- H. Whitney, *The self-intersections of a smooth n-manifold in 2n-space*, Annals of Mathematics (2) **45** (1944), 220–246, [DOI](https://doi.org/10.2307/1969265). Historical attribution as recorded in the LeanEval manifest; no alternate statement from this reference replaces the benchmark goal.
## Motivation: classify three-dimensional periodic symmetry
A **space group** describes the rigid motions compatible with a periodic spatial symmetry. The classification concerns possible symmetry types, rather than the size or shape of a particular drawing of a crystal. The classical three-dimensional numbers are 230, 219 when mirror-related types are identified, and 65 for the orientation-preserving subfamily. These are the three numbers recorded in [Oliver Knill’s survey, §94, “Crystallography,” p. 41](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Keeping their conventions separate matters: changing which coordinate transformations are allowed changes what counts as the same type.
The target is the known classification result selected by **LeanEval v1**, not an unsolved classification conjecture. Its authoritative specification is [the declaration `LeanEval.Geometry.SpaceGroupsProblem.space_groups`](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The accompanying [benchmark manifest](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml) attributes the classification independently to Fedorov and Schoenflies in 1891. The work requested here is a machine-checked proof of that fixed statement.
## Setting: groups, transformations, and orientation
For a natural number $d$, let $E(d)=\mathbb R^d$ with its Euclidean inner product. A **Euclidean isometry** is an invertible affine distance-preserving transformation of this space. The objects being counted are subgroups $G$ of this full motion group. In the [benchmark’s definitions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), $G$ is **discrete** when, for every point $x$ and every real $\varepsilon>0$, the set of its elements satisfying $\operatorname{dist}(gx,x)\leq\varepsilon$ is finite.
Such a group is **crystallographic** when it also contains translations by the members of some linearly independent family of $d$ vectors. Translation by $v$ means exactly that the transformation sends every $x$ to $x+v$. These conditions specify the underlying groups directly; they do not start with a list of previously classified examples. Although the structure field containing the translation condition is called `cocompact`, its actual content is the existence of these independent translations, not a separately assumed compact quotient.
An **affine equivalence** between two groups is an invertible affine map whose conjugation carries the first group’s set of transformations onto the second’s. It need not be an isometry. An **orientation-preserving affine equivalence** additionally requires the determinant of that affine map’s linear part to be positive. Separately, an individual isometry preserves orientation when its own linear part has positive determinant. The **Sohncke subfamily** restricts the groups themselves: every element of a group must preserve orientation. This is distinct from restricting the map used to compare two groups, as explicitly distinguished by the [source definitions and notes](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean).
## Target: one conjunction, with all three exact counts
Write $C_{\mathrm{OP}}(d)$ for `crystallographicCountOP d`, $C(d)$ for `crystallographicCount d`, and $C_{\mathrm{OP,only}}(d)$ for `crystallographicCountOPOnly d`. They count, respectively, orientation-preserving affine classes of all crystallographic groups, arbitrary affine classes of all crystallographic groups, and orientation-preserving affine classes within the all-elements-orientation-preserving subfamily. The sole goal is
$$
C_{\mathrm{OP}}(3)=230\quad\land\quad C(3)=219\quad\land\quad C_{\mathrm{OP,only}}(3)=65.
$$
This is the [exact benchmark conjunction](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean), in its original order. None of its three components is optional, and they are not separate theorem targets. There are no milestones or auxiliary theorem items.
## Significance: exact cardinalities for the underlying groups
The result gives finite and exact answers for the specified spaces of symmetry types, while retaining the distinction between orientation of a coordinate change and orientation of every symmetry in a group. The difference between 230 and 219 reflects the identification of mirror-related types described in [Knill, §94](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf); the 65 count answers a different question, concerning the restricted subfamily. Neither a single count nor a list that silently merges the equivalence conventions establishes the full assertion.
The formalization would add a proof connecting these numerical claims to the actual groups and class subsets specified in Lean. The [benchmark source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) currently supplies the statement with an unproved placeholder. This draft likewise supplies a statement, not a proof or a claim that the benchmark is solved.
## Difficulty: a catalog is not a completeness theorem
A finite catalog can have 230 entries without representing every crystallographic group, and different entries can still represent the same affine class. Thus checking the length of a catalog alone does not establish the [source’s cardinality assertion](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean). The difficulty is the mathematical connection between concrete descriptions and all groups admitted by the definitions, with precisely the required equivalence relations. The restricted 65-count must also respect the condition on every group element, rather than just a label attached to an example.
## Formalization scope: preserve the benchmark model
The Lean representation is `EuclideanSpace ℝ (Fin d)`, with affine isometries and affine equivalences from Mathlib. The [three source counting functions](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean) use `Set.encard` in the extended natural numbers $\mathbb N\cup\{\infty\}$. More precisely, each counts the set of subsets obtained as the class of some admissible group; it does not count representatives with multiplicity. Consequently, the displayed finite equalities include finiteness, which is not assumed beforehand.
One reusable definition bundle contains exactly the source’s model spaces, translation and discreteness predicates, crystallographic-group subtype, orientation predicate, two conjugacy relations, and three counting functions. Their declarations are preserved, including definitions for every natural dimension; only the theorem fixes $d=3$. Definitions for group actions, affine conjugation, and these class subsets can be used independently of this particular count. Contributions must establish the fixed goal with these meanings. Replacing the groups by a hard-coded finite type, defining a count to be its desired answer, or importing an unproved classification into the definition bundle would not establish this target.
## Selected references
- LeanEval contributors; problem submitted by Kim Morrison. *LeanEval v1: 230 space groups*, statement revision 1, 2026, repository commit `296b7491ec989d21bcf8636a9a69231a1e5d1d25`. [Exact Lean source](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/LeanEval/Geometry/SpaceGroups.lean); [manifest with historical bibliography](https://github.com/leanprover/lean-eval/blob/296b7491ec989d21bcf8636a9a69231a1e5d1d25/manifests/problems/space_groups_230.toml).
- Oliver Knill. *Some Fundamental Theorems in Mathematics*, author-hosted expository survey, July 22, 2018; updated June 25, 2023. §94, “Crystallography,” p. 41. [Full text](https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). This provides background for the three counts; the exact formal conventions are those of LeanEval above.
Equality case for compressed convex functional calculusOpen Problem
## Motivation and history
Compressing an operator to a closed subspace keeps the information visible within that subspace but can discard interactions with its orthogonal complement. The **compression-rigidity question** asks whether a particular equality detects that no such interactions were present. Its inputs are two commuting positive contractions and an ordinary strictly convex function of two real variables. The issue is the equality case, not the existence of a general operator inequality for every convex function.
The question was contributed by Boris Bilich to the CUHK-Shenzhen AI Math Problems collection and added on June 1, 2026. The [original problem](https://rybindmitry.github.io/problems/2.html) asks about operators on a Hilbert space without imposing finite dimension. The first formal target in this mission treated matrices with supplied joint spectral data. That finite-dimensional declaration has a verified proof on Prove2Me, but it does not settle the unrestricted Hilbert-space question. The September 2026 correction restores arbitrary complex Hilbert spaces as the main target and preserves the earlier result as a supporting artifact.
## Setting
Let $H$ be a complete complex Hilbert space, and let $\mathcal B(H)$ be its algebra of bounded complex-linear operators. The multiplication $AB$ means composition, with $B$ acting first, and $A^*$ denotes the adjoint. A **positive contraction** $A$ is self-adjoint, satisfies $\operatorname{Re}\langle v,Av\rangle\geq0$ for every $v\in H$, and has operator norm at most one. Both zero and the identity are permitted.
Write $S=[0,1]^2$. Let $X,Y\in\mathcal B(H)$ be positive contractions satisfying $XY=YX$. Their **joint continuous functional calculus** assigns an operator $g(X,Y)$ to each continuous real function $g$ on $S$. It is characterized as a continuous unital real star-algebra homomorphism from $C(S,\mathbb R)$ to $\mathcal B(H)$ that maps the two coordinate functions to $X$ and $Y$. The domain has the uniform norm and the codomain the operator norm. The existence and uniqueness of this calculus follow from the standard joint spectral theorem; the relevant source is [Dereziński, Lemma 6.6, printed page 43](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43).
An **orthogonal projection** is an operator $P$ satisfying $P^*=P$ and $P^2=P$. The compressed operators $PXP$ and $PYP$ are still viewed as operators on the original space $H$, not as operators on a separately chosen finite-dimensional range. The question includes the additional hypothesis that these compressed operators commute. The original commutation of $X$ and $Y$ does not remove the need to state this hypothesis.
## Formalization targets
The main target is the entire compression implication from the source. Let $f:S\to\mathbb R$ be continuous and **strictly convex**: for distinct $x,y\in S$ and $0<t<1$, its value at $tx+(1-t)y$ is strictly less than $t f(x)+(1-t)f(y)$. For $X,Y,P$ as above, the question is whether
$$
P f(X,Y)P=P f(PXP,PYP)P
\quad\Longrightarrow\quad
PX=XP\ \text{and}\ PY=YP.
$$
Both outer projections on the right are part of the original assertion. There is no hypothesis that $f(0,0)=0$. Commutation of $P$ with each coordinate operator is exactly the reducing-subspace conclusion asked for in the [source](https://rybindmitry.github.io/problems/2.html).
The accompanying standard infrastructure target asserts that, for every commuting pair of positive contractions on $H$,
$$
\exists!\,\Phi:C(S,\mathbb R)\longrightarrow\mathcal B(H),\qquad
\Phi(x\mapsto x_0)=X,\quad\Phi(x\mapsto x_1)=Y,
$$
where $\Phi$ is continuous, unital, real-linear, multiplicative and star-preserving. This is the unit-square, real-valued-function specialization of [Lemma 6.6](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43), not a claim that this known theorem is a new research conjecture. Its Lean proof is a separate supporting obligation. The earlier two-dimensional milestone and the proved finite-dimensional capstone remain available; neither replaces the new main target.
## Significance
A positive resolution would show that exact preservation of one strictly convex functional-calculus value, under the specified commuting-compression hypothesis, forces both operators to preserve the projection's range and its orthogonal complement. A negative resolution would require an actual Hilbert space, operators and strictly convex function satisfying every hypothesis while at least one of the two reducing identities fails.
The formal development separates this research question from the standard spectral infrastructure needed to express it. The new main declaration is an open proof obligation. The joint-calculus existence-and-uniqueness declaration is also unproved in this contribution, although mathematically standard. Local compilation and server publication check the declarations' well-formedness; they are not proofs of either statement. Only the earlier finite-dimensional result is being reported here as already proved.
## Difficulty
Arbitrary bounded commuting self-adjoint operators need not have a joint eigenbasis. Consequently a matrix formulation that records finitely many joint spectral atoms cannot serve as the general operator model. The compressed pair may also have different spectral data from the original pair. The equality involves these two different functional calculi, with a projection on either side of each value.
Strict convexity in this question is ordinary scalar strict convexity on the square. Operator convexity, finite rank of the projection, compactness of the coordinate operators, and a multivariable operator Jensen inequality are not additional assumptions. Introducing any of them would change the requested question. The general formulation must also retain boundary cases rather than exclude them to simplify an argument.
## Formalization scope
The Lean model uses actual bounded complex-linear maps on an arbitrary complete inner-product space. It imposes no finite-dimensionality, separability, common-eigenbasis or nonzero-space assumption. It includes $P=0$, $P=I_H$ and the zero Hilbert space. The scalar field convention is complex; a real-Hilbert-space transfer is not separately formalized here.
The function is stored on the ambient real plane, but continuity, strict convexity and evaluation use only its restriction to $S$. Values outside $S$ are irrelevant, and continuity outside the square is not required. Thus storing an ambient function does not exclude any continuous function originally defined only on the square.
Joint evaluation is a total definition. If a representing continuous unital real star-algebra homomorphism exists, it chooses one for the operator pair and then evaluates the supplied function. Otherwise it returns zero. The separate existence-and-uniqueness target establishes that this fallback is inapplicable to commuting positive contractions and that the choice is immaterial. No field in the model assumes the compression-rigidity conclusion. The supporting standard theorem must also apply to the compressed pair using the original projection and positivity hypotheses, without adding representation existence as a new restriction on the main question.
The replacement definition and both statements were built at Lean 4.30.0 with supported Mathlib revision `c5ea00351c28e24afc9f0f84379aa41082b1188f`, and their final versions received independent blind readbacks. Published older declarations and their proof identities are preserved. They should be cited with their finite-dimensional scope, not described as a solution of the arbitrary-Hilbert-space target.
## Selected references
- Boris Bilich, *Equality case for compressed convex functional calculus*, CUHK-Shenzhen AI Math Problems, Problem 2, added June 1, 2026. [Original statement](https://rybindmitry.github.io/problems/2.html).
- Jan Dereziński, *Bounded operators*, Warsaw University lecture notes, January 2007, Lemma 6.6, printed page 43. [Joint continuous functional calculus](https://www.fuw.edu.pl/~derezins/mat-o.pdf#page=43).
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).
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.
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.
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.