Dynamic Programming and Optimal Control VII: Infinite Horizon ProblemsTextbook
## Motivation
Infinite-horizon dynamic programming is the mathematical core of Markov decision processes and reinforcement learning: Bellman equations, value iteration, policy iteration, and their guarantees. Chapter 7 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) develops the finite-state theory in its cleanest generality — stochastic shortest path (SSP) problems first (Prop. 7.2.1–7.2.2), with discounted problems (Prop. 7.3.1) and average-cost problems (Prop. 7.4.1–7.4.2) derived from the SSP analysis. These propositions are cited throughout the MDP/RL literature as the base case of the theory; none of them exists in Mathlib.
## Setting
States $1, \dots, n$ plus an implicit cost-free absorbing termination state $t$; finite nonempty control sets $U(i)$; costs $g(i,u)$; sub-stochastic transitions $p_{ij}(u) \ge 0$, $\sum_j p_{ij}(u) \le 1$, the deficit being the termination probability (`BertsekasSSPModel`). Operators
$$(T_\mu J)(i) = g(i,\mu(i)) + \sum_j p_{ij}(\mu(i)) J(j), \qquad (TJ)(i) = \min_{u \in U(i)}\Big[g(i,u) + \sum_j p_{ij}(u) J(j)\Big]$$
(`BertsekasSSPPolicyOp`, `BertsekasSSPBellmanOp`), $N$-stage costs by backward recursion with policy shift (`BertsekasSSPNCost`), and the survival mass $P\{x_m \ne t\}$ (`BertsekasSSPSurvival`). **Assumption 7.2.1**: for some $m > 0$, every admissible policy has survival mass $< 1$ from every state after $m$ stages. The discounted setting reuses the same model with stochastic rows and $0 < \alpha < 1$ (`BertsekasDiscounted*`); the average-cost setting adds a designated state $s$ with the avoidance probability of Assumption 7.4.1 (`BertsekasSSPAvoidProb`).
## Target
Under Assumption 7.2.1, there is a vector $J^*$ with
$$T^k J_0 \to J^* \ \ \forall J_0, \qquad J^* = T J^* \text{ uniquely}, \qquad J^*(i) \le J_\pi(i) = \lim_N J^N_\pi(i) \ \ \forall \pi \text{ admissible},$$
and a stationary policy attaining $J^*$ — `BertsekasDP.ssp_main_theorem` (goal, Prop. 7.2.1(a),(b)). Milestones: 7.2.1(c) policy evaluation, 7.2.1(d) optimality iff greediness, 7.2.2 policy iteration, 7.3.1 the full discounted counterpart, 7.4.1 the average-cost Bellman equation, 7.4.2 average-cost policy iteration.
## Significance
These are the convergence guarantees behind value iteration and policy iteration — the two algorithms at the root of dynamic programming practice and of RL analyses (Q-learning's target operator is exactly $T$). The SSP form is the strongest of the three: the discounted theory is its special case (termination with probability $1 - \alpha$ per stage) and the average-cost theory reduces to it through cycles at the recurrent state. Formalized, the chapter yields a reusable finite-MDP theory: monotone operators, $m$-stage contractions, and the machinery for later Vol. II material. All results are proved in the book; the formalization is new.
## Difficulty
$T$ is not a one-stage contraction in the sup-norm under Assumption 7.2.1 — only an $m$-stage contraction, uniformly over the finitely many $m$-stage policy prefixes; extracting the uniform contraction factor $\rho < 1$ (via finiteness of the policy space) is the crux of the whole chapter. The limit of $N$-stage costs for *nonstationary* policies must be established, not assumed (tail-sum estimate $\rho^{\lfloor N/m \rfloor}$). For the average-cost results the associated-SSP construction (stop on reaching $s$) must be built inside the proof. The liminf phrasing of average-cost optimality is deliberate: for arbitrary nonstationary policies the Cesàro limit need not exist.
## Formalization scope
Finite states `Fin n`, finite control type, constraint sets as `Finset`s with attained minima; no termination state in the carrier — termination is the sub-stochastic deficit, exactly as the book treats it computationally. Policies are sequences of stage policies (Markov); costs of nonstationary policies via the shift recursion. Convergence is `Tendsto` in the product topology (equivalently sup-norm, $n$ finite). Average cost uses real `liminf` and division with the $N = 0$ term junk-valued at 0 (irrelevant at infinity). The discounted theorem packages parts (a)–(e) in one statement mirroring Prop. 7.3.1.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (§7.1–7.4.) http://www.athenasc.com/dpbook.html
- D. P. Bertsekas, J. N. Tsitsiklis, An analysis of stochastic shortest path problems, *Math. Oper. Res.* 16 (1991), 580–595. https://doi.org/10.1287/moor.16.3.580
- M. L. Puterman, *Markov Decision Processes*, Wiley, 1994. https://doi.org/10.1002/9780470316887
Dynamic Programming and Optimal Control V: LQG and Certainty EquivalenceTextbook
## Motivation
The separation theorem — certainty equivalence for linear-quadratic control with imperfect state information — is one of the celebrated structural results of stochastic control: the optimal controller splits into a least-squares estimator and the deterministic LQR actuator, designed independently. It underlies every LQG autopilot and Kalman-filter-based regulator. Section 5.2 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) proves it from the DP algorithm over information vectors, with Lemma 5.2.1 supplying the key fact that the estimation error is beyond the controller's influence. No formal analogue exists in Mathlib.
## Setting
Linear dynamics and measurements
$$x_{k+1} = A_k x_k + B_k u_k + w_k, \qquad z_k = C_k x_k + v_k,$$
with quadratic cost $\mathbb{E}\big[x_N^\top Q_N x_N + \sum_{k<N}(x_k^\top Q_k x_k + u_k^\top R_k u_k)\big]$, $Q_k \succeq 0$, $R_k \succ 0$. The initial state and the zero-mean disturbances/noises are independent with finite ranges; independence is structural — the sample space is the product of an initial-state coordinate and per-stage noise coordinates (`BertsekasLQGModel`, `BertsekasLQGSample`, `BertsekasLQGProb`). A **policy** maps the realized measurement history $(z_0,\dots,z_k)$ to $u_k$; the closed-loop process is `BertsekasLQGTraj`, the expected cost `BertsekasLQGCost`. The estimator $\mathbb{E}[x_k \mid I_k]$ is an explicit conditional average (`BertsekasCondExpVec`, `BertsekasLQGEstimate`); the gains $L_k$ come from the time-varying Riccati recursion (`BertsekasLQGRiccati`, `BertsekasLQGGain`).
## Target
$$\pi^*(I_k) = L_k\, \mathbb{E}[x_k \mid I_k] \ \text{ along its own trajectories} \quad\Longrightarrow\quad J(\pi^*) \le J(\pi)\ \ \forall \pi,$$
— `BertsekasDP.lqg_certainty_equivalence` (goal). Milestone: Lemma 5.2.1 in pointwise form — the error $x_k - \mathbb{E}[x_k \mid I_k]$ is the same under any two policies, outcome by outcome (`lqg_estimation_error_policy_independent`).
## Significance
This is the theorem that justifies designing estimator and controller separately — remove it and the entire LQG methodology loses its warrant. The formalization also yields the first machine-checked instance of the informational decomposition (control-dependent part + policy-independent error) that recurs throughout imperfect-information control. Notably the result needs no Gaussian assumption — only zero mean and independence — and the finite-support model makes that generality exact. The result is classical (Joseph–Tou 1961, Gunckel–Franklin 1963; the book's §5.2); the formal proof is new.
## Difficulty
The heart is Lemma 5.2.1: showing the estimation error coincides, sample by sample, with the error of the control-free system — which requires proving that the observation-history σ-events under any policy coincide with those of the control-free system (controls are determined by the history, so they shift observations by a known amount). Then the DP argument over information histories must carry the quadratic decomposition through the backward recursion. Bookkeeping over histories-as-lists is the main formal burden; probability theory stays finite.
## Formalization scope
Finite-support randomness (all expectations are finite sums); conditional expectation with the explicit junk value 0 on zero-probability events — the goal's hypothesis is accordingly restricted to outcomes of positive probability. Policies are functions of the measurement list only (equivalent to the book's information vector for deterministic policies, since past controls are recoverable from past measurements). Matrices are time-varying; positive definiteness of $R_k$ makes every matrix inverse in the gains genuine. Measurement noise covariance is *not* assumed positive definite — the estimator is the abstract conditional expectation, not the Kalman filter (whose recursive form, §5.2.1, would be a natural follow-up mission).
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (§5.2, Lemma 5.2.1.) http://www.athenasc.com/dpbook.html
- P. D. Joseph, J. T. Tou, On linear control theory, *Trans. AIEE* 80 (1961), 193–196. https://doi.org/10.1109/TAI.1961.6371743
- T. L. Gunckel, G. F. Franklin, A general solution for linear sampled-data control, *J. Basic Eng.* 85 (1963), 197–201. https://doi.org/10.1115/1.3656559
## Motivation
A polynomial $f \in \mathbb{Q}[x]$ is **split** if $\deg f \ge 1$ and $f(x) = a\prod_{i=1}^{n}(x - r_i)$ for some $a \in \mathbb{Q}^\times$ and $r_1,\dots,r_n \in \mathbb{Q}$. Split polynomials are the simplest non-constant maps defined over $\mathbb{Q}$ that one can apply to an algebraic number: they are exactly the rational polynomials all of whose roots are rational. The question here is how much such a map can do — whether it can always push an algebraic number back down into $\mathbb{Q}$.
Say $\alpha$ is **$k$-collapsible** if there are split $f_1,\dots,f_k$ with $(f_k \circ \cdots \circ f_1)(\alpha) \in \mathbb{Q}$, **collapsible** if it is $1$-collapsible, and **eventually collapsible** if it is $k$-collapsible for some $k \ge 1$. Problem 3 of Griffin Macris's list of open problems asks whether every algebraic number is eventually collapsible. The two notions come apart at degree $3$: Jordi Ribes settled the cubic case of *eventual* collapsibility using a composition of three split polynomials, and for eventual collapsibility the open frontier is $\deg\alpha \ge 4$. For the one-step notion the picture is different — degrees $1$ and $2$ are settled, and **degree $3$ is open**. That one-step cubic case is this mission's goal.
## Setting
Let $\alpha$ be an algebraic number with $[\mathbb{Q}(\alpha):\mathbb{Q}] = 3$. After an affine change of variable over $\mathbb{Q}$ one may assume $\alpha$ is a root of a **depressed cubic**
$$m(x) = x^3 + d\,x + e, \qquad d, e \in \mathbb{Q},$$
with **discriminant** $\Delta = \operatorname{disc}(m) = -4d^3 - 27e^2$. When $\Delta > 0$ the cubic is *totally real* (three real roots); when $\Delta < 0$ it has one real root and a complex-conjugate pair. In the latter case write the roots as
$$\alpha_1 = -2u, \qquad \alpha_{2,3} = u \pm iv, \qquad d = v^2 - 3u^2, \quad e = 2u(u^2 + v^2),$$
and set $\psi = \arctan(3u/v)$, the parameter that controls the archimedean obstruction below. Scaling $\alpha \mapsto w\alpha$ sends $(d,e) \mapsto (w^2 d, w^3 e)$, so the single rational invariant
$$\tau = e^2/d^3$$
determines the problem up to scaling: the search space is one rational parameter, not two.
## Formalization targets
### Goal — every cubic algebraic number is collapsible
$$\forall\, \alpha \in \mathbb{C}, \quad [\mathbb{Q}(\alpha):\mathbb{Q}] = 3 \ \Longrightarrow\ \exists\, f \text{ split with } f(\alpha) \in \mathbb{Q}.$$
This is the weakest statement that settles the case: it fixes no bound on $\deg f$, and asserts only that some split $f$ exists. A version with a degree bound would be strictly stronger and is not the goal, because no such bound is known — indeed the archimedean milestone below shows no uniform one can exist.
### Supporting targets
The milestone list runs from the reformulation and the invariance reductions, through the known sufficient conditions, to the two obstructions and the two genuinely open sub-targets. Ordered as they are stated there:
1. the **product criterion** — $\alpha$ is collapsible iff $\prod_i(\alpha - r_i) \in \mathbb{Q}$ for some nonempty finite multiset of rationals, which turns collapsibility into a multiplicative relation in $K^\times/\mathbb{Q}^\times$;
2. **affine invariance**, and the completeness of $\tau$ as an invariant of the scaling action, which together justify the reduction to one parameter;
3. two **sufficient conditions**: square discriminant, and the power-family condition subsuming it;
4. three **obstructions**: gap parity in the totally real case; the archimedean degree bound when $\Delta < 0$; and the extension of that bound beyond cubics, to any algebraic number possessing both a real and a non-real conjugate.
The mission also carries, as a plain theorem rather than a milestone, the single open instance $x^3 + 6x + 1$ — the smallest cubic within computational reach for which no collapsing is known. It is an instance of the goal rather than a step toward it, which is why it is not on the attack path.
## Significance
A proof of the goal closes the one-step cubic case and, with Ribes's composition result, would give a complete picture at degree $3$. A disproof would be at least as informative: a single cubic $\alpha$ admitting no split $f$ with $f(\alpha) \in \mathbb{Q}$ would separate $1$-collapsibility from eventual collapsibility by an explicit example, showing that composition is genuinely necessary and not an artefact of the known proof.
The supporting targets have value independent of the goal. The product criterion is the statement everything else is phrased against. The archimedean bound is the only known mechanism forcing $\deg f \to \infty$, and it is what rules out a uniform-degree approach.
Status, stated precisely. Six of the eight milestones have machine-checked Lean 4 + Mathlib proofs in the author's development, against a newer Mathlib revision than this mission's environment; restating and reproving them here is a port, not new mathematics, and they are included because the goal cannot be attacked without them. The two archimedean milestones are **not** proved in that form. For the cubic bound both halves exist — the convexity argument and the Möbius reduction — but the statement in terms of a collapsing polynomial has not been assembled. The extension beyond cubics has not been formalised at all; the argument is the same one, since nothing in it uses cubicness beyond the identification of a single circle parameter, but that observation is not a proof. The instance $x^3 + 6x + 1$ and the goal itself are open.
## Difficulty
The obvious approach is to write down a split $f$ with rational roots and force $f(\alpha) \in \mathbb{Q}$ by solving for the roots. This works when $\Delta$ is a rational square, and more generally under the power-family condition, and produces the bulk of the known examples — but it cannot work in general, for a reason that is quantitative rather than technical.
Suppose $\Delta < 0$ and $f = a\prod_i(x - r_i)$ is split with $f(\alpha) \in \mathbb{Q}$. Irreducibility of $m$ forces $f - c$ to be divisible by $m$, hence $f(\alpha_1) = f(\alpha_2) \ne 0$, hence $\prod_i \frac{\alpha_1 - r_i}{\alpha_2 - r_i} = 1$. Each factor lies on a fixed circle through $0$ and $1$ determined by $\psi$, and a convexity argument on $\log\cos$ then forces
$$\deg f \ \ge\ \pi/\psi.$$
As $\tau \to 0^+$ one has $\psi \to 0$, so the required degree is unbounded: there is no uniform degree in which to search, and any construction must produce split polynomials of growing degree. This is the central difficulty. For $x^3 + 6x + 1$ the bound already gives $\deg f \ge 32$, which is why that cubic resists the searches that settle its neighbours.
Only one step of this argument is special to cubics: the identification of the circle parameter as $3u/v$. For an algebraic number of any degree with a real conjugate $\alpha_1$ and a non-real conjugate $\alpha_2$, irreducibility gives the same relation $\prod_i (\alpha_1 - r_i)/(\alpha_2 - r_i) = 1$, the images again lie on a circle through $0$ and $1$, and the parameter is $\lambda = (\operatorname{Re}\alpha_2 - \alpha_1)/\operatorname{Im}\alpha_2$, which specialises to $3u/v$ in the depressed-cubic case. The obstruction therefore constrains the whole conjecture, not merely its cubic case, which is why the extension is carried as a milestone in its own right.
In the totally real case ($\Delta > 0$) the archimedean argument gives nothing at all — the relevant Möbius maps are real and surject onto $\widehat{\mathbb{R}}$ — and the only known constraint is that each gap between consecutive conjugates contains an even number of roots of $f$. Whether degrees stay bounded there is itself unsettled.
## Formalization scope
**Representation.** `IsSplit f` says $0 < \deg f$ and $f = C\,a \cdot \prod_{r \in rs}(X - r)$ for a nonzero rational $a$ and a multiset $rs$ of rationals; multiplicities are therefore allowed and the roots need not be distinct. `Collapsible α` is stated for $\alpha$ in an arbitrary field $K$ carrying a $\mathbb{Q}$-algebra structure, not only for $K = \mathbb{C}$, so the results apply verbatim to a root in $\mathbb{R}$, in $\mathbb{C}$, or in $\mathbb{Q}[x]/(m)$. The goal theorem is stated over $\mathbb{C}$, with "cubic" expressed as $\deg(\operatorname{minpoly}_{\mathbb{Q}}\alpha) = 3$.
**Ruling out a trivialisation.** `Collapsible` places no lower bound on $\deg f$ and does not require the value $c = f(\alpha)$ to be nonzero, so one must check that the goal is not satisfiable by degenerate means. It is not: $c = 0$ would make $m \mid f$, impossible for an irreducible cubic $m$ dividing a polynomial that splits over $\mathbb{Q}$. Constant $f$ is excluded by $0 < \deg f$. Nothing in the statement is vacuous — the hypotheses of the goal are satisfied by every cubic irrationality.
**Conventions in the archimedean milestones.** In the cubic bound the parameters $u, v$ enter as real numbers satisfying the factorisation identity, with the normalisation $0 < uv$; this is not a restriction, since $v$ is determined only up to sign and the sign may be chosen. Under it $\psi = \arctan(3u/v) \in (0, \pi/2)$, and the conclusion is $\pi/\psi \le \deg f$ with $\deg f$ the natural-number degree.
In the general bound the corresponding normalisation is $0 < (\operatorname{Re}\alpha_2 - \alpha_1)\operatorname{Im}\alpha_2$. It forces $\operatorname{Im}\alpha_2 \neq 0$, so $\alpha_2$ is genuinely non-real and $\lambda > 0$, hence $\psi \in (0,\pi/2)$ and no division-by-zero value can arise in the conclusion. Passing to the complex conjugate of $\alpha_2$ flips the sign of both factors, so the condition is a choice of conjugate rather than a restriction — except when $\operatorname{Re}\alpha_2 = \alpha_1$, which the hypothesis excludes and which cannot occur for a depressed cubic with $\Delta<0$. No degree hypothesis on $m$ is needed: possessing both a real and a non-real root already forces $\deg m \ge 3$.
**Infrastructure.** A complete development needs `Polynomial`, `Multiset`, `minpoly`, and for the archimedean bound `Real.arctan`, `Complex.arg`, and strict concavity of $\log\cos$ on $(-\pi/2, \pi/2)$. The convexity and Möbius lemmas are reusable well beyond this mission — they bound the number of factors in any product of complex numbers constrained to a circle through the origin. Contributions of any of the supporting targets are welcome independently of the goal; so is a disproof, and so is an explicit collapsing of $x^3 + 6x + 1$ of any degree.
## Selected references
- Griffin Macris, *List of open problems*, Problem 3. https://sites.google.com/view/griffinmacris/open-problems
- Miles, *Collapsible algebraic numbers*, 2026. https://quesswho.github.io/miles-blog/2026/08/20/collapsible/ — source of the definitions of split, $k$-collapsible, collapsible and eventually collapsible used above, of Ribes's cubic result for eventual collapsibility, and of the statement that the degree-$3$ case of one-step collapsibility is open.
## Motivation
A positive integer is **perfect** when it equals the sum of its proper divisors: $6 = 1 + 2 + 3$, $28 = 1 + 2 + 4 + 7 + 14$, then $496$, $8128$, and so on. Every perfect number anyone has ever exhibited is even. Whether an odd one exists is one of the oldest unsettled questions in mathematics, and it is unsettled in a strong sense: there is no heuristic consensus that odd perfect numbers should be absent for a structural reason, only an accumulating list of conditions any example would have to meet.
The even side of the question is completely resolved. Euclid (Elements IX.36) showed that if $2^p - 1$ is prime then $2^{p-1}(2^p - 1)$ is perfect; Euler proved the converse, so even perfect numbers correspond exactly to Mersenne primes. Nothing comparable is known on the odd side, and the literature instead consists of increasingly severe necessary conditions.
A timeline of what is actually proved about a hypothetical odd perfect number $N$:
- **Euler** (published posthumously in 1849): $N = p^k m^2$ with $p$ prime, $p \equiv k \equiv 1 \pmod 4$, and $p \nmid m$. In particular $N$ is not a perfect square.
- **Servais (1887), Sylvester (1888)**: lower bounds on the number $\omega(N)$ of distinct prime divisors; Sylvester obtained $\omega(N) \ge 5$, and $\omega(N) \ge 8$ when $3 \nmid N$.
- **Touchard (1953)**: $N \equiv 1 \pmod{12}$ or $N \equiv 9 \pmod{36}$. Shorter proofs were later given by Satyanarayana (1959) and Holdener (2002).
- **Chein (1979) and Hagis (1980)**, independently: $\omega(N) \ge 8$; Nielsen (2007): $\omega(N) \ge 9$; Nielsen (2015): $\omega(N) \ge 10$.
- **Nielsen (2003)**: an upper bound in terms of $\omega$, namely $N < 2^{4^{\omega(N)}}$ — the first bound of its kind, later sharpened by Nielsen himself.
- **Ochem–Rao (2012)**: $N > 10^{1500}$; **Ochem–Rao (2014)**: $N$ has at least $101$ prime factors counted with multiplicity.
None of these results, alone or together, rules out an odd perfect number.
## Setting
For $n \ge 1$ write $\sigma(n) = \sum_{d \mid n} d$ for the sum of all positive divisors of $n$. Then $n$ is **perfect** exactly when
$$\sigma(n) = 2n,$$
equivalently when the divisors of $n$ other than $n$ itself sum to $n$. The function $\sigma$ is **multiplicative**: $\sigma(ab) = \sigma(a)\sigma(b)$ whenever $\gcd(a,b) = 1$, and $\sigma(p^a) = 1 + p + \cdots + p^a$ for a prime power. The quantity $\sigma(n)/n$ is the **abundancy index** of $n$, so a perfect number is one of abundancy index exactly $2$.
Write $\omega(n)$ for the number of distinct prime divisors of $n$. In Lean, $\omega(n)$ is `n.primeFactors.card`, and perfection is Mathlib's `Nat.Perfect n`, which unfolds to `∑ i ∈ n.properDivisors, i = n ∧ 0 < n` — the positivity clause is part of the definition, so $n = 0$ is not perfect.
## Formalization targets
### Goal
$$\forall n \in \mathbb{N}, \quad \sigma(n) = 2n \ \Longrightarrow\ 2 \mid n.$$
Every perfect number is even; equivalently, no odd perfect number exists. This is the weakest statement that settles the question, and it fixes no constants, so no future numerical improvement can invalidate it.
### Milestones
The milestones are the unconditional theorems of the literature listed above, each stated for a hypothetical odd perfect number $N$:
$$N = p^k m^2, \quad p \text{ prime}, \quad p \equiv k \equiv 1 \ (\mathrm{mod}\ 4), \quad p \nmid m \qquad \text{(Euler)}$$
$$N \text{ is not a perfect square} \qquad \text{(Euler)}$$
$$\omega(N) \ge 3, \qquad \omega(N) \ge 5 \qquad \text{(Servais, Sylvester)}$$
$$N \equiv 1 \ (\mathrm{mod}\ 12) \quad \text{or} \quad N \equiv 9 \ (\mathrm{mod}\ 36) \qquad \text{(Touchard)}$$
$$N < 2^{4^{\omega(N)}} \qquad \text{(Nielsen)}$$
## Significance
*The result itself.* A proof of the goal would complete the classification of perfect numbers begun by Euclid: together with the Euclid–Euler theorem, every perfect number would be $2^{p-1}(2^p-1)$ for a Mersenne prime $2^p - 1$. A disproof — an explicit odd perfect number — would be an object with at least ten distinct prime factors and more than $1500$ decimal digits, and would immediately settle a long list of dependent questions about the abundancy index, about the distribution of the values of $\sigma$, and about the multiperfect numbers.
*Formalizing it.* Only the even half of the theory is currently formalized: the Euclid–Euler theorem is available in Mathlib's Archive (`Archive/Wiedijk100Theorems/PerfectNumbers.lean`, as `Nat.eq_two_pow_mul_prime_mersenne_of_even_perfect` and `Theorems.perfect_iff_even_and_mersenne`), and the main library carries the divisor-sum API around `Nat.Perfect` in `Mathlib/NumberTheory/Divisors.lean`, but nothing about the odd case. None of the milestones above is in Mathlib; formalizing them builds the missing $\sigma$-arithmetic infrastructure — factor chains, abundancy estimates, and the parity analysis of $\sigma$ on odd numbers — that any attack on the goal, or any future formalization of the computational bounds, will need.
## Difficulty
The obvious approach — take Euler's form $N = p^k m^2$ and push the congruence conditions until they conflict — does not terminate. There is no known local obstruction: the equation $\sigma(N) = 2N$ has no contradiction modulo any fixed integer, so no congruence argument can close the problem. The known results are all of a different type: they exclude configurations of the prime factorization by finite case analysis on factor chains, and each analysis leaves infinitely many admissible configurations. Increasing $\omega$ weakens the constraints rather than strengthening them, which is why the lower bounds on $\omega$ have advanced by one prime factor per decade at very high computational cost. The upper bound $N < 2^{4^{\omega(N)}}$ makes the search space finite for each fixed $\omega$, but astronomically so.
## Formalization scope
The development is stated over `ℕ` with Mathlib's `Nat.Perfect`, so positivity is built into the hypothesis and no separate `0 < n` assumption appears. Oddness is `Odd n`, the number of distinct prime divisors is `n.primeFactors.card`, and Euler's form is stated with explicit residues `p % 4 = 1`, `k % 4 = 1`, together with `¬ p ∣ m` and `n = p ^ k * m ^ 2`. No custom definitions are introduced; everything rests on Mathlib's `Nat.sigma` / `Nat.Perfect` API.
One caution on the shape of the milestones. Each is stated conditionally, for an $n$ assumed both perfect and odd, so each would follow trivially from the goal theorem. The point of the milestones is precisely that they are proved *unconditionally* in the literature: a submission is expected to reproduce (or improve on) the published argument, not to derive the statement from an unproved conjecture. Since the goal is itself open on the platform, no admissible proof can take that shortcut.
Contributions welcome: any of the milestones, the supporting multiplicativity and abundancy lemmas needed for them, and reusable infrastructure for $\sigma$ on odd numbers. Sharper published bounds — larger values of $\omega$, the improved Nielsen bound $N < 2^{4^{\omega(N)} - 2^{\omega(N)}}$, the Ochem–Rao size bound — are also in scope and are strictly stronger than the milestones listed.
## Selected references
- L. Euler, *De numeris amicabilibus*, Commentationes arithmeticae 2 (1849), 627–636.
- J. J. Sylvester, *Sur les nombres parfaits*, Comptes Rendus de l'Académie des Sciences CVI (1888), 403–405.
- J. Touchard, *On prime numbers and perfect numbers*, Scripta Mathematica 19 (1953), 35–39.
- J. A. Holdener, *A theorem of Touchard on the form of odd perfect numbers*, American Mathematical Monthly 109 (2002), 661–663.
- P. P. Nielsen, *An upper bound for odd perfect numbers*, INTEGERS: Electronic Journal of Combinatorial Number Theory 3 (2003), #A14.
- P. P. Nielsen, *Odd perfect numbers have at least nine distinct prime factors*, Mathematics of Computation 76 (2007), 2109–2126.
- P. P. Nielsen, *Odd perfect numbers, Diophantine equations, and upper bounds*, Mathematics of Computation 84 (2015), 2549–2567.
- P. Ochem and M. Rao, *Odd perfect numbers are greater than $10^{1500}$*, Mathematics of Computation 81 (2012), 1869–1877.
- P. Ochem and M. Rao, *On the number of prime factors of an odd perfect number*, Mathematics of Computation 83 (2014), 2435–2439.
- Overview and further pointers: https://en.wikipedia.org/wiki/Perfect_number
Dynamic Programming and Optimal Control III: The Minimum PrincipleTextbook
## Motivation
The Pontryagin Minimum (Maximum) Principle is the fundamental necessary condition of optimal control, in continuous use since 1956 across aerospace guidance, robotics, and mathematical economics. Chapter 3 of Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I (3rd ed., 2005) develops it from the dynamic programming side: the HJB sufficiency theorem (Prop. 3.2.1), an envelope lemma (Lemma 3.3.1), the Minimum Principle itself (Prop. 3.3.1), and its discrete-time counterpart (Prop. 3.3.2). Mathlib's optimal-control coverage is currently near zero — no HJB equation, no adjoint equations, no maximum principle — which makes this the mission with the largest gap between textbook maturity and formal coverage in the series.
## Setting
Minimize, over admissible pairs, the cost
$$h(x(T)) + \int_0^T g(x(t), u(t))\,dt \quad\text{s.t.}\quad \dot x(t) = f(x(t), u(t)),\; x(0) = x_0,\; u(t) \in U \subseteq \mathbb{R}^m,$$
with $f, g, h$ continuously differentiable (`BertsekasCTModel`). Admissible controls are piecewise continuous on $[0,T]$ — formalized as: bounded image and continuous off a finite set (`BertsekasPiecewiseContinuousOn`) — and state trajectories are continuous, satisfying the ODE off a finite set (`BertsekasCTAdmissibleFrom`, parametrized by an arbitrary start $(t_0, \xi)$). The Hamiltonian is $H(x,u,p) = g(x,u) + \langle p, f(x,u)\rangle$ (`BertsekasHamiltonian`).
## Target
For an optimal admissible pair $(u^*, x^*)$: there exist an adjoint $p$ and a constant $c$ with
$$\dot p(t) = -\nabla_x H(x^*(t), u^*(t), p(t)), \quad p(T) = \nabla h(x^*(T)),$$
$$u^*(t) \in \arg\min_{u \in U} H(x^*(t), u, p(t)), \qquad H(x^*(t), u^*(t), p(t)) = c,$$
away from finitely many times — `BertsekasDP.pontryagin_minimum_principle` (goal). Milestones: Prop. 3.2.1 (`hjb_sufficiency_of_continuous`), Lemma 3.3.1 (`envelope_gradient_lemma`), Prop. 3.3.2 (`discrete_minimum_principle`).
The HJB milestone carries the hypotheses that $f$ and $g$ are jointly continuous — the consequence of the §3.1 standing assumptions that its proof uses. An earlier version without any regularity hypothesis was disproved: with a discontinuous running cost the cost integrand need not be integrable, and the library's integral of a non-integrable function is $0$.
## Significance
The Minimum Principle converts an infinite-dimensional optimization into a two-point boundary value problem — the basis of shooting methods and of every "bang-bang" analysis. None of it exists in Mathlib; even the HJB verification theorem would be new. The discrete-time milestone is self-contained multivariable calculus and gives early value; the envelope lemma is reusable well beyond control theory. The results are classical (Pontryagin et al. 1962; the book's Chapter 3); the formal proof of Prop. 3.3.1 will need an honest variational argument — the book's own HJB-based derivation is explicitly informal.
## Difficulty
For the goal: the classical proofs go through needle variations and a separation argument, or through regularity of the value function — neither is in Mathlib. The book's derivation assumes differentiability of the optimal value function, which is *not* a hypothesis of the statement; a formal proof must either supply a rigorous variational argument or add intermediate lemmas as new platform problems (sketching is encouraged). For the HJB milestone, the work is differentiating $t \mapsto V(t, x(t))$ along a trajectory that satisfies the ODE only off a finite set, then integrating.
## Formalization scope
States and controls in `EuclideanSpace ℝ (Fin n)` / `(Fin m)`; gradients in Mathlib's `gradient`; the ODE and adjoint via `HasDerivAt` off a finite exceptional set; costs via `intervalIntegral`. Piecewise continuity includes boundedness of the image, so the cost integrand of an admissible pair is genuinely integrable — the junk-value escape (non-integrable integrand ⇒ integral 0) is closed. Fixed initial state, fixed terminal time, free terminal state; time-independent dynamics (so the Hamiltonian is constant, per the book's remark that time-varying systems lose constancy). $U$ is an arbitrary set — no compactness or convexity is assumed in the goal.
## Selected references
- D. P. Bertsekas, *Dynamic Programming and Optimal Control*, Vol. I, 3rd ed., Athena Scientific, 2005. (Ch. 3.) http://www.athenasc.com/dpbook.html
- L. S. Pontryagin, V. G. Boltyanskii, R. V. Gamkrelidze, E. F. Mishchenko, *The Mathematical Theory of Optimal Processes*, Interscience, 1962.
- W. H. Fleming, R. W. Rishel, *Deterministic and Stochastic Optimal Control*, Springer, 1975. https://doi.org/10.1007/978-1-4612-6380-7
Monochromatic Reachability in Three-Colored Tournaments (OPG-1808)Open Problem
## Motivation
Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.
The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly `candidate_only`: it is bounded search evidence, not a proof of the unrestricted theorem.
## Setting
A **tournament** is an orientation of a finite complete simple graph. For each pair of distinct vertices $u,v$, exactly one of $u\to v$ and $v\to u$ is present. Every directed arc receives one of three labeled colors.
A **rainbow directed triangle** is a cyclically oriented triangle
$$
a\to b\to c\to a
$$
whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.
A vertex $s$ is a **monochromatic source** when, for every vertex $t$, there is some color $k$ and a directed $s$-to-$t$ path all of whose arcs have color $k$. The chosen color may depend on $t$; the theorem does not demand one common color for all targets. Length-zero reachability handles $t=s$.
The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.
## Formalization targets
### Root theorem
For every nonempty finite tournament $T$ with a three-coloring of its arcs,
$$
T\text{ has a rainbow directed triangle}
\quad\lor\quad
\exists s\in V(T)\ \forall t\in V(T),\
\text{$s$ reaches $t$ monochromatically}.
$$
No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.
### Finite order milestone
The first milestone freezes the exact bounded claim supported by the replay package:
$$
1\le |V(T)|\le 11\text{ and no rainbow directed triangle}
\quad\Longrightarrow\quad
T\text{ has a monochromatic source}.
$$
The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.
## Significance
The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.
The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc $u\to_F v$ may encode that $v$ cannot reach $u$; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.
## Difficulty
The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.
The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.
## Formalization scope
Lean represents the tournament as a binary relation `D` with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.
The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.
## Selected references
- Open Problem Garden, *Monochromatic reachability versus rainbow triangles*, posted 2008. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles
- B. Sands, N. Sauer, and R. Woodrow, *On monochromatic paths in edge-coloured digraphs*, Journal of Combinatorial Theory, Series B 33 (1982), 271–275.
- A. Georgakopoulos and P. Sprüssel, *On 3-coloured tournaments*, 2009. https://arxiv.org/abs/0904.1967
- A. Trygub, *Full Characterization of Color Degree Sequences in Complete Graphs Without Tricolored Triangles*, 2023. https://arxiv.org/abs/2304.14579
Circular (20,7)-Coloring of Triangle-Free Subcubic Planar Graphs (OPG-401)Open Problem
## Motivation
Circular coloring refines ordinary vertex coloring by placing colors on a cycle and measuring separation modulo the palette size. It records information that an ordinary chromatic-number bound can lose, and it interacts sharply with planarity, forbidden short cycles, and degree constraints. OPG-401 asks for a specific bound at the intersection of those themes: whether triangle-free planar graphs of maximum degree three always admit a circular coloring of ratio $20/7$.
The question appears on Xuding Zhu's open-problem page and in the Open Problem Garden record. Nearby theorems on fractional coloring do not settle it: fractional chromatic number and circular chromatic number are distinct parameters, so the known fractional bounds for subcubic triangle-free graphs cannot simply be substituted for a circular-coloring proof. Work on circular recoloring likewise studies connectivity between colorings that already exist and does not supply the missing universal existence theorem.
## Setting
For integers $p\ge 2q>0$, a **$(p,q)$-coloring** of a finite simple graph $G$ is a map
$$
\varphi:V(G)\longrightarrow \mathbb Z_p
$$
such that the shortest cyclic distance between $\varphi(u)$ and $\varphi(v)$ is at least $q$ for every edge $uv$. Equivalently, using representatives in $\{0,\ldots,p-1\}$, the modular difference lies between $q$ and $p-q$, inclusive. The **circular chromatic number** is the infimum of the ratios $p/q$ for which such a coloring exists.
The root domain consists of all finite simple graphs that are planar, triangle-free, and subcubic. Disconnected and empty graphs are included. Planarity is represented by an injective straight-line drawing with no vertex in the interior of an edge and no intersection between nonincident edges. For finite simple graphs this is the standard straight-line form of planarity.
## Formalization targets
### Root question
The central target is
$$
G\text{ finite, simple, planar, triangle-free, and }\Delta(G)\le 3
\quad\Longrightarrow\quad
G\text{ has a }(20,7)\text{-coloring}.
$$
This is exactly the claim $\chi_c(G)\le 20/7$ in a form suitable for finite Lean data.
### Local extension table
A reusable finite milestone freezes the local palette arithmetic. For $a\in\mathbb Z_{20}$, let $A(a)$ be the colors at cyclic distance at least seven from $a$. For all $a,b$,
$$
|A(a)\cap A(b)|=7-d_{20}(a,b),
\qquad
A(a)\cap A(b)\ne\varnothing\iff d_{20}(a,b)\le6.
$$
This includes equal colors, antipodal colors, tied symmetries, and all twenty residues. It is the exact obstruction encountered when extending a coloring over a deleted degree-two vertex while preserving every old color. The repository artifact supporting this formulation is only `candidate_only`; the mission publishes the statement as an open formal target rather than claiming it as proved.
## Significance
A proof of the root theorem would give the requested sharp circular-coloring guarantee uniformly over a broad planar graph class. It would also separate the circular problem from nearby fractional results by constructing the stronger cyclic palette assignment itself. A counterexample, if one exists, would have to survive the combined restrictions of planarity, triangle-freeness, and maximum degree three, and would identify a genuine boundary for local extension methods.
Formalization adds two concrete assets. First, the cyclic-distance convention is fixed once, avoiding common errors involving directed residues, unrestricted integer lifts, or truncated subtraction. Second, graph reductions can be checked against a precise preservation obligation: deleting a vertex does not help unless the chosen coloring of the smaller graph has compatible boundary colors. The mission therefore welcomes both global structural arguments and verified finite boundary classifications, but finite enumeration alone is not accepted as a proof for arbitrary graph order.
## Difficulty
The obvious induction on vertices fails at degree two. A coloring of $G-v$ need not extend over $v$: if its two neighbors receive colors at cyclic distance at least seven, their two allowed sets can be disjoint. The local table characterizes this failure exactly but does not guarantee that a different coloring of $G-v$ has favorable boundary values. Recoloring, reducible configurations, and planar discharging must therefore interact without silently assuming universal extension or connectivity of the recoloring graph.
A second source of difficulty is parameter confusion. Bounds for fractional colorings do not automatically yield $(20,7)$-colorings, and a theorem about mixing existing circular colorings does not prove existence. Any proposed bridge must be stated and verified explicitly.
## Formalization scope
Lean represents colors by `Fin 20` and uses the minimum of the two directed modular differences as cyclic distance. Edge compatibility includes both the lower bound $7$ and the formal upper bound $13$. Triangle-freeness is literal absence of three mutually cyclic adjacent vertices, and subcubic means every neighbor set has extended cardinality at most three.
The definition bundle contains no theorem and no `sorry`. Draft theorem items contain exactly one `:= by sorry`. The local candidate computations and GitHub transport records are provenance, not evidence that either theorem is proved. A complete contribution may formalize the finite palette table, a faithful reducible configuration, a recoloring lemma with all quantifiers exposed, or the root theorem. Every claimed universal reduction must retain finiteness, simplicity, planarity, triangle-freeness, and the degree bound.
## Selected references
- X. Zhu, *Circular chromatic number of triangle-free planar graphs with maximum degree three*, open-problem page. https://www.math.nsysu.edu.tw/~zhu/open-problems/chic-k3free-planar.htm
- Open Problem Garden, *OPG-401*. https://www.unsolvedmath.com/problems/OPG-401
- X. Zhu, *The fractional version of Hedetniemi's conjecture is true*, European Journal of Combinatorics, 2011. https://doi.org/10.1016/j.ejc.2011.03.004
- Z. Dvořák, J.-S. Sereni, and J. Volec, *Subcubic triangle-free graphs have fractional chromatic number at most 14/5*, Journal of the London Mathematical Society, 2014. https://arxiv.org/abs/1301.5296
## Motivation
Every introductory number theory course opens with the same fact: the integers factor into primes in exactly one way. Euclid's *Elements* (Book IX, Proposition 14) already proves a form of it for the case of two factorizations sharing no further structure, but the theorem is not stated in full generality — with existence *and* uniqueness as a single package — until Gauss's *Disquisitiones Arithmeticae* (1801, Art. 16). Every standard modern treatment restates it as the opening theorem of the subject: Hardy & Wright, *An Introduction to the Theory of Numbers* (Theorem 2), and Apostol, *Introduction to Analytic Number Theory* (1976, Theorems 1.9–1.10), both prove it in the first chapter, before anything else is developed. The reason is structural, not pedagogical convenience: gcd, lcm, multiplicative functions, the notion of "the" prime factorization of an integer, and the entire multiplicative structure of $\mathbb{Z}$ depend on it being true. Mathlib itself packages the general statement as `UniqueFactorizationMonoid`, of which $\mathbb{N}$ is one instance — this mission asks for the classical, elementary argument specific to $\mathbb{N}$, in the two-part shape every textbook gives it.
## Setting
A **prime** $p \in \mathbb{N}$ is a natural number $p \geq 2$ whose only divisors are $1$ and $p$ (Mathlib's `Nat.Prime`). A **factorization** of $n \in \mathbb{N}$ is represented here as a **multiset** $l$ of natural numbers — an unordered collection that tracks multiplicity but not order, so that two factorizations differing only by a reordering of their factors are already identified as the same multiset, with no separate permutation argument needed. Write $l.\mathrm{prod} = \prod_{p \in l} p$ for the product of the elements of $l$ with multiplicity, under the convention that the empty multiset has product $1$. The theorem concerns multisets all of whose elements are prime.
## Formalization targets
### Goal — unique factorization
$$
\forall\, n \neq 0,\quad \exists!\, l : \mathrm{Multiset}\ \mathbb{N},\ \left(\forall p \in l,\ p \text{ prime}\right) \wedge l.\mathrm{prod} = n.
$$
For every nonzero $n$ there is exactly one multiset of primes whose product is $n$. This is the capstone: existence and uniqueness combined into the single statement every textbook eventually asserts.
### Milestone 1 — existence
$$
\forall\, n \neq 0,\quad \exists\, l : \mathrm{Multiset}\ \mathbb{N},\ \left(\forall p \in l,\ p \text{ prime}\right) \wedge l.\mathrm{prod} = n.
$$
Every nonzero natural number is *a* product of primes (Apostol, Theorem 1.9). This alone says nothing about how many such multisets there might be.
### Milestone 2 — uniqueness
$$
\left(\forall p \in l_1,\ p \text{ prime}\right) \wedge \left(\forall p \in l_2,\ p \text{ prime}\right) \wedge l_1.\mathrm{prod} = n = l_2.\mathrm{prod} \ \implies\ l_1 = l_2.
$$
Any two multisets of primes with the same product are equal (Apostol, Theorem 1.10). Combined with Milestone 1, this gives the Goal.
## Significance
**The result itself.** Unique factorization is what makes "the prime factorization of $n$" a well-defined object rather than a choice. Every downstream elementary and analytic number theory construction leans on it: $\gcd(a,b)$ and $\mathrm{lcm}(a,b)$ computed via shared prime exponents, multiplicative arithmetic functions ($\varphi$, $\sigma$, $\mu$) defined by their values on prime powers, the Euler product for $\zeta(s)$, and $p$-adic valuations. Without it, none of these constructions are canonical.
**Formalizing it.** The general statement is already machine-checked in Mathlib as an instance of `UniqueFactorizationMonoid` (and concretely realized for $\mathbb{N}$ via `Nat.factors`/`Nat.factors_unique`), so this is not open mathematics. What this mission asks for is the specific, elementary two-lemma argument — strong induction for existence, Euclid's lemma plus strong induction for uniqueness — spelled out for $\mathbb{N}$ with the `Multiset` representation used here, rather than a one-line appeal to the packaged Mathlib result. A solution that simply repackages `Nat.factors_unique` and its companions is a legitimate route (nothing here is designed to block it), but the more valuable contribution is the self-contained classical proof, since that is what a reader of Apostol or Hardy & Wright expects to see reconstructed.
## Difficulty
For **existence**, ordinary induction on $n$ does not immediately work: if $n$ is composite, $n = ab$ with $1 < a, b < n$, and the inductive hypothesis is needed for *both* $a$ and $b$ at once, neither of which is simply $n - 1$. The fix is strong (well-founded) induction on $n$, splitting into the prime case (trivial single-element multiset) and the composite case (combine the two multisets for $a$ and $b$).
For **uniqueness**, the natural first attempt — "cancel a common prime factor from both sides and recurse" — silently assumes that the *same* prime appears in both multisets, which is exactly what needs to be proved. The step that actually does the work is **Euclid's lemma**: if a prime $p$ divides a product $l_2.\mathrm{prod}$, it divides one of the factors of $l_2$. This is not a restatement of primality (irreducibility, "no nontrivial divisors") but a genuinely separate fact about $\mathbb{N}$ that requires either Bézout's identity or a well-ordering argument to establish; conflating "prime" with "has this divisibility property" is the standard trap for a first attempt at this proof.
## Formalization scope
The statement is specific to $\mathbb{N}$ (not $\mathbb{Z}$ or a general `UniqueFactorizationMonoid`), and factorizations are represented as `Multiset ℕ` rather than `List ℕ` up to permutation — this is a deliberate choice that folds "unique up to reordering" directly into multiset equality. The hypothesis is $n \neq 0$, not $n > 1$: the case $n = 1$ is included, and its unique witness is the *empty* multiset, since the empty product is $1$ and no nonempty multiset of primes (each $\geq 2$) can have product $1$. $n = 0$ is excluded because no multiset of natural numbers has product $0$ under this convention (every prime is $\geq 2$, and the empty product is $1$), so no factorization of $0$ exists to be unique.
No auxiliary platform `Definitions` are required — the statement is expressed entirely in terms of `Nat.Prime` and `Multiset.prod` from Mathlib. Reusable contributions welcome beyond the two milestones: an explicit construction of the canonical *sorted* `List ℕ` factorization (`Nat.factors`-style) connecting this multiset formulation to the more computational list representation, or a generalization of the uniqueness argument to an explicit statement and proof of Euclid's lemma as a standalone milestone.
## Selected references
- C. F. Gauss, *Disquisitiones Arithmeticae*, 1801, Art. 16.
- G. H. Hardy and E. M. Wright, *An Introduction to the Theory of Numbers*, 6th ed., Oxford University Press, 2008, Theorem 2.
- T. M. Apostol, *Introduction to Analytic Number Theory*, Springer, 1976, Theorems 1.9–1.10.
- The Mathlib Community, *Mathlib4*, `Mathlib.RingTheory.UniqueFactorizationDomain`, https://leanprover-community.github.io/mathlib4_docs/Mathlib/RingTheory/UniqueFactorizationDomain.html
Diaz's modulus conjecture: if |u| is algebraic, e^u is transcendentalOpen Problem
**If $|u|$ is algebraic and $u \neq 0$, is $e^{u}$ transcendental?** Guy Diaz asked this in 2004 and it is still open. Note it is $e^{u}$, not $e^{|u|}$ — the latter would follow at once from Hermite–Lindemann. The whole difficulty is that $u$ itself may be transcendental while only its modulus is constrained.
## The question
Write $\bar{\mathbb{Q}}$ for the algebraic numbers in $\mathbb{C}$ and
$$\mathcal{L}=\{u\in\mathbb{C}\ :\ e^{u}\in\bar{\mathbb{Q}}^{\times}\}$$
for the logarithms of algebraic numbers. In 2004 Guy Diaz asked, and conjectured, that no non-zero element of $\mathcal{L}$ has algebraic modulus. He states it as
> « Soit $u \in \mathbb{C}\setminus\{0\}$ avec $|u| \in \bar{\mathbb{Q}}$ ; alors $\mathrm{e}^{u}$ est transcendant. »
The statement fits on one line and needs no machinery beyond $\exp$ and $|\cdot|$. It has been open for twenty-two years.
It is not a curiosity. Diaz records that it follows from Schanuel's conjecture and also from the strong four exponentials conjecture, so it sits underneath two of the standard pillars of transcendence theory while being far more concrete than either. Anything that settles it settles a case of both.
## Why it suits a distributed platform
The mission decomposes into work that can be done **now**, without any open input.
Two milestones are *conditional* theorems — "Schanuel implies Diaz", "strong four exponentials implies Diaz". Diaz asserts both implications in a single sentence and does not write out either derivation; as far as I can establish, neither has been written out anywhere. Each is a short, self-contained argument that any solver can attack today. Both are stated here without axioms: Schanuel, the strong four exponentials conjecture and Hermite--Lindemann are all `Prop`-valued definitions in the mission's definition bundle, so a conditional milestone takes its hypothesis explicitly and nothing is assumed silently.
A third milestone is the elementary geometry of the configuration — the coordinate axes, which turn out to be exactly the degenerate branch where $u$ and $\bar u$ are $\mathbb{Q}$-linearly dependent.
The remaining two milestones are classical theorems that the platform's Mathlib does not have: **Hermite--Lindemann** and the **six exponentials theorem**. The first is needed by the four-exponentials route and by the axis case. The second is the proved member of the family this conjecture lives in, and the distance between it and the strong four exponentials conjecture is a fair measure of how far the known machinery falls short.
Only the top node needs genuinely new transcendence.
One structural remark that shapes the whole ladder: **Hermite--Lindemann is a special case of the goal**, not just an input to it. If $a \neq 0$ is algebraic then $|a|^{2} = a\bar a$ is algebraic, hence so is $|a|$, and the goal applied to $u := a$ gives that $e^{a}$ is transcendental. Diaz's conjecture is therefore strictly stronger than Hermite--Lindemann, and no route to it can avoid that node.
## Timeline
| | |
|---|---|
| 1873, 1882 | Hermite, then Lindemann: $e^{a}$ is transcendental for algebraic $a \neq 0$. In particular every non-zero element of $\mathcal{L}$ is itself transcendental, so a counterexample $u$ would be a transcendental number with algebraic modulus and algebraic exponential. |
| 1934--35 | Gelfond and Schneider settle Hilbert's seventh problem. |
| 1966 | Lang's *Introduction to Transcendental Numbers* records Schanuel's conjecture, and gives the six exponentials theorem (also Siegel, unpublished; Ramachandra 1968). The **four** exponentials conjecture stays open, and still is. |
| 1966 | Baker's theorem on linear forms in logarithms. |
| 1997 | Diaz studies the companion condition $\lvert\tau\rvert^{2}\in\mathbb{Q}$, assertion (4-1), p. 237. |
| 2000 | Waldschmidt's *Diophantine Approximation on Linear Algebraic Groups* states the conjecture at p. 399, credited to Diaz 1997, and records the relevant four-exponentials configuration with $y_1 = \lambda$, $y_2 = \lvert\lambda\rvert$ at p. 15. |
| 2004 | Diaz states the modulus question, §5.1, p. 550. On p. 551 he asks the accompanying methodological question: how could the non-holomorphic maps $z \mapsto \bar z$ and $z \mapsto \lvert z\rvert$ enter a transcendence proof at all? |
| 2026 | A machine-checked negative result on a class of strategies (see below). The conjecture itself is untouched. |
## What is known not to work
For a candidate $u$ one has $u\bar u = |u|^{2}$ with $|u|^{2}$ algebraic, hence
$$\bar u = \frac{|u|^{2}}{u}.$$
So $\bar u$ is not independent data: complex conjugation on $\bar{\mathbb{Q}}(u)$ is a rational function of the generator, determined by the ring structure. Three consequences follow, all formalised at <https://github.com/carlok/diaz-modulus-lean>: a ring homomorphism fixing $\bar{\mathbb{Q}}$ and carrying $u$ to any other transcendental point of the same circle automatically intertwines conjugation; such a homomorphism exists whenever both points are transcendental over the base; and no vanishing-coefficient statement over $\bar{\mathbb{Q}} \oplus \bar{\mathbb{Q}}u \oplus \bar{\mathbb{Q}}\bar u$ separates a candidate from an ordinary complex number placed on the same circle.
The practical consequence for solvers: **accumulating algebraic relations between $u$ and $\bar u$ until they collide cannot settle this.** A successful attack has to introduce information that is not a rational function of $u$ over $\bar{\mathbb{Q}}$ — which is precisely Diaz's own methodological question, still open.
## Mathlib gaps a solver will meet
- **Hermite--Lindemann is not in Mathlib.** Only the analytic half is present, in `Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean` — verified in all three of the platform's pinned revisions (`0df444a3`, `c5ea0035`, `777aaa61`), none of which contains `transcendental_exp`. Hence the choice to carry it as a `Prop` and give it its own milestone rather than assume it. There is an open PR, [leanprover-community/mathlib4#28013](https://github.com/leanprover-community/mathlib4/pull/28013) (*feat: Lindemann-Weierstrass Theorem*, opened 2025-08-05, label `awaiting-author` as of 2026-09-07); if it merges and a pin advances, that milestone collapses to a short transfer.
- **Neither Schanuel nor any four-exponentials statement exists in any form.** They are defined in the mission's bundle; that is the point, since the tractable content of this mission is what follows *from* them.
- **`Algebra.trdeg` has almost no computational API.** It is cardinal-valued, with transcendence bases and `lift_cardinalMk_eq_trdeg`, but nothing that evaluates the degree of an explicitly adjoined finite set. The Schanuel milestone will want a lemma of the shape "if $S \subseteq K(t)$ with $t$ transcendental over $K$ then $\operatorname{trdeg}_K K[S] \le 1$". That is worth splitting off as a child in its own right; it is reusable well beyond this mission.
## Sources
- G. Diaz, *Utilisation de la conjugaison complexe dans l'étude de la transcendance de valeurs de la fonction exponentielle usuelle*, J. Théor. Nombres Bordeaux **16** (2004), no. 3, 535–553, [doi:10.5802/jtnb.459](https://doi.org/10.5802/jtnb.459) — the conjecture is §5.1, p. 550; the methodological question is p. 551.
- G. Diaz (1997) — the companion condition $|\tau|^{2}\in\mathbb{Q}$ is assertion (4-1), p. 237.
- M. Waldschmidt, *Diophantine Approximation on Linear Algebraic Groups*, Grundlehren der mathematischen Wissenschaften **326**, Springer 2000 — pp. 15, 399, 614, and Exercise 15.16.
- S. Lang, *Introduction to Transcendental Numbers*, Addison-Wesley 1966, Ch. 2 (six exponentials, Schanuel's conjecture).
- A. Baker, *Transcendental Number Theory*, Cambridge University Press 1975, Theorem 1.4 (Hermite--Lindemann).
Six Colors for Star Edge-Coloring Subcubic Graphs (OPG-37271)Open Problem
## Motivation
A **star edge coloring** is a proper edge coloring with an additional local restriction: no path or cycle of four edges may use only two colors. It sits between ordinary proper edge coloring and strong edge coloring. The problem is local enough to admit finite obstruction searches, but global enough that independently valid local colorings may fail to fit together.
Dvořák, Mohar, and Šámal proved in 2013 that every subcubic multigraph has a star edge coloring with seven colors and conjectured that six always suffice. The Open Problem Garden records the simple-graph version as [OPG-37271](https://www.openproblemgarden.org/comment/reply/37271). The value six would be best possible because the complete bipartite graph $K_{3,3}$ has star chromatic index six.
Subsequent work has proved the six-color bound under additional hypotheses. Lei, Shi, and Song proved it for subcubic multigraphs with maximum average degree less than $5/2$ and obtained a five-color result below $24/11$. Casselgren, Granholm, and Raspaud proved the conjecture for cubic Halin graphs and several bipartite families. These results leave the unrestricted finite subcubic case as the target of this mission.
## Setting
Let $G$ be a finite simple undirected graph. An edge coloring assigns to each unordered edge of $G$ one color from a finite palette. It is **proper** if two distinct edges incident with the same vertex always have different colors.
A simple path of four edges has five pairwise distinct vertices $v_0,v_1,v_2,v_3,v_4$ and consecutive edges $v_0v_1,v_1v_2,v_2v_3,v_3v_4$. It is bichromatic in a proper coloring exactly when the first and third edges have the same color and the second and fourth edges have the same color. The path need not be induced: additional chords do not remove it. A four-cycle has four pairwise distinct vertices and is bichromatic under the analogous alternating equalities, including the closing edge.
A coloring is a **star edge coloring** when it is proper and contains neither type of bichromatic four-edge configuration. The star chromatic index $\chi'_s(G)$ is the least palette size admitting such a coloring. A graph is **subcubic** when every vertex has at most three neighbors.
## Formalization targets
### Goal — the six-color conjecture
The main target is the exact OPG-37271 assertion for finite simple graphs:
$$
\Delta(G)\le 3 \quad\Longrightarrow\quad \chi'_s(G)\le 6.
$$
In the Lean statement, this is expressed directly as the existence of a coloring by `Fin 6`; no separate minimization operator is needed.
### Known upper bound
The first literature milestone is the established seven-color theorem:
$$
\Delta(G)\le 3 \quad\Longrightarrow\quad \chi'_s(G)\le 7.
$$
Formalizing this result provides a checked baseline and infrastructure that a six-color argument can reuse.
### Sharpness at $K_{3,3}$
The second literature milestone records both sides of the exact value
$$
\chi'_s(K_{3,3})=6.
$$
Thus the mission cannot be completed by weakening the goal to a larger universal constant.
## Significance
A proof would determine the universal star chromatic-index bound for graphs of maximum degree three and would match the known lower-bound example $K_{3,3}$. A counterexample, if one exists, would separate six from the established seven-color bound and identify the first genuinely seven-chromatic subcubic graph.
The formalization contributes a reusable definition of star edge coloring on Mathlib finite simple graphs. In particular, it fixes several conventions that are easy to blur in informal or computational work: forbidden paths have four edges rather than four vertices; they are simple but need not be induced; four-cycles are checked separately; and properness is not inferred merely from the absence of an alternating four-edge pattern. These definitions can support certified bounded searches, verified coloring certificates, and later formalizations of sparse or planar special cases.
The current research repository contains candidate-only local extension criteria and finite certificates. They may motivate future milestones, but they are not treated here as proofs of the conjecture, as admitted evidence, or as replacements for the literature milestones.
## Difficulty
A direct greedy coloring argument can fail at a newly inserted edge because a color may be forbidden either by an adjacent edge or by a bichromatic four-edge path created several incidences away. Deleting a low-degree vertex and coloring the remaining graph therefore does not guarantee that the old coloring extends without recoloring. Explicit small configurations already witness failure of this zero-recoloring strategy while remaining globally six-colorable.
The known seven-color proof has one extra color available to break such interactions. Reaching six requires coordinating local recolorings or extracting stronger structure from a minimal counterexample. Finite searches can test configurations and produce certificates, but bounded verification alone cannot establish the universal quantifier over all finite graphs.
## Formalization scope
The mission uses `SimpleGraph` with an arbitrary finite vertex type. Edges are unordered edge-set elements, and palettes are the labeled finite types `Fin k`. The graph need not be connected, cubic, planar, or nonempty; isolated vertices and the empty graph are included. “Subcubic” means degree at most three, not degree exactly three.
A forbidden path is represented by five pairwise distinct vertices and four consecutive adjacencies. It is not required to be induced. A forbidden cycle is represented separately by four pairwise distinct vertices and four cyclic adjacencies. Under the properness hypothesis, equality of opposite edge colors is precisely the bichromatic alternating pattern.
A complete development should supply the known seven-color theorem, certify the exact value for $K_{3,3}$, and then address the six-color goal. Contributions formalizing faithful special cases or reusable extension lemmas are welcome, but sampled graph families and successful SAT searches remain finite evidence unless converted into a general Lean proof.
## Selected references
- Z. Dvořák, B. Mohar, and R. Šámal, *Star chromatic index*, Journal of Graph Theory 72 (2013), 313–326. [arXiv:1011.3376](https://arxiv.org/abs/1011.3376)
- H. Lei, Y. Shi, and Z.-X. Song, *Star chromatic index of subcubic multigraphs*, Journal of Graph Theory 88 (2018), 566–576. [arXiv:1701.04105](https://arxiv.org/abs/1701.04105)
- C. J. Casselgren, J. B. Granholm, and A. Raspaud, *On star edge colorings of bipartite and subcubic graphs*, Discrete Applied Mathematics 298 (2021), 21–33. [arXiv:1912.02467](https://arxiv.org/abs/1912.02467)
- Open Problem Garden, *Star chromatic index of subcubic graphs*, OPG-37271. [Problem page](https://www.openproblemgarden.org/comment/reply/37271)
- Vibe Mathing candidate repository, *OPG-37271 star chromatic index of subcubic graphs*, candidate-only artifacts at commit `ddc49c1978a196490702150bb75264793a658457`. [Repository](https://github.com/vibemathing/problem-opg-37271-star-chromatic-index-cubic/tree/ddc49c1978a196490702150bb75264793a658457)
Formalizing an 8-Vertex Candidate Counterexample to the Geodesic-Cycle Assignment Problem (OPG-500)Open Problem
[VM-STATUS-20260908-R05-PROVED]
> **Status update (2026-09-08):** The root theorem `OPG500Counterexample.eight_vertex_counterexample` is now **Proved** by an accepted Prove2Me submission. All six milestones are proved and the root has zero open leaves. The accepted proof has also been independently rebuilt with Lean 4.33.1 / Mathlib `0df444a360eaa60ab8c11dca51a86af692955474`. The historical text below describes the mission as it stood before formal closure.
---
## Motivation and historical context
Peripheral cycles occupy a distinguished place in structural graph theory. A cycle is peripheral when it is induced and does not separate the graph after its vertices are removed. Tutte proved in 1963 that the peripheral cycles of a finite 3-connected graph generate its binary cycle space. This theorem links a local, visibly embedded kind of cycle to the global algebraic structure of all cycles.
Weighted geodesic cycles provide a different generating family. Georgakopoulos and Sprüssel proved in 2009 that, for every finite graph with positive edge lengths, every cycle is a binary sum of weighted geodesic cycles whose lengths do not exceed the length of the original cycle. In the same paper they posed Problem 3: can the edges of every finite 3-connected graph be assigned positive lengths so that every weighted geodesic cycle is peripheral? A positive answer would recover Tutte's generation theorem through metric structure.
The present target tests the opposite possibility on one explicitly specified graph with eight vertices. A candidate argument and finite certificates are available in the frozen OPG-500 research repository, but those artifacts are explicitly marked `candidate_only`: they are neither a published counterexample nor a machine-checked resolution. The purpose of the formal target is to determine whether the proposed universal obstruction survives complete definition, proof, and statement-faithfulness checks.
## Setting
Let $G$ be a finite simple graph. A **positive edge-length assignment** is a function
$$
\ell:E(G)\longrightarrow \mathbb R
$$
such that $\ell(e)>0$ for every edge $e$. The length of a finite path or cycle is the sum of the lengths of its edges.
A simple cycle $C$ is **$\ell$-geodesic** when, for every pair of vertices $x,y$ on $C$, at least one of the two $x$–$y$ arcs of $C$ has length equal to the shortest-path distance between $x$ and $y$ in $G$. Equivalently, there is no $x$–$y$ path in $G$ whose length is strictly smaller than both $x$–$y$ arcs of $C$. The definition concerns vertices of the cycle and permits ties between shortest paths.
A simple cycle is **peripheral** when it is induced and deleting all of its vertices leaves a connected graph or the empty graph. This is vertex deletion, not edge deletion.
Fix the graph $H$ on vertices $0,1,\ldots,7$. The vertices $0,1,2,3$ induce $K_4$. For each $i\in\{0,1,2,3\}$, set $y_i=7-i$ and join $y_i$ to exactly the three core vertices other than $i$. The four vertices $y_i$ are pairwise nonadjacent. Thus the frozen edge set is
$$
\{01,02,03,04,05,06,12,13,14,15,17,23,24,26,27,35,36,37\}.
$$
The labels and edge set are part of the statement and are not interchangeable with earlier candidate labelings without an explicit isomorphism.
## Formalization targets
### Main target: the universal eight-vertex obstruction
Formalize the following statement for the fixed graph $H$:
$$
H\text{ is 3-connected}\quad\text{and}\quad
\forall\ell:E(H)\to\mathbb R_{>0},\;
\exists C,\; C\text{ is an $\ell$-geodesic simple cycle of $H$ and is not peripheral}.
$$
The existential cycle may depend on $\ell$. The universal quantifier includes all strictly positive real assignments, including assignments with tied shortest paths. This is the stable target; finite samples and rational specializations are subordinate checks rather than replacements for it.
### Supporting targets
The development should also formalize the finite weighted geodesic-cycle generation theorem of Georgakopoulos and Sprüssel, the exact 3-connectivity and peripheral-cycle classification of $H$, the required shortest-path and tight-subgraph statements, the finite cycle-space rank statements, and the finite minimum/descent principle used to select a cycle outside a closed binary span. These targets should remain separate declarations so that their assumptions and reuse boundaries are visible.
## Significance
A proof of the main target would give a negative answer to the finite problem by exhibiting a 3-connected graph for which no positive edge weighting can make all geodesic cycles peripheral. It would not contradict Tutte's theorem: peripheral cycles may still generate the cycle space even though they cannot be made to contain every geodesic cycle for any weighting. The distinction between these two generation mechanisms is part of the mathematical content.
A formal development would add more than a checked final sentence. It would provide reusable definitions for positively weighted finite graphs and vertex-geodesic cycles, a precise treatment of the two arcs between cycle vertices, explicit deletion semantics for peripheral cycles, and finite cycle-space infrastructure. It would also separate purely finite graph facts from statements quantified over arbitrary real weights. The candidate repository currently supplies finite enumeration and abstract Lean fragments, but no existing artifact checks this full dependency chain.
Until the complete main theorem is verified, the eight-vertex graph remains a candidate obstruction and the original problem remains unresolved by this development.
## Difficulty
The central difficulty is the universal quantification over real edge lengths. Testing many integer or rational vectors cannot cover it. Shortest paths need not be unique, so an argument that silently perturbs the weights or assumes unique geodesics can change which cycles are geodesic. Every strict and weak inequality must therefore agree with the source definition, including tie cases.
The graph is small but the semantic boundary is not. A formal cycle representation must expose the two cycle arcs for every vertex pair without admitting malformed or repeated-vertex objects. The peripheral predicate must combine inducedness with connectivity after vertex deletion and must classify all cycles, not only a selected family of triangles. Finally, finite cycle-space computations and rank inequalities must be connected to actual paths and weighted geodesicity; a propositional or enumerative certificate alone does not establish that bridge.
## Formalization scope
The Lean development will use `Fin 8` for the vertices of $H$ and a `SimpleGraph` representation for adjacency. Weights will be functions on the edge subtype, so values on nonedges cannot affect the theorem. All weights are real and strictly positive. Paths and cycles are finite and simple; arbitrary walks do not count as target witnesses. Geodesicity is vertex-based and includes tied shortest paths. Peripheral cycles use inducedness and vertex deletion, with a connected-or-empty remainder.
The main theorem must retain the quantifier order “for every weighting, there exists a cycle.” It may not be weakened to rational weights, finitely many tested assignments, nonnegative weights, one selected weighting, edge-geodesicity, or the assertion that only four named core triangles fail to be peripheral. Definitions must be sorry-free, and nontrivial mathematical claims must be theorem declarations with separately checked proofs.
Reusable contributions include finite weighted-path length, shortest-path attainment in finite positive graphs, the equivalence of the two geodesic formulations, cycle-arc APIs, vertex-deletion connectivity, binary edge-vector encodings, and finite descent outside a closed span. Graph-specific finite certificates are welcome only when their checker is represented in Lean or their conclusions are otherwise proved in the kernel.
## Selected references
- A. Georgakopoulos and P. Sprüssel, *Geodetic topological cycles in locally finite graphs*, Electronic Journal of Combinatorics 16 (2009), R144. Section 3.1, Theorem 3.1; Section 5, Problem 3. https://arxiv.org/abs/0911.3999v1
- Open Problem Garden, *Geodesic cycles and Tutte's Theorem*, problem statement and vertex-based definition. https://www.openproblemgarden.org/op/geodesic_cycles_and_tuttes_theorem
- W. T. Tutte, *How to draw a graph*, Proceedings of the London Mathematical Society 13 (1963), 743–768. Cited as reference [18] by Georgakopoulos and Sprüssel for peripheral-cycle generation.
- Vibe Mathing, frozen OPG-500 candidate repository at commit `a41fe59b4535851ea55f6e868e938b9aaf81e924`. https://github.com/vibemathing/problem-opg-500-geodesic-cycles/tree/a41fe59b4535851ea55f6e868e938b9aaf81e924
P3-Partitions of Cubic 3-Connected Graphs (OPG-46613)Open Problem
## Motivation
A **$P_3$-packing** in a graph is a collection of pairwise vertex-disjoint paths on three vertices. Determining the largest such packing is NP-hard even in restricted graph classes, so structural hypotheses that force an optimal packing are of independent interest in graph factor theory. The present question asks whether 3-vertex-connectivity and cubicity force the strongest possible packing whenever the vertex count permits a perfect partition.
A. Kelmans attributes the broader packing problem to 1984. In Problem 1.10 of [*Packing 3-vertex Paths in Cubic 3-connected Graphs*](https://arxiv.org/abs/0910.2766v2), the question is whether every cubic 3-connected graph $G$ satisfies $\lambda(G)=\lfloor |V(G)|/3\rfloor$. Theorem 3.1 of that paper proves that the divisible-order factor statement is equivalent to several apparently stronger deletion and prescribed-edge statements; it does not prove the open claim itself. [OPG-46613](https://www.unsolvedmath.com/problems/OPG-46613) records the divisible-order form targeted here.
A 2026 candidate analysis in the [Vibe Mathing problem repository](https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition) investigated a tempting sufficient route: find a perfect matching whose complementary 2-factor has every cycle length divisible by three. Candidate C01 explains why that condition would yield a $P_3$-factor. Candidate C02 gives an explicit proposed family $H_q$ of order $18+12q$ that has $P_3$-factors but is claimed not to satisfy the stronger matching condition. These candidate claims have computational and partial Lean checks, but no complete Lean kernel proof; they are milestones here, not declarations that the original problem or the candidate family has already been formally established.
## Setting
All graphs are finite and simple. A graph is **cubic** when every vertex has exactly three neighbors. It is **3-vertex-connected** here when it has at least four vertices and deleting any set of at most two vertices leaves a connected induced graph.
A **$P_3$-factor** is represented by a natural number $b$, together with a bijection
$$
\operatorname{Fin}(b)\times\operatorname{Fin}(3)\simeq V(G),
$$
such that, in every block, positions $0$ and $1$ are adjacent and positions $1$ and $2$ are adjacent. The path is not required to be induced: an ambient edge between positions $0$ and $2$ is allowed because the two selected path edges still form a copy of $P_3$.
A **2-factor** is a spanning 2-regular subgraph. It is called divisible when every one of its connected components has order divisible by three. A **divisible matching complement** is a perfect matching $M$ such that the relative complement $G\setminus M$ is a divisible 2-factor.
The explicit graph $H_q$ is defined on $\operatorname{Fin}(18+12q)$. Its first nine vertices form the fixed Petersen-minus-one-vertex brick from C02; the remaining vertices form the stated cycle-and-opposite-chord brick with three joining edges. The full adjacency relation is part of the Lean definition rather than an external data file.
## Formalization targets
### Main goal
For every finite simple graph $G$,
$$
\bigl(G\text{ cubic}\bigr)\land
\bigl(G\text{ 3-vertex-connected}\bigr)\land
3\mid |V(G)|
\quad\Longrightarrow\quad
G\text{ has a }P_3\text{-factor}.
$$
This is the OPG-46613 target. Cubicity forces the order to be even, so within this domain divisibility by three is equivalent to divisibility by six.
### Literature and route milestones
The mission also formalizes the $(z1)\Leftrightarrow(z8)$ part of Kelmans's Theorem 3.1: the divisible-order factor claim is equivalent to the assertion that deleting any specified 3-vertex path leaves a $P_3$-factor. Two route lemmas state that divisible 2-factors split into $P_3$-factors and that, in cubic graphs, divisible 2-factors are equivalent to divisible perfect-matching complements.
### Candidate boundary milestones
The C02 milestones ask first for the complete 18-vertex statement and then for the full family:
$$
\forall q\in\mathbb N,\quad
H_q\text{ is cubic and 3-vertex-connected, has a }P_3\text{-factor, and has no divisible matching complement}.
$$
This separates a sufficient method from the root conclusion. It is not a counterexample to OPG-46613 because every $H_q$ in the proposed family explicitly satisfies the desired $P_3$ conclusion.
## Significance
A proof of the main goal would settle the divisible-order form of a long-standing path-packing problem. Through Kelmans's equivalences it would also control several deletion and prescribed-edge variants for cubic 3-connected graphs. A disproof would require a graph satisfying all domain hypotheses but lacking a $P_3$-factor; the C02 family does not claim this.
Formalizing the candidate boundary is useful even before the root is resolved. It turns a route exclusion into a checkable theorem and prevents a search campaign from silently assuming that every relevant graph possesses a divisible complementary 2-factor. The definitions of noninduced $P_3$-factors, vertex connectivity by deletion, perfect matchings, 2-factors, and component-order divisibility are intended to be reusable in later graph-factor work.
## Difficulty
The perfect-matching route is attractive because the complement of a perfect matching in a cubic graph is 2-regular. The obstruction is that its cycles need not have lengths divisible by three. The C02 candidate family is designed to expose exactly that gap: a persistent 5-cycle is claimed to occur in every complementary 2-factor even though an unrelated $P_3$-factor exists. Consequently, proving the main theorem cannot simply assume that a favorable perfect matching always exists.
The formal difficulty is also semantic. Connectivity must mean vertex connectivity, the complement must be relative to $G$ on the same vertex set, component sizes must refer to the 2-factor rather than the ambient graph, and $P_3$ must remain noninduced. Weakening any of these points can create a materially different or vacuous theorem.
## Formalization scope
The development targets Lean 4.33.1 and Mathlib revision `0df444a360eaa60ab8c11dca51a86af692955474`. Graphs use `SimpleGraph` on finite vertex types. Degree is the cardinality of the actual neighbor subtype. Three-vertex-connectivity explicitly quantifies over all finite deletion sets of cardinality at most two and includes a four-vertex order guard.
The main theorem is universe-polymorphic and does not hard-code a finite graph enumeration. The $H_q$ family includes $q=0$. The factor structure uses a bijection, so disjointness and coverage cannot be discharged by duplicate or omitted vertices. Ambient chords do not invalidate a block, while both required consecutive adjacencies must be genuine graph edges. The candidate family statements remain open theorem goals ending in `sorry`; the shared definition module itself is sorry-free.
Welcome contributions include proofs of the model lemmas, the finite $H_0$ statement, the general C02 family, Kelmans's equivalence, or decompositions of the root theorem into faithful reusable lemmas. Numerical enumeration alone is supporting evidence and should not be presented as a kernel proof.
## Selected references
- A. Kelmans, *Packing 3-vertex Paths In Cubic 3-connected Graphs*, arXiv:0910.2766v2, 2011, Problem 1.10 (p. 3) and Theorem 3.1 (pp. 7–8). https://arxiv.org/abs/0910.2766v2
- UnsolvedMath, *OPG-46613: P3-partitions of cubic 3-connected graphs*. https://www.unsolvedmath.com/problems/OPG-46613
- Vibe Mathing, *C01: divisible-cycle implication and a 30-vertex obstruction*, fixed repository revision `14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a`. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c01/proof.md
- Vibe Mathing, *C02: an 18-vertex obstruction and an infinite family with P3-factors*, fixed repository revision `14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a`. https://github.com/vibemathing/problem-opg-46613-cubic-p3-partition/blob/14b8dc64ac2d89c98cf3a2bbb2fcba76ced0df6a/research/artifacts/candidates/opg46613-c02/proof.md
## Motivation
The Fourier series of a periodic function decomposes it into sinusoidal components, but the partial sums of that series need not converge to the function even when the function is continuous: du Bois-Reymond exhibited in 1873 a continuous $2\pi$-periodic function whose Fourier partial sums diverge at a point. Fejér's 1904 theorem repairs this failure by replacing the partial sums with their Cesàro (arithmetic) averages: for *every* continuous periodic function, these averages converge to the function, uniformly, with no smoothness hypothesis beyond continuity. This was the first universally valid summation method for Fourier series, and its underlying technique — averaging against a kernel whose mass concentrates at the origin — became the template for what is now called a good kernel or approximate identity, the basic device used throughout harmonic analysis (heat-kernel smoothing, Poisson summation, Fourier-inversion arguments) [Stein & Shakarchi, 2003].
**Timeline.**
- 1873 — du Bois-Reymond constructs a continuous $2\pi$-periodic function whose Fourier series diverges at a point, showing continuity alone cannot guarantee convergence of the partial sums themselves.
- 1904 — Fejér proves that the Cesàro means of the Fourier series of any continuous periodic function converge to it uniformly (Fejér, 1904).
- The good-kernel method Fejér introduced was later systematized as the general framework for approximate identities in harmonic analysis (Stein & Shakarchi, 2003, Ch. 2, §5).
## Setting
Let $f : \mathbb{R} \to \mathbb{C}$ be continuous and $2\pi$-periodic, i.e. $f(x + 2\pi) = f(x)$ for every $x \in \mathbb{R}$. Its $n$-th **Fourier coefficient**, for $n \in \mathbb{Z}$, is
$$\hat f(n) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta)\, e^{-in\theta}\, d\theta.$$
Its $N$-th **partial sum** is $S_N(f)(\theta) = \sum_{n=-N}^{N} \hat f(n)\, e^{in\theta}$, and its $N$-th **Cesàro (Fejér) mean** is the arithmetic average of the first $N+1$ partial sums,
$$\sigma_N(f)(\theta) = \frac{1}{N+1}\sum_{k=0}^{N} S_k(f)(\theta).$$
## Formalization targets
### Fejér's theorem
$$\sigma_N(f) \longrightarrow f \quad \text{uniformly on } \mathbb{R} \text{ as } N \to \infty.$$
This is the full 1904 statement: no restriction to pointwise convergence, and no extra regularity assumed on $f$ beyond continuity.
## Significance
**The result itself.** Fejér's theorem gives the first universally valid summation method for the Fourier series of a continuous function, closing the gap left open by pointwise convergence tests that need extra regularity. It also yields, essentially for free, a proof of the Weierstrass approximation theorem on the circle — the trigonometric polynomials $\sigma_N(f)$ are dense in the continuous $2\pi$-periodic functions under the uniform norm — and it is the historical prototype of the good-kernel/approximate-identity method underlying Poisson summation, heat-kernel smoothing, and $L^1$ Fourier-inversion arguments.
**Formalizing it.** Mathlib currently has no infrastructure for this at all. `Mathlib.Analysis.Fourier.AddCircle` defines Fourier coefficients on the circle and proves $L^2$ convergence (Parseval's identity, via the orthonormal Fourier basis), but it has no notion of a partial sum, no Dirichlet or Fejér kernel, and no pointwise or uniform convergence result for Fourier series of any kind. This mission builds that classical convergence theory — the Fejér kernel, its closed form and positivity, the good-kernel estimates, and the uniform convergence theorem itself — from first principles.
## Difficulty
The obvious first attempt is to bound $|\sigma_N(f)(\theta) - f(\theta)|$ termwise from the individual Fourier coefficients. This fails outright: a continuous function's Fourier coefficients need not be absolutely summable, which is exactly the mechanism behind du Bois-Reymond's divergence example. The real difficulty is representing $\sigma_N(f)$ as a convolution,
$$\sigma_N(f)(\theta) = \frac{1}{2\pi}\int_{-\pi}^{\pi} f(\theta - \varphi)\, F_N(\varphi)\, d\varphi,$$
against the Fejér kernel $F_N$, and then proving $F_N$ is a *good kernel*: nonnegative, integrating to $1$ over one period, and — the genuinely quantitative step — with its mass outside any fixed neighborhood of $0$ vanishing as $N \to \infty$. That last estimate needs the closed form
$$F_N(\theta) = \frac{1}{N+1}\left(\frac{\sin((N+1)\theta/2)}{\sin(\theta/2)}\right)^2,$$
which carries a removable singularity at $\theta = 0$ that must be handled carefully, together with a genuine decay estimate — via a lower bound on $|\sin(\theta/2)|$ — valid uniformly outside any fixed $\delta$-neighborhood of the origin.
## Formalization scope
$f$ is complex-valued, and only continuity together with exact $2\pi$-periodicity is assumed — no differentiability, no bounded variation, no realness. Uniform convergence is stated with Mathlib's `TendstoUniformly`. The period is fixed at $2\pi$, matching the classical circle-group convention, rather than a general $T > 0$; the $T$-periodic statement is a routine rescaling of this one and is not separately targeted here. One route to a trivializing formalization is worth ruling out explicitly: assuming any extra regularity on $f$ (differentiability, bounded variation, Lipschitz continuity) would let the uniform-convergence conclusion follow from the much easier Dirichlet-kernel estimates, and would no longer be Fejér's theorem — the entire content of the result is that continuity alone suffices.
The needed infrastructure is the four definitions above (Fourier coefficient, partial sum, Cesàro mean, Fejér kernel) and the milestone lemmas below, culminating in the goal. The Fejér kernel's closed form, positivity, and good-kernel estimates are reusable well beyond this mission: directly for a Lean proof of the Weierstrass approximation theorem on the circle, and for any future development that needs an explicit approximate identity on the circle group. Contributions are welcome at every milestone; the concentration estimate is the analytic heart of the mission and a natural place to start.
## Selected references
- L. Fejér, "Untersuchungen über Fouriersche Reihen," *Mathematische Annalen* 58 (1904), 51–69.
- E. M. Stein and R. Shakarchi, *Fourier Analysis: An Introduction*, Princeton Lectures in Analysis I, Princeton University Press, 2003, Chapter 2, §5 ("Good Kernels") and Theorem 5.2.
- Wikipedia, "Fejér's theorem." https://en.wikipedia.org/wiki/Fej%C3%A9r%27s_theorem
## Motivation: when pairwise square conditions limit a set
**Diophantine equations** ask for integer solutions to arithmetic equations. One family of questions starts with a set of positive integers and imposes the same condition on every pair: their product, increased by one, must be a square. The question is how many distinct integers can satisfy all those conditions together. It connects a simple definition with a global restriction on simultaneous integer solutions.
The paper [*There is no Diophantine quintuple*](https://arxiv.org/abs/1610.04020v2), by Bo He, Alain Togbé, and Volker Ziegler, resolves the nonexistence question for sets of five elements. This mission targets its headline result, Theorem 1 in Section 1. The mathematical theorem is proved in the paper; the remaining goal is a complete Lean proof of that result.
## Setting: positive integers and pairwise perfect squares
A **perfect square** is an integer of the form $r^2$ for a natural number $r$. A **Diophantine $m$-tuple** is a set of $m$ distinct positive integers such that the product of any two different members, plus one, is a perfect square. Here $m$ records the number of elements, not a bound on their sizes. A Diophantine quintuple would have exactly five members ([definition in Section 1](https://arxiv.org/html/1610.04020v2#S1)).
Write those five integers as $a_1,\ldots,a_5$. Positivity means $a_i>0$ for every index. Distinctness means $a_i\ne a_j$ whenever $i\ne j$. The square condition requires a possibly different square root for each pair. There is no requirement that the ten square roots coincide, be distinct, or satisfy an additional ordering condition.
The theorem concerns positive integers. Replacing them by rational numbers changes the question. Likewise, allowing zero changes the admissible objects, and allowing repeated entries ceases to represent a five-element set. These domain choices are explicit in the formal target.
## Formalization target: no Diophantine quintuple
The single goal is the following nonexistence statement:
$$
\nexists\,a_1,\ldots,a_5\in\mathbb Z_{>0}\quad
\left[
(\forall i\ne j,\ a_i\ne a_j)
\ \land\
(\forall\,1\le i<j\le5,\ \exists r_{ij}\in\mathbb N,\ a_i a_j+1=r_{ij}^{,2})
\right].
$$
This is [Theorem 1 of the paper](https://arxiv.org/abs/1610.04020v2). The mission's goal is the existing declaration [`no_diophantine_quintuple`](https://prove2.me/theorems/780bea2d-21a2-4653-82ae-842b3c4a1927).
The integers are unrestricted in size. The target does not fix the smallest entry, require a particular triple among the entries, or assume that an entry falls below a numerical search threshold. A proof must cover every quintuple satisfying the stated domain conditions.
## Significance: an exact obstruction to larger sets
The result rules out an entire class of simultaneous square equations. As an immediate consequence, any set of distinct positive integers satisfying the same pairwise condition has at most four elements: a larger set would contain five distinct members that inherit the condition. This consequence explains why the five-element statement also constrains larger configurations.
A completed formalization would supply a reusable theorem that can be invoked whenever five distinct positive integers and their pairwise square witnesses arise. It would turn the informal nonexistence claim into a checked contradiction from precisely those hypotheses. The published statement is currently open for a Lean proof; its successful compilation verifies that the statement is well formed, not that the theorem has been proved.
## Difficulty: the quantifier over all positive integers
Testing examples cannot establish this target by itself. Any computation with a fixed search limit addresses only a bounded collection, while the statement quantifies over all positive integers. A formal proof that uses a finite computation must also establish why the computation covers every possible case.
The conditions are simultaneous: each entry participates in four pairwise equations. Solving or excluding one isolated pair does not by itself settle whether all ten equations can hold together. The paper's [proof overview in Section 2](https://arxiv.org/html/1610.04020v2#S2) describes the arithmetic estimates and computational components behind its result. Formalizing those components entails checking their hypotheses and connecting their conclusions to the unrestricted goal.
## Formalization scope: five indexed natural numbers
The Lean declaration represents the entries by a function `a : Fin 5 → Nat`. It places the existence of that function under a negation and includes three conditions: every value is positive, different indices have different values, and every pair of different indices has a natural-number square witness.
The square condition is written for all unequal indices. This is equivalent to the usual condition for increasing pairs because multiplication is commutative. No increasing ordering of the five values is imposed. A development using sorted entries must justify its connection to this unrestricted indexed representation.
The root statement needs only Lean's core natural numbers, finite index type, arithmetic, and logic. It introduces no custom predicate whose meaning could hide additional assumptions. A complete proof may use Mathlib and reusable supporting results about integer arithmetic, squares, and the arithmetic tools required by the chosen argument. Supporting declarations should state their hypotheses explicitly and ultimately connect to this exact root theorem. Contributions establishing the known result, including an alternative rigorous proof, are within scope.
## Selected references
- Bo He, Alain Togbé, and Volker Ziegler, *There is no Diophantine quintuple*, arXiv preprint, 2016; revised 2018, arXiv:1610.04020v2. [Paper](https://arxiv.org/abs/1610.04020v2). The target is Section 1, Theorem 1; the definition precedes it, and Section 2 gives the proof overview.
Every Odd Number Greater Than 1 is the Sum of at Most Five PrimesResearch Paper
## Motivation
An additive question about the primes asks how many of them are needed to represent
every integer. **Shnirelman's constant** is the least $k$ such that every natural number
greater than $1$ is a sum of at most $k$ primes; that such a $k$ exists at all is
Shnirelman's theorem (1930). The even Goldbach conjecture would give $k = 3$, and is
close to equivalent to that claim, but Goldbach is open, so every bound on $k$ has come
from the circle method together with explicit numerical input.
The history is a sequence of shrinking bounds, each one effective and each one resting on
a numerical verification available at the time:
* **1937.** Vinogradov proves that every *sufficiently large* odd integer is a sum of
three primes, with no effective threshold
([Vinogradov's theorem](https://en.wikipedia.org/wiki/Vinogradov%27s_theorem)).
* **1956.** Borozdkin makes the threshold effective; later work reduces it, and Liu and
Wang bring it to $\exp(3100)$
([Liu–Wang, 2002](https://doi.org/10.4064/aa105-2-3)).
* **1995.** Ramaré proves that every even natural number is a sum of at most six primes,
giving Shnirelman's constant $k \le 7$
([Ramaré](http://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/)).
* **1995.** Kaniecki obtains "at most five primes" **under the Riemann hypothesis**
([Kaniecki](https://doi.org/10.4064/aa-72-4-361-374)).
* **2012.** Tao removes the hypothesis: every odd number greater than $1$ is a sum of at
most five primes, unconditionally, lowering Shnirelman's constant to $k \le 6$
([arXiv:1201.6656](https://arxiv.org/abs/1201.6656)). This mission's goal.
* **2013.** Helfgott proves the ternary Goldbach conjecture outright — every odd
$n > 5$ is a sum of three primes — which supersedes the statement above
([arXiv:1312.7748](https://arxiv.org/abs/1312.7748)). Neither result is formalized.
## Setting
For a real number $\theta$ write $e(\theta) = \exp(2\pi i\theta)$. The **von Mangoldt
function** $\Lambda(n)$ equals $\log p$ when $n = p^m$ is a prime power and $0$
otherwise; it is Mathlib's `ArithmeticFunction.vonMangoldt`.
The paper does not work with the sharp-cutoff exponential sum
$S(x,\alpha) = \sum_{n \le x} \Lambda(n)e(\alpha n)$ but with a **smoothed** variant. For
a piecewise smooth $\eta : \mathbb{R} \to \mathbb{C}$ and a modulus $q_0$, set
$$S_{\eta,q_0}(x,\alpha) \;:=\; \sum_{n} \Lambda(n)\,e(\alpha n)\,
\mathbf{1}_{(n,q_0)=1}\,\eta(n/x).$$
The modulus $q_0$ is a technical device: taking $q_0 = 2$ restricts the sum to odd $n$
and saves a factor of two in the explicit constants. Because of that restriction it is
$4\alpha$, not $\alpha$, that gets approximated by a rational $a/q$.
Two explicit cutoffs are fixed. The **Lipschitz cutoff**
$$\eta_0(t) := 4\big(\log 2 - |\log 2t|\big)_+$$
has unit mass and is supported on $[1/4, 1]$; it is chosen because it factorises the Type
II sums. The **$L^2$-normalised cutoff**
$$\eta_1(t) := \big(1 - 10\,\mathrm{dist}(t,[0.2,0.8])\big)_+$$
is supported on $[0.1,0.9]$ and symmetric, $\eta_1(1-t) = \eta_1(t)$.
Throughout, $O^*(Y)$ denotes a quantity of magnitude at most $Y$ — an explicit bound, not
an asymptotic one. Two numerical constants are fixed once and for all:
$T_0 := 3.29\times 10^9$ and $N_0 := 4\times 10^{14}$.
## Formalization targets
### Goal (Theorem 1.4)
$$\forall n \text{ odd},\ n > 1 \;\Longrightarrow\;
\exists\, p_1,\dots,p_k \text{ prime},\ k \le 5,\ n = p_1 + \cdots + p_k.$$
The goal fixes no constants and no thresholds, so no later improvement can invalidate it.
The milestone list is the paper's own attack path, in its numbering: the two numerical
verifications (Theorems 1.5, 1.6) and the short-interval prime bound (Theorem 8.1) that
together settle $n \le 8.7\times10^{36}$; the $L^2$ apparatus (Lemma 4.4, Proposition
4.10) and Vaughan-type identity (Lemma 4.11) feeding the minor-arc bound (Theorem 5.1)
and hence the main exponential sum estimate (Theorem 1.3); the major-arc analysis
(Proposition 7.2); and the circle-method core (Theorem 8.2).
## Significance
*The result itself.* Theorem 1.4 lowers Shnirelman's constant from $7$ to $6$ and removes
the Riemann hypothesis from Kaniecki's conditional "five primes". Its durable content,
however, is not the headline but the **explicit exponential sum estimate** of Theorem
1.3: a bound on $|S_{\eta_0,q_0}(x,\alpha)|$ with constants small enough to be useful for
$x$ between $10^{30}$ and $10^{1300}$, a range where the asymptotically superior estimates
of Vinogradov, Chen–Daboussi and Ramaré carry constants too large or too ineffective to
apply. That estimate is the reusable object; it has been improved since
([Helfgott–Platt](https://arxiv.org/abs/1305.3062)) but not superseded in method.
*Formalizing it.* Status honesty matters here. Theorem 1.4 is **closed mathematics**, and
as a *statement* it was superseded within a year by Helfgott's ternary Goldbach theorem,
which gives three primes for every odd $n > 5$ and hence five a fortiori. Neither Tao's
theorem nor Helfgott's is formalized anywhere, and this mission does not claim to be
attacking an open problem: the work is formalizing a known, fully explicit proof. That
proof happens to be an unusually good formalization target, because every constant in it
is written down.
The platform already hosts the surrounding infrastructure. The `CircleMethod` namespace
carries a large verified development of Hardy–Littlewood apparatus following Vaughan, and
the `ThreePrimes` namespace carries a machine-checked proof of Vinogradov's three primes
theorem conditional on Siegel–Walfisz. This mission sits directly downstream of both and
should import from them rather than rebuild.
## Difficulty
The obvious route — deduce five primes from three primes — fails on the range where it is
needed. Vinogradov's theorem is asymptotic, and the best effective threshold is
$\exp(3100)$; below it the theorem says nothing, and $\exp(3100)$ is far beyond any
possible exhaustive check. So the entire difficulty lives in the window
$8.7\times10^{36} \le x \le \exp(3100)$, which must be handled by a circle-method argument
carrying explicit constants at every step.
Within that window the specific obstruction is the minor arc
$T_0/x \ll \|\alpha\|_{\mathbb{R}/\mathbb{Z}} \ll 1/N_0$. A direct Plancherel bound on the
$L^2$ side costs a factor of $\log x$, which is more than the argument can afford;
Montgomery's uncertainty principle cuts the loss to roughly $2\log x/\log N_0$, and only a
large-sieve estimate on prime pairs brings it down to a bounded factor of $8$. On the
$L^\infty$ side, Theorem 1.3 must be non-trivial across the whole window, which is why the
refinements (1.10)–(1.12) for $q$ near $1$ and near $x$ exist at all. Neither bound alone
suffices; the proof closes only because both are pushed to explicit constants
simultaneously.
## Formalization scope
The goal is stated over $\mathbb{N}$ as a `Multiset ℕ` of cardinality at most $5$ whose
members are all `Nat.Prime` and whose `sum` is $n$. A multiset, not a list or a finset:
repetition is essential ($9 = 3+3+3$) and order is not. **"At most five" is not "exactly
five"** — $3$ is a sum of one prime and cannot be a sum of five, since the least sum of
five primes is $10$. A formalization asserting exactly five primes is false, not merely
weaker.
The goal admits no trivializing reading: the empty multiset has sum $0 \ne n$, and the
cardinality bound is on the multiset itself, so no prime can be counted with multiplicity
zero to evade it.
Everything else in the mission is stated with explicit constants and $O^*(\cdot)$ bounds
rather than asymptotic notation, matching the paper: $X = O^*(Y)$ becomes $\|X\| \le Y$
outright. Sums over $n$ are unrestricted sums against a compactly supported cutoff, not
sums over `Finset.range`. Real powers are `Real.rpow`. The two cutoffs $\eta_0,\eta_1$ and
the sum $S_{\eta,q_0}$ are published as mission definitions; solvers should use them
verbatim rather than re-deriving equivalent forms.
**Three of the milestones are honest dead weight for a solver to attempt directly, and are
listed so the dependency graph is truthful rather than because they are tractable.**
Theorem 1.5 (all zeroes of $\zeta$ up to height $3.29\times10^9$ lie on the critical line)
and Theorem 1.6 (every even number up to $4\times10^{14}$ is a sum of two primes) are
finite, decidable statements that Lean can express and that are true, but each represents a
verified computation of a scale no current proof assistant can replay — Theorem 1.6 alone
is $2\times10^{14}$ cases. Theorem 8.1 is quoted from Ramaré–Saouter and itself depends on
Theorem 1.5. They are leaves that will stay open; a solver's effort is far better spent on
the analytic milestones, and the circle-method core (Theorem 8.2) can be closed
independently of them.
A complete development additionally needs the smoothed Vaughan identity bookkeeping, the
large sieve in Siebert's form, the von Mangoldt explicit formula with a zero sum
(Proposition 7.1), and Bourgain's trick of taking one of the three summands of size $x/K$.
The exponential sum machinery is reusable well beyond this mission — it is the standard
input to every explicit Goldbach-type result. Contributions to any milestone are welcome
independently, and a formalization of Helfgott's theorem that closes the goal by a
different route would be an entirely acceptable solution.
## Selected references
- T. Tao, *Every odd number greater than 1 is the sum of at most five primes*,
Mathematics of Computation 83 (2014), 997–1038.
[arXiv:1201.6656](https://arxiv.org/abs/1201.6656)
- H. A. Helfgott, *The ternary Goldbach conjecture is true*, 2013.
[arXiv:1312.7748](https://arxiv.org/abs/1312.7748)
- H. A. Helfgott and D. Platt, *Numerical verification of the ternary Goldbach
conjecture up to $8.875\cdot10^{30}$*, 2013.
[arXiv:1305.3062](https://arxiv.org/abs/1305.3062)
- O. Ramaré, *On Shnirel'man's constant*, Ann. Scuola Norm. Sup. Pisa 22 (1995), 645–706.
[numdam](http://www.numdam.org/item/ASNSP_1995_4_22_4_645_0/)
- L. Kaniecki, *On Shnirelman's constant under the Riemann hypothesis*, Acta Arithmetica
72 (1995), 361–374. [doi:10.4064/aa-72-4-361-374](https://doi.org/10.4064/aa-72-4-361-374)
- J. Richstein, *Verifying the Goldbach conjecture up to $4\cdot10^{14}$*, Mathematics of
Computation 70 (2001), 1745–1749.
[doi:10.1090/S0025-5718-00-01290-4](https://doi.org/10.1090/S0025-5718-00-01290-4)
- O. Ramaré and Y. Saouter, *Short effective intervals containing primes*, Journal of
Number Theory 98 (2003), 10–33.
[doi:10.1016/S0022-314X(02)00029-X](https://doi.org/10.1016/S0022-314X(02)00029-X)
- M. C. Liu and T. Z. Wang, *On the Vinogradov bound in the three primes Goldbach
conjecture*, Acta Arithmetica 105 (2002), 133–175.
[doi:10.4064/aa105-2-3](https://doi.org/10.4064/aa105-2-3)
- H. L. Montgomery, *The analytic principle of the large sieve*, Bulletin of the AMS 84
(1978), 547–567. [doi:10.1090/S0002-9904-1978-14497-8](https://doi.org/10.1090/S0002-9904-1978-14497-8)
- R. C. Vaughan, *The Hardy–Littlewood Method*, 2nd ed., Cambridge University Press, 1997.
[doi:10.1017/CBO9780511470929](https://doi.org/10.1017/CBO9780511470929)
More Asymmetry Bound: omega < 2.37134Research Paper
## Motivation
The **matrix-multiplication exponent** measures how the arithmetic complexity of multiplying square matrices grows with the ir dimension. Known upper bounds come from constructing large independent matrix products inside tensor powers whose asymptotic rank is controlled. Improving the extraction, rather than finding a lower-rank starting tensor, has driven several recent advances.
Alman, Duan, Vassilevska Williams, Xu, Xu, and Zhou improve the combination-loss analysis by allowing all three variable directions to be treated differently. Their original fourth-power computation gives the bound $\omega<2.371339$. The mission targets the slightly weaker rational endpoint $2.37134$, keeping the historical result distinct from the later AlphaEvolve numerical improvement incorporated into the latest manuscript. [*More Asymmetry Yields Faster Matrix Multiplication*, version 2, SODA 2025](https://arxiv.org/abs/2404.16349v2).
## Setting
Fix an arbitrary field $K$. The **matrix-multiplication tensor** $\langle a,b,c\rangle_K$ represents multiplication of an $a\times b$ matrix by a $b\times c$ matrix. A tensor's rank is the least number of pure tensors summing to it. The existing Lean definition `matMulExp K` is the infimum of $\log R(\langle n,n,n\rangle_K)/\log n$ for integer dimensions $n\ge2$, with value $3$ at the excluded dimensions $0$ and $1$. This definition, and the existing equivalence with the Strassen-preorder exponent, remain unchanged.
The source tensor is the literal fourth power $T=CW_5^{\otimes4}$ of the **Coppersmith–Winograd tensor**. The public parenthesization is $(CW_5\otimes CW_5)\otimes(CW_5\otimes CW_5)$. Its asymptotic rank is at most $7^4=2401$. Its canonical coarse components are indexed by triples $(i,j,k)$ with $i+j+k=8$. This is the fourth-power, recursion-level-three specialization described in Section 7, not the eighth-power specialization used by the later optimization note. [More Asymmetry, Section 7](https://arxiv.org/abs/2404.16349v2).
A **complete split distribution** records frequencies of entire fine-grade words, rather than only the marginal split at the next recursion step. At level $\ell\ge1$, these words have length $2^{\ell-1}$ over the alphabet $\{0,1,2\}$. Three such distributions describe the X-, Y-, and Z-variable blocks. A restricted constituent power keeps only blocks approximately consistent with those distributions, in maximum-coordinate distance at most a specified $\varepsilon\ge0$. An **interface tensor** is a tensor product of these restricted constituent powers. The approximation tolerance and all three distributions are part of the interface. [More Asymmetry, Definitions 3.4–3.6 and 4.1](https://arxiv.org/abs/2404.16349v2).
## Formalization targets
The goal is the unconditional field-uniform statement
$$\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{237134}{100000}.$$
Its binders and exponent definition match the existing Schönhage and Stothers goals; only the declaration name and endpoint differ. No optimizer result, characteristic condition, distribution, or assumed value surplus is a hypothesis of the root.
The compact proposal has four milestones and the root, totaling five review items. The milestones concern literal fine-to-coarse source restrictions; the fourth-power rank budget; an actual strict six-symmetrized value surplus at the chosen parameter; and the conditional implication from that surplus to the exponent bound. Existing proved source and rank theorems are reused. The open surplus target contains the new complete-split extraction and exact numerical obligations, which are described separately in the proof outline rather than hidden in an opaque certificate definition.
The chosen internal parameter is $\tau_0=3952233/5000000$, so
$$2.371339<3\tau_0=2.3713398<2.37134.$$
The substantive value target is the existence of a real $V>2401$ such that the actual source has six-symmetrized $\tau_0$-value at least $V$ in the existing finite-witness semantics. The strict slack leaves room to translate limiting extraction rates into strict lower bases. Neither the existence of that surplus nor a completed exact numerical certificate is claimed at proposal time.
## Significance
This formalization would capture a new structural improvement, not a re-optimization of the same DWZ square data. Its distinguishing feature is sequentially obtaining the necessary ownership properties for X, then Y, then Z, while preserving more useful fine blocks. The resulting complete-split and interface-tensor theory is also the mathematical foundation for the later AlphaEvolve optimization. [More Asymmetry, Sections 2, 4–6](https://arxiv.org/abs/2404.16349v2); [Dupont et al., Section 2](https://arxiv.org/abs/2608.16884v1).
The known mathematical result is not an open conjecture. The open work is its machine-checked reconstruction. The earlier square and Stothers roots are marked Proved. The newer DWZ fourth-power root has an accepted reduction but remains Open. Its literal fourth source, rank budget, sixfold-symmetry bridge and entropy-certificate infrastructure can be reused independently of that unfinished endpoint. A proof of the numerical DWZ bound alone would not imply the smaller bound targeted here.
## Difficulty
The old hashing interface guarantees both coarse X- and Y-block uniqueness. The new method initially requires only coarse X-block uniqueness. Fine Y-block compatibility and usefulness must then establish the ownership needed for the subsequent Z-stage. Applying a theorem whose hypotheses already demand coarse Y uniqueness would discard the new method's essential advantage. Six coordinate permutations create six regions whose parameters and output interfaces must remain consistent. [More Asymmetry, Section 4.1 and Figure 1](https://arxiv.org/abs/2404.16349v2).
Removing incompatible fine blocks creates holes. The relevant repair theorem concerns holes in all three modes and a quantitative supply of broken interface copies. It cannot be replaced without proof by the older square-specific Z-only repair interface. The global and recursive stages also carry subexponential losses and approximation tolerances; their limiting order must be explicit. Numerical feasibility is a separate obligation: floating-point parameters and optimization success are not exact normalization, marginal, entropy, or logarithm proofs. [More Asymmetry, Theorem 4.2, Theorems 5.3 and 6.4, and Section 7](https://arxiv.org/abs/2404.16349v2).
## Formalization scope
The environment is pinned to Mathlib `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e` and Lean `v4.29.0-rc3`. The development reuses `TensorObj`, `MMObj`, restrictions, degenerations, tensor powers, existing tau-value predicates, and `matMulExp`. The root is uniform over arbitrary fields. Source relations remain target-first: a restriction of A from B is written `Restrict A B`. A collection of overlapping constituent restrictions must not be relabeled as an external direct sum.
Complete split distributions, simultaneous three-mode projections, interface tensors, region permutations, and explicit finite extraction maps form reusable infrastructure. Exact rational profiles require compatible lengths; approximate profiles require their stated tolerance and limiting argument. No constant-valued replacement for tensor value, vacuous witness hypothesis, or certificate that merely assumes the desired extraction is admissible.
The authors' released code and parameter archive is the provenance source for the original computation. Versioned archive and witness hashes belong to the companion source audit. The optimization program need not be formalized: an exact certificate checker must establish its own normalization, support, marginal and interval conditions. Contributions to complete-split interfaces, sequential ownership, three-mode repair, recursive extraction, entropy certificates, and finite source-to-exponent bridges all advance this mission.
## Selected references
- Josh Alman, Ran Duan, Virginia Vassilevska Williams, Yinzhan Xu, Zixuan Xu, and Renfei Zhou, *More Asymmetry Yields Faster Matrix Multiplication*, SODA 2025. [Pinned version 2](https://arxiv.org/abs/2404.16349v2).
- Authors' code and parameters for the original fourth-power bounds. [OSF release](https://osf.io/mw5ak/).
- Ran Duan, Hongxun Wu, and Renfei Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*, FOCS 2023. [Version 5](https://arxiv.org/abs/2210.10173v5).
- Emilien Dupont et al., *Improving the matrix multiplication exponent with modern optimization and AlphaEvolve*, 2026 preprint. [Version 1](https://arxiv.org/abs/2608.16884v1).
Duan–Wu–Zhou Fourth-Power Bound: omega < 2.37193Research Paper
## Motivation
The **matrix-multiplication exponent** measures how the arithmetic cost of multiplying square matrices grows with their dimension. An improvement in this exponent is relevant both to algebraic complexity and to algorithms whose running times depend on matrix multiplication. This mission formalizes a known improvement using the fourth power of the Coppersmith–Winograd tensor; it does not claim a new mathematical record.
Duan, Wu, and Zhou identify a loss that arises when constituent tensors are analyzed independently although some of their finer components can coexist inside a shared variable block. Their asymmetric-hashing method recovers part of this combination loss. The paper's headline result concerns the eighth power. Its separate fourth-power computation reports $2.371919$ in Table 3, printed page 78. The present target is the slightly weaker exact rational endpoint $2.37193$. [Duan–Wu–Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*](https://arxiv.org/abs/2210.10173v5).
## Setting
Fix an arbitrary field $K$. The **matrix-multiplication tensor** $\langle a,b,c\rangle_K$ encodes multiplication of an $a\times b$ matrix by a $b\times c$ matrix. Its tensor rank is the smallest number of pure tensors whose sum is that tensor. The existing Lean definition `matMulExp K` takes the infimum of $\log R(\langle n,n,n\rangle_K)/\log n$ over integers $n\ge2$, with the value $3$ at the two excluded small dimensions. This definition is reused without alteration.
A **restriction** applies a linear map separately to each of a tensor's three variable spaces. A **degeneration** allows polynomial families of such maps and takes an appropriate leading coefficient. The order of the Lean relation is target first: `Restrict A B` means that $A$ is obtained from $B$. A direct sum uses disjoint variable spaces; a collection of overlapping restrictions does not constitute a direct sum.
The **Coppersmith–Winograd tensor** $CW_q$ has border rank at most $q+2$. This mission fixes $q=5$ and uses the literal tensor $T=(CW_5\otimes CW_5)\otimes(CW_5\otimes CW_5)$, whose asymptotic-rank budget is $7^4=2401$. Its standard coordinate partition has 45 coarse components $T_{ijk}$ indexed by nonnegative integers $i+j+k=8$. Each coarse component consists of ordered products of square components, whose grades sum to $(i,j,k)$. [Duan–Wu–Zhou, Sections 3 and 6–8](https://arxiv.org/abs/2210.10173v5).
A **restricted-splitting value pair** consists of a lower value bound and a prescribed distribution on finer Z-variable blocks. In a tensor power, Z-blocks with the wrong empirical split distribution are removed before measuring value. Sixfold symmetrization, using all permutations of the three modes, is part of this definition. Keeping the scalar and discarding the prescribed distribution loses information required by the recursion. [Duan–Wu–Zhou, Definition 3.9, Equation (3), and Definition 8.1](https://arxiv.org/abs/2210.10173v5).
## Formalization targets
The goal is precisely
$$\forall K\;[\mathrm{Field}(K)],\qquad \operatorname{matMulExp}(K)<\frac{237193}{100000}.$$
It has the same field quantification and exponent definition as the completed Schönhage and Stothers goals. Only the name and rational endpoint change. No distribution, optimizer, characteristic restriction, or unproved value bound is a hypothesis of this goal.
The supporting targets concern the literal fourth-power source; prescribed-splitting component values; the recursive and global extraction inequalities of Equations (34) and (25); an exact certificate for the released fourth-power computation; and the value-to-exponent implication of Theorem 3.2. The proof outline distinguishes stable formal statements from source-level tasks whose complete Lean interfaces still require development. It does not turn an unspecified certificate into an assumption that the desired extraction exists.
The compact milestone list contains four precise statements: the literal fine-to-coarse product restriction; the fourth-power asymptotic-rank bound; existence of a strict six-symmetrized value surplus; and the conditional implication from that surplus to the goal. Together with the root, these are five review items. The first, second, and fourth milestones are marked Proved. The surplus remains Open. An accepted root reduction links the surplus to the proved capstone; it is a proof sketch, not a proof of the exponent bound. Recursive component extraction and exact numerical certification remain substantial work inside that open target.
The planned internal parameter is $\tau=790643/1000000$. Thus $3\tau=2.371929<2.37193$. The substantive value obligation is a strict surplus over $2401$ for the actual fourth-power source, with asymptotic losses absorbed by choosing strict lower rates. The exact certificate must establish this surplus; neither its existence nor its numerical slack is presently claimed as proved.
## Significance
The result would extend the formalized Stothers endpoint $2.3737$ to an asymmetric fourth-power bound. More importantly, it would provide restricted-splitting interfaces that can support subsequent higher-power and more-asymmetric analyses. The mathematical improvement is already established in the cited paper. The task here is to reconstruct its argument with machine-checked statements, concrete tensor maps, and exact numerical bounds.
The earlier square and Stothers mission roots are marked Proved. Reusable infrastructure includes polynomial degenerations, tensor powers, direct-sum value witnesses, hashing and hole-repair lemmas, the literal fourth-power grading, and the final exponent bridge. Two additional literal fourth-power support/restriction bridges and an additive entropy certificate with directed-log inputs are also marked Proved. These statuses do not imply that the new restricted-value recursion or numerical witness is already formalized.
## Difficulty
The central difficulty is retaining the correct dependence between each value bound and its prescribed split distribution. The released fourth-power data contains consumer-specific copies of square value pairs. Equal coarse grades do not justify identifying their chosen distributions. The 21 positive fourth-power components use the six-region recursion, whereas the 24 components with a zero coordinate require the boundary merging argument. [Duan–Wu–Zhou, Equation (34), Section 7.3, and released implementation](https://osf.io/dta6p/).
Global hashing must additionally control competitors with the same marginals, shared Z-blocks, missing fine blocks, and subexponential losses. An isolated restriction into each constituent is insufficient to establish a simultaneous extraction. Numerical optimization presents a separate issue: floating-point normalization and approximate maximum-entropy computations are not exact feasibility or entropy proofs. Exact marginal constraints, positivity domains, and directed error bounds must all be checked.
## Formalization scope
The environment is pinned to Mathlib `777aaa61dcd2a1258d2b4962dbe983ede4d23b2e` and Lean `v4.29.0-rc3`. The development reuses `TensorObj`, `MMObj`, `Degenerates`, `HasTauValueAtLeast`, the six-symmetrized value infrastructure, and `matMulExp`. All endpoint theorems remain uniform over arbitrary fields. Finite profiles use exact integer counts; rational distributions must have compatible unbounded lengths before an asymptotic statement is invoked. Real limiting rates are represented with explicit strict slack where the existing finite-witness predicate does not guarantee endpoint attainment.
No constant-valued replacement for tensor value, opaque witness carrying its desired conclusion, or external direct sum substituted for overlapping source blocks is admissible. New definitions must specify the actual coordinate projections and restrictions they represent. The authors' optimizer is used to find candidate data, not trusted as a proof oracle. Contributions to restricted-power semantics, consumer-specific square pairs, boundary merging, recursive extraction, exact entropy bounds, and source-to-exponent bridges are all directly relevant to the goal.
## Selected references
- Ran Duan, Hongxun Wu, and Renfei Zhou, *Faster Matrix Multiplication via Asymmetric Hashing*, FOCS 2023. [Full paper, version 5](https://arxiv.org/abs/2210.10173v5).
- Duan–Wu–Zhou, accompanying optimization and verification code, including `power4_dup_2.371919.mat`. [Authors' release](https://osf.io/dta6p/).
- A. M. Davie and A. J. Stothers, *Improved Bound for Complexity of Matrix Multiplication*, Proceedings of the Royal Society of Edinburgh Section A 143(2), 2013. [DOI](https://doi.org/10.1017/S0308210511001646).
- Arnold Schönhage, *Partial and Total Matrix Multiplication*, SIAM Journal on Computing 10(3), 1981. [DOI](https://doi.org/10.1137/0210032).
## Motivation
A **strongly regular graph** with parameters $(n,k,\lambda,\mu)$ is a finite simple graph on $n$ vertices in which every vertex has exactly $k$ neighbours, every pair of adjacent vertices has exactly $\lambda$ common neighbours, and every pair of non-adjacent vertices has exactly $\mu$ common neighbours. For most parameter tuples the elementary counting and integrality conditions already decide existence; the interesting cases are those that survive every known feasibility test and still resist construction. The tuple $(99,14,1,2)$ is the smallest such case in the family $\lambda = 1$, $\mu = 2$, and its existence has been open for more than fifty years. John Horton Conway offered \$1000 for a resolution, as one of five problems posed at the 2014 DIMACS conference on Challenges of Identifying Integer Sequences ([Conway, *Five \$1,000 Problems (Update 2017)*](https://oeis.org/A248380/a248380.pdf)).
Timeline of the problem and of what is known about it:
- **1969/1971** — the parameter set is raised by Norman Biggs in his Southampton lectures (*Finite Groups of Automorphisms*, LMS Lecture Note Series 6, p. 111).
- **1973** — Berlekamp, van Lint and Seidel construct a strongly regular graph with parameters $(243,22,1,2)$ as the coset graph of the perfect ternary Golay code, settling one of the five feasible parameter tuples in this family.
- **1975** — the existence question appears as Problem 7 (attributed to J. J. Seidel) in R. K. Guy's problem list, *The Geometry of Metric and Linear Spaces*, Springer LNM 490, pp. 237–238; Conway had worked on it by then.
- **1984** — H. A. Wilbrink, [*On the $(99,14,1,2)$ strongly regular graph*](https://research.tue.nl/files/2449333/256699.pdf), shows that such a graph cannot be vertex-transitive: no group of automorphisms can act transitively on its 99 vertices.
- **1988** — Brouwer and Neumaier, [*A remark on partial linear spaces of girth 5 with an application to strongly regular graphs*](https://ir.cwi.nl/pub/1721), Combinatorica 8, 57–61.
- **2004** — Makhnev and Minakova, *On automorphisms of strongly regular graphs with $\lambda=1$, $\mu=2$*, Discrete Math. Appl. 14(2), and **2011** — Behbahani and Lam, [*Strongly regular graphs with non-trivial automorphisms*](https://doi.org/10.1016/j.disc.2010.10.005), Discrete Math. 311, 132–144: further restrictions on the possible automorphism groups.
- **2014/2017** — Conway's prize offer publicises the problem.
No graph with these parameters has been found, and no non-existence proof is known.
## Setting
Fix a finite vertex set $V$ and a simple graph $g$ on $V$ (irreflexive, symmetric adjacency $\mathrm{Adj}$). For vertices $v,w$ write $N(v) = \{u : \mathrm{Adj}(v,u)\}$ for the neighbourhood of $v$ and $N(v)\cap N(w)$ for the set of common neighbours. The graph $g$ is **strongly regular with parameters $(n,k,\lambda,\mu)$**, written $\mathrm{IsSRGWith}\ g\ n\ k\ \lambda\ \mu$, when
- $|V| = n$;
- $|N(v)| = k$ for every vertex $v$;
- $|N(v)\cap N(w)| = \lambda$ whenever $v$ and $w$ are adjacent;
- $|N(v)\cap N(w)| = \mu$ whenever $v \neq w$ are non-adjacent.
The case $\lambda = 1$ says that every edge lies in exactly one triangle — equivalently, the neighbourhood of each vertex induces a perfect matching, so such graphs are **locally linear**. The case $\mu = 2$ says that every non-adjacent pair is the pair of opposite corners of exactly one $4$-cycle. Conway's problem asks for $(n,k) = (99,14)$ with these two local conditions.
Counting paths of length two from a fixed vertex gives $k(k-\lambda-1) = (n-k-1)\mu$, which for $\lambda=1$, $\mu=2$ reduces to $2n = k^2 + 2$; with $k = 14$ this yields $n = 99$. Writing $A$ for the adjacency matrix, $I$ for the identity and $J$ for the all-ones matrix, strong regularity is equivalent to the matrix identity $A^2 = kI + \lambda A + \mu(J - I - A)$, which for $(99,14,1,2)$ reads $A^2 + A = 12I + 2J$; the eigenvalues of $A$ other than $k=14$ are then $3$ and $-4$, and integrality of their multiplicities ($54$ and $44$) is one of the feasibility conditions that $(99,14,1,2)$ passes.
## Formalization targets
### Goal
$$\exists\ \alpha,\ \exists\ g \text{ a simple graph on } \alpha,\quad \mathrm{IsSRGWith}\ g\ 99\ 14\ 1\ 2 .$$
The goal is Mathlib's own `proof_wanted conway_99` in `Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean`, stated verbatim: existence of a finite type carrying a strongly regular graph with parameters $(99,14,1,2)$. A resolution in either direction is welcome — a proof settles the existence half, and a proof of the negation settles the non-existence half; the platform records the two as proof and disproof of the same statement.
### Supporting targets
$$2n = k^2 + 2, \qquad k \text{ even}, \qquad k \in \{2,4,14,22,112,994\}$$
for every strongly regular graph with $\lambda = 1$, $\mu = 2$: the counting identity, local linearity, and the integrality restriction that cuts the family down to five non-degenerate parameter tuples.
$$\exists\, g,\ \mathrm{IsSRGWith}\ g\ 9\ 4\ 1\ 2, \qquad \exists\, g,\ \mathrm{IsSRGWith}\ g\ 243\ 22\ 1\ 2$$
the two members of the family that are known to exist: the $3\times 3$ rook's graph (the Paley graph on $9$ vertices) and the Berlekamp–van Lint–Seidel graph.
$$|E(g)| = 693, \qquad |\{\text{triangles of } g\}| = 231, \qquad A^2 + A = 12I + 2J, \qquad g \text{ not vertex-transitive}$$
structural consequences for a hypothetical $99$-graph, the last one being Wilbrink's theorem.
## Significance
A $(99,14,1,2)$ graph, if it exists, is a locally linear graph of maximal density in its parameter range and a partial linear space of girth $5$ with $99$ points and $231$ lines of size $3$; its existence would also produce new association schemes and new examples for the general classification of strongly regular graphs. A non-existence proof would be the first case in this family ruled out by anything other than the classical feasibility conditions, and would say something new about how far local conditions ($\lambda=1$, $\mu=2$) constrain global structure.
Nothing in this mission is presently formalized. Mathlib defines `SimpleGraph.IsSRGWith`, proves the counting identity `IsSRGWith.param_eq`, the complement rule `IsSRGWith.compl`, and the matrix identity `IsSRGWith.matrix_eq`, and records the $99$-graph problem as a `proof_wanted`. The supporting targets are of three kinds: results that are proved in the literature and only need formalizing (existence at $(9,4,1,2)$ and $(243,22,1,2)$; Wilbrink's non-vertex-transitivity; the integrality restriction on $k$); routine consequences that supply reusable infrastructure (edge and triangle counts, the spectral identity, evenness of $k$); and the goal itself, which is open mathematics.
## Difficulty
The obvious approaches fail for concrete reasons. Exhaustive search is out of range: the graph has $693$ edges among $\binom{99}{2} = 4851$ pairs, and no isomorph-free generation of locally linear graphs on $99$ vertices is feasible. Algebraic constructions are blocked by Wilbrink's theorem — the graph cannot be vertex-transitive, so it is not a Cayley graph and cannot be produced by the group-theoretic constructions that yield most known strongly regular graphs, including the two that work at $(9,4,1,2)$ and $(243,22,1,2)$. On the non-existence side, every classical feasibility test (the counting identity, integrality of the eigenvalue multiplicities, the Krein conditions, the absolute bound) is passed by $(99,14,1,2)$, so a proof of non-existence needs an argument that does not factor through the parameters alone.
## Formalization scope
All statements are phrased with Mathlib's `SimpleGraph.IsSRGWith` on a `Fintype` vertex type with `DecidableRel` adjacency, and use `Fintype.card`, `SimpleGraph.edgeFinset`, `SimpleGraph.cliqueFinset 3` (triangles as $3$-cliques), `SimpleGraph.adjMatrix` over $\mathbb{Z}$, and graph isomorphisms `g ≃g g` for automorphisms. The goal quantifies over `α : Type` together with a `Fintype α` instance, so the vertex set is finite by construction and the empty type does not satisfy the cardinality clause; the statement is therefore not vacuously satisfiable. Note that Mathlib's definition constrains $\lambda$ only through pairs that are actually adjacent and $\mu$ only through pairs that are actually distinct and non-adjacent, so degenerate small graphs (the one-vertex graph, $K_3$) do satisfy `IsSRGWith` with $\lambda = 1$, $\mu = 2$; the supporting statements carry the cardinality hypotheses ($0 < n$, $1 < n$) that exclude them where needed, and the degenerate degree $k = 2$ is listed explicitly in the classification of feasible degrees.
Infrastructure a complete development needs, and which is reusable beyond this mission: interface lemmas for counting common neighbours in a strongly regular graph; the spectral theory of the adjacency matrix (multiplicities of the two non-principal eigenvalues, and their integrality), which is the missing ingredient for the classification of feasible degrees; a Lean construction of the perfect ternary Golay code and its coset graph, for the $(243,22,1,2)$ case; and decision procedures for strong regularity of an explicitly given small graph, for the $(9,4,1,2)$ case. Contributions to any of these are welcome, as are partial non-existence results (for instance, restrictions on automorphisms of prime order) submitted as separate statements.
## Selected references
- N. Biggs, *Finite Groups of Automorphisms: Course Given at the University of Southampton, October–December 1969*, London Mathematical Society Lecture Note Series 6, Cambridge University Press, 1971, p. 111.
- E. R. Berlekamp, J. H. van Lint, J. J. Seidel, *A strongly regular graph derived from the perfect ternary Golay code*, in: A Survey of Combinatorial Theory, North-Holland, 1973, pp. 25–30.
- R. K. Guy, *Problems*, in: The Geometry of Metric and Linear Spaces, Springer Lecture Notes in Mathematics 490, 1975, pp. 233–244 (Problem 7, J. J. Seidel, pp. 237–238). [doi:10.1007/BFb0081147](https://doi.org/10.1007/BFb0081147)
- H. A. Wilbrink, *On the $(99,14,1,2)$ strongly regular graph*, in: Papers dedicated to J. J. Seidel, EUT Report 84-WSK-03, Eindhoven University of Technology, 1984, pp. 342–355. [PDF](https://research.tue.nl/files/2449333/256699.pdf)
- A. E. Brouwer, A. Neumaier, *A remark on partial linear spaces of girth 5 with an application to strongly regular graphs*, Combinatorica 8 (1988), 57–61. [doi:10.1007/BF02122552](https://doi.org/10.1007/BF02122552)
- A. A. Makhnev, I. M. Minakova, *On automorphisms of strongly regular graphs with $\lambda=1$, $\mu=2$*, Discrete Mathematics and Applications 14 (2004), no. 2. [doi:10.1515/156939204872374](https://doi.org/10.1515/156939204872374)
- M. Behbahani, C. Lam, *Strongly regular graphs with non-trivial automorphisms*, Discrete Mathematics 311 (2011), 132–144. [doi:10.1016/j.disc.2010.10.005](https://doi.org/10.1016/j.disc.2010.10.005)
- J. H. Conway, *Five \$1,000 Problems (Update 2017)*, OEIS. [PDF](https://oeis.org/A248380/a248380.pdf)
Almost-Complex-to-Complex Conjecture in Real Dimension at Least SixOpen Problem
## Motivation
An **almost complex structure** gives every tangent space of a smooth manifold the linear algebra of a complex vector space, but it need not come from complex-valued coordinate charts. The gap between these two notions is a global differential-geometric question, not a change of terminology. Granja and Milivojević describe the following as “a major open problem in differential geometry”: whether every closed almost complex manifold of dimension at least six admits an integrable complex structure ([Introduction, p. 1](https://doi.org/10.3842/SIGMA.2022.093)). This mission records that question as an open conjecture, not as an established theorem.
### Timeline
- **1957:** Newlander and Nirenberg proved that an almost complex structure is integrable exactly when its Nijenhuis tensor vanishes, under the regularity assumptions in their theorem. This turns integrability into a nonlinear first-order differential condition rather than a consequence of the pointwise equation $J^2=-\mathrm{id}$ ([article](https://doi.org/10.2307/1970051)).
- **2014–2021:** Bryant’s account of Chern’s program still calls the existence of an integrable almost complex structure on $S^6$ open, while referring to the sphere’s well-known almost complex structure ([abstract](https://arxiv.org/abs/1405.3405)).
- **2022:** Granja and Milivojević state the broader closed-manifold question above and study the topology of spaces of almost complex structures on six-manifolds ([SIGMA article](https://sigma-journal.com/2022/093/)).
## Setting
Fix an integer $n\ge 3$. Let $M$ be a connected, compact, Hausdorff, second-countable smooth manifold without boundary and of **real dimension** $2n$. An almost complex structure on $M$ is a smooth field
$$
J_x:T_xM\longrightarrow T_xM
$$
of real-linear maps satisfying $J_x(J_xv)=-v$ for every $x\in M$ and $v\in T_xM$. This condition forces even real dimension, but by itself supplies no complex coordinate charts.
A **complex structure** of complex dimension $n$ is an atlas with values in $\mathbb C^n$ whose transition maps are complex differentiable. Such an atlas induces an integrable almost complex structure. The target concerns existence on the underlying smooth manifold: the complex structure obtained may induce a different almost complex structure from the supplied $J$. It does not claim that every chosen almost complex structure is integrable.
Here “closed” means compact and without boundary. Connectedness is explicit because it is part of the standing manifold convention in the cited 2022 source. The lower bound is on real dimension: $2n\ge 6$, equivalently $n\ge 3$.
## Formalization target
### Main open conjecture
For every $n\ge 3$ and every closed connected smooth real $2n$-manifold $M$,
$$
M\text{ admits a smooth almost complex structure}
\quad\Longrightarrow\quad
M\text{ admits a compatible complex atlas of complex dimension }n.
$$
“Compatible” means that the underlying real smooth structure of the complex atlas is smoothly equivalent to the given smooth structure on the same topological space. No claim of uniqueness, equality with the original atlas, or integrability of the supplied $J$ is made.
The real six-dimensional case is essential. Since $S^6$ carries an almost complex structure, the conjecture would imply that its underlying smooth manifold carries some complex structure. That special case remains unresolved; restricted nonexistence results, such as results imposing compatibility with a particular metric, do not decide the unrestricted existence question.
## Significance
A positive solution would replace a pointwise tangent-bundle reduction by genuine holomorphic coordinates for every manifold in the stated class. It would in particular settle the existence question for $S^6$. A negative solution would identify additional global obstructions to complex atlases that are invisible to the existence of an almost complex structure.
The formalization isolates a reusable smooth almost complex structure on top of Mathlib’s tangent-bundle and manifold APIs, while making the desired complex atlas explicit. This prevents the central distinction from being hidden inside an unconstrained predicate named “integrable.” It also exposes the compatibility between the original real smooth atlas and the real atlas underlying the complex charts, which future work on characteristic classes, Nijenhuis tensors, and concrete six-manifolds can reuse.
## Difficulty
The equation $J^2=-\mathrm{id}$ is fiberwise algebra. Integrability requires local complex coordinates whose overlaps are holomorphic, equivalently the vanishing condition identified by Newlander and Nirenberg. Smooth variation of $J$ does not make that differential condition automatic. Thus simply viewing each tangent space as a complex vector space does not construct a complex manifold.
The six-sphere shows why the dimension threshold cannot be treated as a routine stable-range simplification. Its known almost complex structure supplies the hypothesis in real dimension six, while no arbitrary complex atlas is known. Likewise, replacing the conclusion by a complex vector-space structure on each tangent fiber would merely repeat the hypothesis and would not address the open problem.
## Formalization scope
The namespace `AlmostComplexToComplex` uses Mathlib’s boundaryless Euclidean manifold model. `AlmostComplexStructure n M` contains a continuous real-linear map on every tangent space, the pointwise identity $J^2=-\mathrm{id}$, and smoothness of the induced self-map of the total tangent bundle. It contains no integrability field.
The main theorem assumes the real atlas is modeled on $\mathbb R^{2n}$ and concludes the existence of charts modeled on $\mathbb C^n$. Mathlib’s `IsManifold` condition over $\mathbb C$ at order one states complex differentiability of chart transitions. Two $C^\infty$ conditions on the identity map compare the original real atlas and the real manifold structure underlying the complex charts in both directions; an unrelated smooth structure therefore cannot satisfy the conclusion merely by being placed on the same carrier type.
This is a chart-level interface, not yet a development of analytic integrability theory. Mathlib at the pinned revision has no ready-made almost-complex/Nijenhuis package connecting the structure above to the Newlander–Nirenberg criterion. The target does not assert that the supplied $J$ is integrable or homotopic to the one induced by the resulting atlas. A dedicated $S^6$ milestone is also outside this minimal draft because faithfully constructing the standard sphere and its known almost complex structure would require additional sourced infrastructure; no surrogate special case is inserted.
## Selected references
- Gustavo Granja and Aleksandar Milivojević, *Topology of Almost Complex Structures on Six-Manifolds*, SIGMA 18 (2022), 093, Introduction, p. 1. [DOI](https://doi.org/10.3842/SIGMA.2022.093); [arXiv](https://arxiv.org/abs/2207.12946).
- August Newlander and Louis Nirenberg, *Complex Analytic Coordinates in Almost Complex Manifolds*, Annals of Mathematics 65 (1957), 391–404. [DOI](https://doi.org/10.2307/1970051).
- Robert L. Bryant, *S.-S. Chern’s Study of Almost-Complex Structures on the Six-Sphere*, arXiv:1405.3405v2 (2021 revision), abstract. [arXiv](https://arxiv.org/abs/1405.3405).
Smale's Ninth Problem: Strongly Polynomial Linear ProgrammingOpen Problem
## The problem of solving linear inequalities
The **linear feasibility problem** takes a matrix $A \in \mathbb{R}^{m\times n}$ and a vector $b \in \mathbb{R}^m$ and asks whether the system of $m$ linear inequalities in $n$ real unknowns
$$\{\,x \in \mathbb{R}^n \mid Ax \ge b\,\} \;\ne\; \emptyset$$
has a solution. By linear programming duality, optimizing a linear objective over such a set reduces to feasibility, so this decision problem carries the whole complexity of linear programming.
What "polynomial time" means here depends on the machine. In the **bit model** the input is a list of rational numbers, its size $L$ counts the bits of all numerators and denominators, and an algorithm is polynomial if it runs in time $\mathrm{poly}(m, n, L)$. In the **real-number model** the input is a list of $mn + m$ exact real numbers, each arithmetic operation ($+, -, \times, \div$), comparison, or memory move costs one unit, and a running time may only depend on $m$ and $n$. An algorithm polynomial in this second sense is what Smale asks for; the closely related bit-model notion — $\mathrm{poly}(m,n)$ arithmetic operations *and* polynomially bounded intermediate bit sizes — is called **strongly polynomial**. This mission fixes the real-number model precisely as a **Blum–Shub–Smale (BSS) machine** ([Blum–Shub–Smale 1989](https://doi.org/10.1090/S0273-0979-1989-15750-9)): a finite program of instructions acting on a bi-infinite tape $\mathbb{Z} \to \mathbb{R}$ of real registers — loads of arbitrary real machine constants, exact field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch, and accept/reject — with cost equal to the number of executed instructions. The convention that costs something: the program must be **uniform**, one finite instruction list serving every $m$, $n$, and every real instance. Uniformity is exactly what separates the question from point-location tricks available to non-uniform families of decision trees.
## Why it matters
For optimization, the question is the last gap in the complexity of its central problem. Linear programs with combinatorial structure already admit strongly polynomial algorithms — [Tardos (1986)](https://doi.org/10.1287/opre.34.2.250) solved every LP whose running time may depend on the entries of $A$ but not on $b$ or $c$, covering network flows and all $\{0,\pm1\}$-constraint problems — and a positive answer for general LP would extend that unification to the whole class, while explaining why simplex-type methods behave so well in practice ([Spielman–Teng 2004](https://doi.org/10.1145/990308.990310)).
For the theory of computation over the reals, the problem is a benchmark for what unit-cost exact arithmetic can do: it is Problem 9 on Smale's list of mathematical problems for the twenty-first century ([Smale 1998](https://doi.org/10.1007/BF03025291)), posed in the BSS model as the real-number analogue of the P-versus-NP style questions of that program, and it interacts with polyhedral combinatorics through the polynomial Hirsch conjecture: a polynomial bound on polytope diameters is a necessary condition for any polynomial pivot rule. A problem that calibrates both the practice of optimization and the foundations of real computation is a subject, not a special case.
## The question and what is known
$$\textbf{Question (Smale's 9th).}\quad \text{Is there a uniform BSS program deciding } \{x \mid Ax \ge b\} \ne \emptyset \text{ in } \mathrm{poly}(m,n) \text{ steps?}$$
The timeline splits into a negative branch (lower bounds against algorithm classes) and a positive branch (polynomial algorithms in weaker senses).
*Lower bounds.* [Klee–Minty (1972)](https://link.springer.com/rwe/10.1007/978-0-387-74759-0_339) constructed a deformed cube on which Dantzig's largest-coefficient simplex rule visits all $2^n$ vertices; analogous exponential examples were later found for essentially every deterministic pivot rule, and randomized rules were driven to subexponential lower bounds by [Friedmann–Hansen–Zwick (2011)](https://doi.org/10.1145/1993636.1993675) — against upper bounds of $\exp(O(\sqrt{n \log n}))$ from [Kalai (1992)](https://doi.org/10.1145/129712.129759) and [Matoušek–Sharir–Welzl (1996)](https://doi.org/10.1007/BF01940877). On the interior-point side, [Allamigeon–Benchimol–Gaubert–Joswig (2018)](https://doi.org/10.1137/17M1142132) showed by tropical methods that log-barrier path following is not strongly polynomial, and [Allamigeon–Gaubert–Vandame (2022)](https://arxiv.org/abs/2201.02186) extended this to **every** self-concordant barrier: no interior-point method of that class can settle the question positively.
*Polynomial algorithms in weaker senses.* [Khachiyan (1979/80)](https://doi.org/10.1016/0041-5553(80)90061-0) proved LP feasibility is polynomial in the bit model via the ellipsoid method; [Karmarkar (1984)](https://doi.org/10.1007/BF02579150) and then [Renegar (1988)](https://doi.org/10.1007/BF01580724) brought interior-point methods to $O(\sqrt{n}\,L)$ iterations. [Megiddo (1984)](https://doi.org/10.1145/2422.322418) solved LP in linear time for every fixed dimension; [Tardos (1986)](https://doi.org/10.1287/opre.34.2.250) gave the combinatorial strongly polynomial class; [Vavasis–Ye (1996)](https://doi.org/10.1007/BF02592148) and [Dadush–Huiberts–Natura–Végh (2020)](https://arxiv.org/abs/1912.06252) replaced the bit size by condition measures of $A$ alone; [Ye (2011)](https://doi.org/10.1287/moor.1110.0516) proved policy iteration strongly polynomial for fixed-discount Markov decision processes.
The central difficulty is visible in every positive result: each known iteration count is controlled by a *scale-dependent* quantity — bit length, condition number, barrier curvature — that is unbounded over the real instances with $m, n$ fixed. The naive plan, "run the ellipsoid method and round", fails at its first step in the real model: the number of iterations needed to separate a feasible system from an infeasible one grows with the thinness of the feasible set, which is not a function of $(m, n)$; no data-independent perturbation $\varepsilon$ exists when the data are arbitrary reals. All results above are proved on paper only; none has a machine-checked proof in the literature. What *is* already formalized, on this platform, is the substrate this mission builds on: the simplex iteration (mission *Introduction to Linear Optimization IV*), the ellipsoid method with its volume-halving correctness theorem (*XI*), interior-point path following (*XII*), and self-concordance with the barrier method (*Convex Optimization VI*).
## A hierarchy of formalization targets
The mission's milestone list realizes this hierarchy in order; each level states what it deliberately leaves open.
**Level 0 — the model works.** A uniform BSS program decides one-variable feasibility in linear time:
$$\exists\,P,\,C\ \ \forall m,\ \forall (a,b) \in \mathbb{R}^m \times \mathbb{R}^m:\ P \text{ decides } \{x \in \mathbb{R} \mid a_i x \ge b_i\ \forall i\} \ne \emptyset \text{ within } C(m{+}1) \text{ steps}.$$
It fixes nothing about $n \ge 2$; its role is to certify that the machine model and cost semantics of the goal are non-vacuous.
**Level 1 — the classical method is exponential.** On the Klee–Minty cube, Dantzig's rule admits a run of
$$2^n - 1 \text{ pivots}$$
from the all-slack basis to the optimum. It leaves open all other pivot rules — extensions to further rules are welcome as strengthenings.
**Level 2 — the bit model succeeds.** Through the Cramer–Hadamard solution bound $|x_j| \le n!\,U^n$ and the perturbation estimates, Khachiyan's theorem: for integer data bounded by $U$, every admissible ellipsoid run decides feasibility within
$$t^* \le 10^6\,(n{+}2)^4(\log_2 U + n + 2) \text{ iterations}.$$
The generous constants are deliberate — only the polynomial order is load-bearing. This level leaves open exactly the dependence on $\log U$.
**Level 3 — the goal (open).** A uniform program with data-independent polynomial cost:
$$\exists\,P,\,C,\,d\ \ \forall m, n, A, b:\ P \text{ decides } \{x \mid Ax \ge b\} \ne \emptyset \text{ within } C\,(mn + m + 2)^d \text{ steps}.$$
The statement asserts only the shape of the truth — no hard-coded degree or constant — so it is stable under every future quantitative improvement. These levels do not exhaust the project: Tardos' combinatorial LP theorem, Ye's fixed-discount MDP result, and impossibility statements for restricted program classes in the style of Allamigeon–Gaubert–Vandame are natural later milestones.
## Formalization scope
Polyhedra, simplex states, pivots, and ellipsoid runs are the platform's existing `LinearOptimization` development over `Matrix (Fin m) (Fin n) ℝ`, with $\{x \mid Ax \ge b\}$ as `polyhedron A b`; algorithms with data-dependent iteration counts are formalized as run predicates, as in the parent missions. The new `SmaleNinth` definitions supply what the goal genuinely needs and the run-predicate style cannot express: a concrete inductive type of BSS programs with operational semantics and unit-cost accounting, the Klee–Minty data with Dantzig's rule, and the explicit Khachiyan constants. One convention closes the degenerate escape hatch: the goal quantifies over finite `BSSProgram` terms under the fixed `encodeLP` input convention — formalizing "algorithm" as an arbitrary function $\mathbb{R}^{mn+m} \to \mathrm{Bool}$ would make the statement trivially true and is not the theorem. Division is totalized as $x/0 = 0$ and the branch test is $x_i \le 0$; both are benign for the class of programs quantified over.
The machine module is infrastructure beyond this mission — any real-number complexity statement (other Smale problems, sums-of-square-roots, BSS-completeness) can reuse it, as can any pivot-rule lower bound reuse the Klee–Minty module. Formalization forces distinctions the literature leaves informal: which machine variant carries the unit-cost claim, how ties in Dantzig's rule are resolved, and which of the interchangeable Khachiyan constants each estimate actually needs. Welcome contributions include proofs of any milestone, alternative exponential instances for other pivot rules, sharper constants in the Khachiyan module, and ports of the known strongly polynomial special cases.
## Selected references
- L. Blum, M. Shub, S. Smale, *On a theory of computation and complexity over the real numbers*, Bull. AMS 21(1):1–46, 1989. [DOI](https://doi.org/10.1090/S0273-0979-1989-15750-9)
- S. Smale, *Mathematical problems for the next century*, Math. Intelligencer 20(2):7–15, 1998. [DOI](https://doi.org/10.1007/BF03025291)
- V. Klee, G. J. Minty, *How good is the simplex algorithm?*, in Inequalities III, Academic Press, 1972, pp. 159–175.
- L. G. Khachiyan, *Polynomial algorithms in linear programming*, USSR Comput. Math. Math. Phys. 20:53–72, 1980. [DOI](https://doi.org/10.1016/0041-5553(80)90061-0)
- N. Karmarkar, *A new polynomial-time algorithm for linear programming*, Combinatorica 4:373–395, 1984. [DOI](https://doi.org/10.1007/BF02579150)
- J. Renegar, *A polynomial-time algorithm, based on Newton's method, for linear programming*, Math. Programming 40:59–93, 1988. [DOI](https://doi.org/10.1007/BF01580724)
- É. Tardos, *A strongly polynomial algorithm to solve combinatorial linear programs*, Oper. Res. 34(2):250–256, 1986. [DOI](https://doi.org/10.1287/opre.34.2.250)
- N. Megiddo, *Linear programming in linear time when the dimension is fixed*, J. ACM 31(1):114–127, 1984. [DOI](https://doi.org/10.1145/2422.322418)
- G. Kalai, *A subexponential randomized simplex algorithm*, STOC 1992. [DOI](https://doi.org/10.1145/129712.129759)
- O. Friedmann, T. D. Hansen, U. Zwick, *Subexponential lower bounds for randomized pivoting rules for the simplex algorithm*, STOC 2011. [DOI](https://doi.org/10.1145/1993636.1993675)
- D. A. Spielman, S.-H. Teng, *Smoothed analysis of algorithms: why the simplex algorithm usually takes polynomial time*, J. ACM 51(3):385–463, 2004. [DOI](https://doi.org/10.1145/990308.990310)
- S. A. Vavasis, Y. Ye, *A primal-dual interior point method whose running time depends only on the constraint matrix*, Math. Programming 74:79–120, 1996. [DOI](https://doi.org/10.1007/BF02592148)
- Y. Ye, *The simplex and policy-iteration methods are strongly polynomial for the Markov decision problem with a fixed discount rate*, Math. Oper. Res. 36(4):593–603, 2011. [DOI](https://doi.org/10.1287/moor.1110.0516)
- X. Allamigeon, P. Benchimol, S. Gaubert, M. Joswig, *Log-barrier interior point methods are not strongly polynomial*, SIAM J. Appl. Algebra Geom. 2(1):140–178, 2018. [DOI](https://doi.org/10.1137/17M1142132)
- X. Allamigeon, S. Gaubert, N. Vandame, *No self-concordant barrier interior point method is strongly polynomial*, STOC 2022. [arXiv](https://arxiv.org/abs/2201.02186)
- D. Dadush, S. Huiberts, B. Natura, L. A. Végh, *A scaling-invariant algorithm for linear programming whose running time depends only on the constraint matrix*, STOC 2020. [arXiv](https://arxiv.org/abs/1912.06252)
- D. Bertsimas, J. N. Tsitsiklis, *Introduction to Linear Optimization*, Athena Scientific, 1997 (Chapters 3, 8, 9 — formalized in the *Introduction to Linear Optimization* mission series).
- B. Korte, J. Vygen, *Combinatorial Optimization: Theory and Algorithms*, 6th ed., Springer, 2018, §4.1–4.5.
Coherent Measures of Risk: the axioms, and why Value-at-Risk fails themResearch Paper
## Motivation
In 1999 Artzner, Delbaen, Eber and Heath asked what a *risk measure* ought to satisfy, wrote
down four axioms, and observed that the industry standard of the day -- Value-at-Risk -- fails
one of them. The failing axiom is subadditivity: merging two positions should never require more
capital than holding them apart. VaR can violate it, so under VaR a diversified book can appear
riskier than its parts.
That observation did not stay academic. It is the reason the Basel framework moved its market-risk
capital standard from Value-at-Risk to Expected Shortfall. Few results in mathematical finance
have had a more direct regulatory consequence, and the mathematics is elementary enough to state
completely.
## Setting
A position is a payoff `X : Fin (n+1) -> R` across finitely many equally-weighted states, and a
risk measure `rho` sends it to the capital that must be added to make it acceptable. Following
Definition 2.4 of the paper, `rho` is **coherent** when it is translation-invariant, subadditive,
positively homogeneous and monotone. Nonemptiness of the state space is carried in the index type
so the worst case is always attained; no probability measure is needed for these four axioms,
which is faithful to the paper -- Artzner et al. state T, S, PH and M without reference to one.
Value-at-Risk is defined here at an integer tolerance `k` rather than a probability level, which
keeps the quantile unambiguous on a finite space: `VaR X k` is the least capital leaving at most
`k` states in loss, corresponding to level `k/(n+1)`.
## The goal
The mission's goal theorem is the negative result: **Value-at-Risk is not subadditive.** A witness
is 25 equiprobable states with `X` losing 100 in state 0 alone and `Y` losing 100 in state 1
alone. Each has one losing state in twenty-five, so at tolerance `k = 1` both have `VaR = 0`;
their sum loses in two states, exceeding the tolerance, so `VaR (X+Y) 1 = 100 > 0 + 0`. The
witness was checked numerically before this mission was drafted; what is open is the Lean proof.
The milestones establish the positive contrast on the same footing: worst-case risk, the most
conservative measure, satisfies all four axioms, so the failure is specific to VaR rather than
inherent to risk measurement.
## Source
P. Artzner, F. Delbaen, J.-M. Eber and D. Heath, *Coherent Measures of Risk*, Mathematical
Finance **9** (1999) 203-228. Axioms T, S, PH and M are Definition 2.4; the failure of
subadditivity for VaR and the diversification consequence are discussed in Section 3.
Kelly's Criterion: the optimal fraction for an even-money betResearch Paper
## Motivation
In 1956 Kelly answered a question that looks like gambling and is really about information: if
a channel gives you a noisy advance signal about a sequence of bets, how much is that signal
worth? His answer was that the maximum exponential rate of growth of a gambler's capital equals
the rate of transmission over the channel -- so information rate and capital growth rate are
the same quantity in different units. The betting fraction that achieves it is now called the
Kelly criterion, and it is the basis of a large practical literature on position sizing.
The result is short, entirely explicit, and has no analytic subtleties -- which makes it a good
formalization target and a surprising gap: the platform currently has fifteen missions on bandit
algorithms and none on optimal growth.
## Setting
This mission formalizes the *simplest case* of Kelly's Section 4: an even-money bet with no
track take, won independently with probability `p` and lost with probability `q = 1 - p`. A
gambler stakes a fixed fraction `l` of current wealth on each bet, so wealth is multiplied by
`1 + l` on a win and `1 - l` on a loss. The exponential rate of growth is
$$G(l) = p \log(1+l) + q \log(1-l).$$
Kelly shows this is maximised at `l = p - q`, with maximum value `1 + p log p + q log q` in
bits. We state `G` in nats (natural logarithm), so the maximum carries an additive `log 2`;
dividing by `log 2` recovers Kelly's bit-valued form, which is exactly `1 - H(p)` for the
binary entropy `H`. The maximiser is unaffected by the choice of base.
## What is being asked
The goal theorem is that `l = 2p - 1` maximises `G` over the admissible range `(-1, 1)` when
the bet is favourable (`p > 1/2`). Milestones supply the maximum value (Kelly's
information-rate identity), the admissibility of the maximiser, and the concavity that makes
the first-order condition sufficient.
## Source
J. L. Kelly Jr., *A New Interpretation of Information Rate*, Bell System Technical Journal
**35** (1956) 917-926, Section 4 ("the simplest case"). The growth-rate expression and the
maximiser `l = p - q` are stated there; the maximum value in bits is Kelly's eq. for `G_max`.
The identity and maximiser were checked numerically before drafting: for p = 0.55, 0.6, 0.7,
0.9 the claimed maximum matches `log 2 + p log p + q log q` to six decimals, and a grid search
over `(-1, 1)` at 1e-5 resolution returns `2p - 1` in every case.
Smooth 4-dimensional Poincaré conjecture: foundations and reductionsOpen Problem
## Motivation
The **smooth four-dimensional Poincaré conjecture** asks whether a smooth manifold with the topology of the four-sphere must also have its standard smooth structure, up to diffeomorphism. The distinction is between the existence of continuous coordinates and the compatibility of differentiable coordinates. The mission concerns this precise sphere question, listed as open in Problem 4.1 of *K3 — A New Problem List in Low-Dimensional Topology*. It does not treat a collection of algebraic obstructions as an existing proof of the conjecture. [Baykur–Kirby–Ruberman, Problem 4.1](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf)
### Historical landmarks
- **1961:** Smale proved that a closed smooth manifold homotopy equivalent to a sphere of dimension at least five is homeomorphic to that sphere. This is not a theorem that all such smooth manifolds are diffeomorphic to the standard sphere. [Smale, Theorem A](https://www.math.uchicago.edu/~shmuel/tom-readings/Smale,%20PC.pdf)
- **1982:** Freedman established the topological four-dimensional Poincaré theorem: a topological four-manifold homotopy equivalent to the four-sphere is homeomorphic to it. [Freedman, Theorem 1.6](https://www.maths.gla.ac.uk/~mpowell/1982_The%20topology%20of%20four-dimensional%20manifolds.pdf)
- **2026:** The *K3* problem list continues to distinguish this established topological result from the open smooth sphere problem. [Problem 4.1, pp. 191–192](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf)
## Setting
Let $S^4$ be the unit sphere in $ℝ^5$, with its standard stereographic smooth structure. A **homeomorphism** is a continuous bijection with continuous inverse; a **diffeomorphism** is a smooth bijection with smooth inverse. A **smooth atlas** is a collection of local Euclidean coordinates whose transition maps are smooth.
The manifold $M$ is compact and Hausdorff, has no boundary, and is equipped with a specified smooth atlas modeled on $ℝ^4$. The given atlas is arbitrary: it is not defined by transporting the standard structure from $S^4$.
For a homeomorphism $e:N\to S^4$, let $\mathcal A_e$ denote the atlas transported from the standard sphere along $e$. A **structomorphism** for the smooth structure groupoid is a homeomorphism whose coordinate expressions belong to that groupoid. The predicate $\mathsf{SPC4Pullback}$ requires, for every given smooth atlas $\mathcal A$ on such an $N$ and every such $e$, a structomorphism between $(N,\mathcal A)$ and $(N,\mathcal A_e)$. It does not require that structomorphism to be the identity. These are the conventions of the source definitions, not additional uniqueness assumptions. [Shin, *SPC4.lean*, lines 53–81 and 211–221]
## Formalization targets
### Main open goal
For every manifold $M$ with the preceding hypotheses, the goal is
$$
M\cong_{\mathrm{Top}}S^4
\quad\Longrightarrow\quad
M\cong_{\mathrm{Diff}}S^4.
$$
This is the source predicate $\mathsf{SPC4}$. Its conclusion asserts the existence of a diffeomorphism; it does not assert that a particular supplied homeomorphism is smooth.
### Structural and literature milestones
The atlas formulation has the exact equivalence
$$
\mathsf{SPC4}\quad\Longleftrightarrow\quad\mathsf{SPC4Pullback}.
$$
The source supplies a proof of this equivalence without invoking Freedman's theorem or assuming the conjecture as an unconditional fact. It is a reformulation, not a solution. Its foundations include the correspondence
$$
\operatorname{Structomorph}(\mathcal G^{\infty},M,N)
\simeq \operatorname{Diff}^{\infty}(M,N),
$$
where $\mathcal G^{\infty}$ is the smooth coordinate-change groupoid for the common model. [Shin, *SPC4.lean*, lines 334–365; *Bridge.lean*]
Write $F_4$ for the following compact Hausdorff, boundaryless instance of Freedman's topological theorem:
$$
M\simeq S^4\quad\Longrightarrow\quad M\cong_{\mathrm{Top}}S^4,
$$
where $\simeq$ denotes homotopy equivalence and only topological manifold charts are assumed. This is established mathematics, but a proof in the present formal development remains a target. If $\mathsf{SPC4Homotopy}$ denotes the analogous smooth conclusion from a homotopy equivalence, the relation to the main goal is recorded with its hypothesis visible:
$$
F_4\quad\Longrightarrow\quad
(\mathsf{SPC4}\Longleftrightarrow\mathsf{SPC4Homotopy}).
$$
Explicit standard-disk foundations form another track. For every $m\geq0$, they concern the manifold-with-boundary structure on $\overline B^{m+1}$, its boundary set $S^m$, and the smooth collar
$$
c:S^m\times[0,1]\longrightarrow\overline B^{m+1},
\qquad c(u,t)=(1-t/2)u.
$$
The collar is a closed embedding, has image
$$
\{z\in\overline B^{m+1}:\|z\|\geq1/2\},
$$
and satisfies $c(u,0)=u$, using the boundary inclusion. Its image is a neighborhood of every boundary point in the disk. A companion interface characterizes a $C^k$ map from a $C^k$ manifold with corners into the disk as precisely a continuous map whose inclusion into Euclidean space is $C^k$. These targets concern the actual disk smooth structure. [Shin, *Disk.lean*, lines 1076–1141 and 1263–1318]
### Topological two-disk gluing
For each integer $m\geq0$, let $D^{m+1}=\overline B^{m+1}$ be the closed unit disk in $\mathbb R^{m+1}$ and let $\varphi:S^m\to S^m$ be any homeomorphism of its boundary. The **twisted double** identifies the boundary point $u$ in a left copy of the disk with $\varphi(u)$ in a right copy. With the quotient topology, the target is
$$
X_\varphi:=\bigl(D^{m+1}_L\sqcup D^{m+1}_R\bigr)/(u_L\sim\varphi(u)_R)
\quad\cong_{\mathrm{Top}}\quad S^{m+1}.
$$
This statement is published as [SP4Gluing.twistedSphere_homeomorphic](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c). The theorem and its supporting [continuity](https://prove2.me/theorems/e09b0118-b3a4-44e3-9ba2-e70fb31a2faa) and [injectivity](https://prove2.me/theorems/12c0403c-fdcf-4202-8b53-9f12893b568f) lemmas have accepted Lean proofs contributed by [carlok](https://prove2.me/users/fca9fd8a-84f4-46ca-8845-a4a2b665381d). All three accepted proofs have also been checked locally with their proved dependencies. It concerns these explicit topological quotients, not arbitrary homotopy spheres or a prescribed smooth structure.
### Seam–interior smooth compatibility
For every regional chart base point, the open-bicollar and left-interior transitions are smooth in both directions. Right-interior-to-seam smoothness requires smooth $\varphi^{-1}$; the reverse requires smooth $\varphi$. The [single compatibility target](https://prove2.me/theorems/f1e93fb9-c414-46aa-8b6c-fc6978243ee7) concerns exact overlap sources, combining four source results internally. It provides neither a global smooth-manifold instance nor smooth standardness. [Shin, *Hemisphere.lean*, lines 2439–3577]
## Significance
A proof of the main goal would identify every smooth structure in its stated sphere class with the standard one, up to diffeomorphism. A proof of the transported-atlas equivalence instead locates the same unresolved comparison in a different formal language. The distinction matters: constructing a smooth structure by transport is not the same as identifying an arbitrary pre-existing one.
The bridge, explicit disk atlas, and stated collar properties have accepted kernel-checked Lean proofs. The clean atlas equivalence also has a proof with no admitted theorem among its axioms. The conjecture remains open, and Freedman's topological theorem remains unproved in this formal development despite its published mathematical proof.
The [topological two-disk gluing result](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c) identifies the homeomorphism type of these quotients for every boundary homeomorphism and every disk dimension at least one. The accepted formalization supplies a global topological comparison for this explicit quotient. It does not resolve the comparison with a prescribed smooth structure or recognition of general smooth four-manifolds.
Four supporting algebraic tracks concern orbit coinvariants, homology dimension budgets, finite-support shift rigidity, and Laurent-polynomial positivity. Their source results arose in route-specific obstruction studies. As of 6 September 2026, all eleven theorem targets in these algebraic tracks have accepted Lean proofs. The five additional formal proofs were contributed by [wamlart](https://prove2.me/users/70d2064f-6b47-4a3f-bb90-74e71a55cbb7): [orbit augmentation](https://prove2.me/theorems/85478003-b7db-44ef-be81-1c0fc5d7a8b4), [region homology budgets](https://prove2.me/theorems/e3d78c98-ef71-4b2a-a04a-7fd93fe9246f), [two-corner homology budgets](https://prove2.me/theorems/f6cc0221-29eb-4e8a-9649-8856b2954f2a), [the Laurent mass threshold](https://prove2.me/theorems/2d22450e-c4ce-4a0c-8829-b51d65e80eb5), and [mass-two positivity](https://prove2.me/theorems/988bc029-7a8a-43d7-9413-9e9cc3f86c24). No theorem currently connects their completion to a proof or disproof of $\mathsf{SPC4}$. They are exploratory tools, not established milestones in a proof of the main goal.
## Difficulty
A homeomorphism can transport the standard atlas, but that observation does not compare the transported atlas with the one already specified on the manifold. Treating those two atlases as equal would remove the central mathematical question by changing its hypotheses.
Likewise, topological recognition does not supply a smooth recognition theorem. Standard disk and collar constructions establish local models; they do not establish a smooth gluing or recognition theorem for an arbitrary prescribed smooth structure, a recognition theorem for arbitrary smooth balls, or a smooth Schoenflies theorem. The missing global comparison cannot be replaced by successful finite algebraic tests or by constructing a standard local chart.
## Formalization scope
The sphere goal quantifies over `Type` in universe zero, exactly as in the source. It uses real four-dimensional Euclidean chart models, compactness, the Hausdorff condition, and smoothness of order $\infty$. Boundaryless manifolds are built into that model. No orientation, fixed parametrization, or identity-map uniqueness is imposed.
The geometric foundations use charted spaces, structure groupoids, models with corners, homotopy equivalences and diffeomorphisms. Disk results include every $m\geq0$, so their dimensions are $m+1\geq1$. The boundary-set identification does not by itself construct a general induced smooth boundary structure. Nor is smoothness asserted for a radial clamp across its nonsmooth locus.
The separate source assertion `SPC4Ball` is not treated as equivalent to the sphere goal: the required formal boundary, capping and gluing bridge is absent. The transported-annulus product diffeomorphism is not a current target; its chart instances serve only as constructor support. No unconditional implication is taken through the source's admitted Freedman declaration. Gaussian coupling, transport defects, partition incidence and merge-score results remain outside this mission because no mathematical dependency on them has been established.
## Selected references
- R. İnanç Baykur, Robion C. Kirby and Daniel Ruberman, eds., *K3 — A New Problem List in Low-Dimensional Topology*, Mathematical Surveys and Monographs 295, American Mathematical Society, 2026, Problem 4.1, pp. 191–192. [Author PDF](https://math.berkeley.edu/sites/default/files/surv-295-ruberman-watermarked-author-pdf.pdf).
- Michael Hartley Freedman, *The topology of four-dimensional manifolds*, Journal of Differential Geometry 17 (1982), 357–453, Theorem 1.6, p. 371. [DOI](https://doi.org/10.4310/jdg/1214437136); [primary-article scan](https://www.maths.gla.ac.uk/~mpowell/1982_The%20topology%20of%20four-dimensional%20manifolds.pdf).
- Stephen Smale, *Generalized Poincaré's Conjecture in Dimensions Greater Than Four*, Annals of Mathematics 74 (1961), 391–406, Theorem A. [DOI](https://doi.org/10.2307/1970239); [primary-article scan](https://www.math.uchicago.edu/~shmuel/tom-readings/Smale,%20PC.pdf).
- Ryan Shin, *SPC4.lean*, *Bridge.lean* and *Disk.lean*, unpublished source files, 2026; no public manuscript URL available. SHA-256, respectively: `b17fdb932034e5211d0db8171c08e2b3a182016bceaecdd2deb49c39d6bfd5cc`, `e8ea6b66f6bd675ca272e862e0825ab2db1f8bb792eaffe1b9e8f5d89024d302`, `889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e`.
- Ryan Shin, *Hemisphere.lean*, unpublished Lean source file, 2026, declaration `twistedSphereHomeoSphere`; source SHA-256 `c48843d2c4ec6987acfd7f7ab3a92bfed990376206142e74712795b4e9399828`. [Published topological two-disk gluing target](https://prove2.me/theorems/fe8e71c7-85fd-4392-8327-453dda13f24c); the recovered local construction is checked; the accepted proof and its two supporting lemmas were contributed by carlok.
## Motivation
Positive-definite functions sit at a crossroads of harmonic analysis, probability, and machine learning. A function $f:\mathbb R\to\mathbb C$ is *positive-definite* if, for every finite family of points $x_1,\dots,x_n$ and complex coefficients $c_1,\dots,c_n$, the Hermitian quadratic form $\sum_{i,j}\overline{c_i}c_j f(x_i-x_j)$ is real and nonnegative. This single algebraic condition is exactly what makes $f$ realizable as: the covariance kernel of a stationary stochastic process; the characteristic function of a random variable (up to normalization); a valid Mercer/RBF kernel in machine learning; or a valid random-features/spectral density in random-feature kernel approximation methods.
Bochner's theorem (1932) is the structural reason all of these examples work: it says positive-definiteness is not merely a *necessary* condition for such a representation, but *exactly characterizes* it. A continuous, normalized ($f(0)=1$) function is positive-definite if and only if it is the Fourier–Stieltjes transform of some probability measure $\nu$ on $\mathbb R$ — i.e. $f$ is the characteristic function of a random variable. This mission asks for a machine-checked proof of that theorem, together with its most useful corollary: the case where $f$ is additionally Lebesgue-integrable, so that $\nu$ has an explicit continuous density given directly by the ordinary Fourier transform of $f$.
## Setting
Fix `IsPositiveDefinite f` as above, for $f:\mathbb R\to\mathbb C$ (not restricted to real-valued kernels — the standard, fully general statement). A positive-definite function is automatically Hermitian-symmetric, $f(-x)=\overline{f(x)}$ (`IsPositiveDefinite.conj_neg`), which is exactly what makes a representation by a genuine (positive) probability measure possible, rather than a signed or complex one. The theorem works with `f` continuous and normalized. No further hypothesis (in particular, no integrability of `f`) is assumed for the general representation theorem: the representing measure $\nu$ need not be absolutely continuous (e.g. for a periodic $f$, $\nu$ is a discrete measure supported on the harmonics of the period — this is Herglotz's 1911 theorem, the periodic special case). Under the extra hypothesis that `f` is Lebesgue-integrable, the representing measure becomes absolutely continuous with a continuous density: this density is `fourierTransform f`, the (real part of the) Fourier transform of `f` — automatically real-valued, again by Hermitian symmetry — and Fourier inversion recovers `f` from it.
## Formalization targets
### Goal — Bochner's theorem, general case
$$
f \text{ continuous, positive-definite, } f(0)=1 \;\Longrightarrow\; \exists\, \nu \text{ a probability measure on } \mathbb R,\; \forall x,\; f(x) = \int_{\mathbb R} e^{i2\pi\xi x}\,d\nu(\xi).
$$
The central representation theorem: no integrability hypothesis on $f$, so $\nu$ may be any probability measure, not necessarily a density.
### Milestone — Bochner's theorem, `L¹` (density) case
$$
f \text{ continuous, integrable, positive-definite, } f(0)=1 \;\Longrightarrow\; \tau:=\text{fourierTransform } f \text{ is continuous}, \;\tau \ge 0,\; \int \tau = 1, \text{ and } f(x) = \int e^{i2\pi\xi x}\tau(\xi)\,d\xi.
$$
The special case where the representing measure of the goal theorem is absolutely continuous with an explicit density — the form most directly usable in applications. Provable independently of the general goal theorem via classical Fourier-inversion machinery, so it is a natural, self-contained first target.
## Significance
Bochner's theorem is one of the load-bearing structural results of 20th-century harmonic analysis: it underlies Bochner–Minlos-type theorems for random fields, the entire theory of stationary Gaussian processes, kernel methods in statistics and machine learning, and (via its periodic specialization, Herglotz's theorem) the spectral theory of stationary time series. Formalizing it gives the platform a reusable, general-purpose characterization of positive-definite functions that any future mission on kernel methods, random features, or characteristic functions can build on directly.
## Difficulty
The general representation theorem is the harder target: the standard proof (see the Wikipedia article linked below) constructs, from `f`, a strongly continuous unitary representation of $\mathbb R$ on a Hilbert space via a GNS-type construction, then invokes Stone's theorem and the spectral theorem to extract the representing measure — a substantial functional-analytic argument, since `f` need not be integrable and $\nu$ need not have a density. The `L¹` milestone is comparatively more tractable: it can be attacked directly via Mathlib's existing Fourier-transform and Fourier-inversion machinery for integrable functions, plus the elementary fact (already available for reuse: `IsPositiveDefinite.conj_neg`) that a positive-definite function is Hermitian-symmetric.
## Formalization scope
`IsPositiveDefinite` is formalized exactly as the finite Hermitian-form condition above, over `Fin n → ℝ` point families and `Fin n → ℂ` coefficients, matching the standard convention in the literature, with `f : ℝ → ℂ` — the fully general, complex-valued statement, not restricted to real-valued kernels. `fourierTransform f ξ` is defined as the real part of `∫ Complex.exp(-i2πξ x) * f(x) dx`; this is provably the exact (not merely real-part-of) Fourier transform once `f` is positive-definite, since Hermitian symmetry forces the integral to be real already.
## Selected references
- [Bochner's theorem](https://en.wikipedia.org/wiki/Bochner%27s_theorem), Wikipedia — states the general locally-compact-abelian-group form and sketches the unitary-representation proof; a good map of the territory before diving into either target.
- Salomon Bochner, *Vorlesungen über Fouriersche Integrale*, Akademische Verlagsgesellschaft, 1932.
- Gustav Herglotz, *Über Potenzreihen mit positivem, reellem Teil im Einheitskreis*, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, 1911.
- Walter Rudin, *Fourier Analysis on Groups*, Interscience, 1962, Chapter 1.