Motivation

A sorting network is a sorting procedure whose sequence of comparisons is fixed in advance, independently of the data. Its depth, the number of rounds of simultaneous comparisons on disjoint pairs, is the parallel running time. Sorting networks are used in parallel and hardware sorting, in switching networks, and in cryptography, where a data-independent (oblivious) sequence of operations is required. How small the depth can be as a function of the number of inputs $n$ is a basic question of parallel computation.

Timeline:

• 1968. Batcher's odd-even merge sort and bitonic sort give networks of depth $O((\log n)^2)$ and size $O(n(\log n)^2)$ (K. E. Batcher, Sorting networks and their applications, AFIPS Spring Joint Computer Conference, 1968). For $n$ a power of two they remain the best explicit networks in practice.
• 1973. Knuth's The Art of Computer Programming, Vol. 3, §5.3.4, surveys sorting networks. A simple counting argument gives the lower bound: every sorting network has depth at least $\log_2 n$, since each output depends on at most $2^{\text{depth}}$ inputs.
• 1983. Ajtai, Komlós and Szemerédi construct networks of depth $O(\log n)$ and size $O(n\log n)$ (Combinatorica 3 (1983) 1–19, doi:10.1007/BF02579338), matching the lower bound up to a constant. The constant is not computed in the paper and is known to be very large.
• 1990. Paterson simplifies the construction and gives the first explicit, still very large, depth constant (M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92, doi:10.1007/BF01840378).
• 2014. Goodrich gives Zig-zag sort, a simpler deterministic data-oblivious sorting algorithm with $O(n\log n)$ comparisons that avoids the AKS machinery but is not of logarithmic depth (arXiv:1403.2777).

Setting

There are $n$ registers $R_1,\dots,R_n$ holding elements of a linearly ordered set. An elementary step (a comparator) $(i,j)$ with $i\neq j$ compares the contents of $R_i$ and $R_j$ and exchanges them if the content of $R_i$ is larger. Afterwards $R_i$ holds the minimum and $R_j$ the maximum of the two, and every other register is unchanged. A parallel step is a set of comparators in which no register occurs twice, so it has at most $n/2$ comparators. A comparator network $N$ is a finite sequence of parallel steps, fixed before the input is seen. Its depth $\operatorname{depth}(N)$ is the number of parallel steps and its size $\operatorname{size}(N)$ the total number of comparators. $N$ sorts if for every input $x=(x_1,\dots,x_n)$ the output $N(x)$ satisfies $N(x)_1\le\cdots\le N(x)_n$.

The construction runs on the tree $T$ of finite $0$-$1$ sequences, whose levels are ordered lexicographically. A chain on level $i$ assigns to every node of that level a set of registers, with the sets pairwise disjoint and of a common size $N(C)$. A ⟨k, ε⟩ expander on ⟨A, B⟩, for disjoint register sets $A$ and $B$, is a bipartite graph between $A$ and $B$ of maximum degree $k$ in which every nonempty $X\subseteq A$ has more than $(1-\varepsilon)\varepsilon^{-1}\min\{|X|,\varepsilon|B|\}$ neighbours, and symmetrically for $B$. The Lean development uses the names ComparatorNetwork, compareExchange, IsChain, chainN, IsExpander, IsLowerSection for these objects.

Formalization targets

Goal: the AKS theorem (Abstract and §1, p. 1)

The constant is absolute and is not fixed. Any explicit value would be invalidated by the next improvement, and the paper gives none.

Milestones (the paper's numbered lemmas that hold as stated)

• Lemma 3 (p. 6): for $0<\varepsilon<1$ and $c\ge1$ there is $k(\varepsilon,c)$ such that every pair of disjoint sets with $1/c\le|A|/|B|\le c$ carries a $\langle k,\varepsilon\rangle$ expander.
• Lemma 4 (p. 7): performing every comparator of such an expander once, in any order, from $A$ to $B$ leaves all but an $\varepsilon$-fraction of any lower section $S$ with $|S|\le|A|$ in $A$, and symmetrically for upper sections in $B$:

• Lemma 1 (pp. 3–4): the splitting $V(C,k)$ of a chain, which moves one register of each leaf set up the tree, produces chains with properties (1.1)–(1.5).
• Lemma 2 (p. 4): chains $W(C,k)$ with $a_k-1\le N(W(C,k))\le a_k$ exist under conditions (2a), (2.b).
• Lemma 12(a) (p. 14): a violation of the order relation $R^\beta_G$ between two nodes of a level is witnessed by two consecutive nodes.

Significance

The result. The AKS theorem settles the asymptotic depth of sorting networks at $\Theta(\log n)$ and their size at $\Theta(n\log n)$. It gives an $O(\log n)$-time sorting algorithm with $n$ processors that performs only data-independent comparisons. It is the standard reference point for oblivious sorting in parallel algorithms, circuit complexity (sorting is in $\mathsf{NC}^1$ via comparators) and oblivious RAM constructions. Lemma 4, the ε-halver property of expander comparisons, is the component that later constructions (Paterson) reuse.

Formalizing it. The theorem has been proved since 1983. No Lean proof of the AKS theorem is known. Mathlib has no expander graphs in the ⟨k, ε⟩ sense and no sorting networks. The mission asks for a formal proof of the headline theorem by any route (the AKS construction or Paterson's variant), and for formal proofs of the paper's verified lemmas as reusable components. The expander lemma needs either an explicit family (Margulis; Gabber–Galil) or a probabilistic existence argument, both substantial on their own.

Difficulty

Every elementary argument stalls at depth $O((\log n)^2)$: recursive merging needs $\log n$ merge rounds, and merging two sorted lists by a comparator network needs depth $\Omega(\log n)$. A depth of $O(\log n)$ therefore cannot come from exact merging. It must come from constant-depth approximate operations (ε-halvers, which require bounded-degree expanders) combined with a mechanism that corrects the errors they leave. In the paper this mechanism is a movement of registers up and down a binary tree, controlled by a family of constants chosen in a fixed order ("$\varepsilon_1\ll q_2\ll1-g\ll q_1\ll 1/c_1\ll1$", p. 2). The accounting that shows the misplaced elements decay geometrically is the hard part. Several intermediate lemmas of the paper are false as printed, so the paper's text is not a checklist to transcribe.

Formalization scope

Conventions committed to in Lean:

• Registers are Fin n, and contents lie in an arbitrary linearly ordered type. A network is a List of layers, each a List (Fin n × Fin n) of comparators with distinct endpoints, and no register occurs twice in a layer. A comparator $(i,j)$ puts the minimum into $i$, and both directions $i<j$ and $i>j$ are allowed. Sorts means the output is monotone for every linearly ordered type and every input, not only for permutations.
• $\log_2 n$ is Real.logb 2 n, and the goal is stated for $n\ge2$. The constant $c$ is quantified before $n$.
• Tree levels are Fin (2^i), with numeric order equal to lexicographic order. A chain is a Fin (2^i) → Finset R.
• Definition 2.2 of the paper, read literally, requires $|\Gamma_\emptyset|>0$, which fails, so no graph would be an expander. The expansion inequalities are imposed on nonempty sets only, and the strict inequality is kept.

Trivializing formalizations are ruled out. The goal is not "for every $n$ there is a network of depth $O(\log n)$" with the constant chosen after $n$, which is true for trivial reasons. Layers without the disjointness condition would let a single layer contain a whole insertion sort. A bound on the number of comparisons alone, with unbounded depth, is a different and much older result; the goal states both the depth and the size bound.

The mission states the AKS theorem and the paper's lemmas that are correct as stated. It does not formalize the AKS algorithm itself ($S^\alpha$, $P^\alpha$, the operations CH1–CH4, IMP) or its intermediate Lemmas 5–11 and 13–15. Those depend on unspecified constants constrained only by "sufficiently small" chains, and Lemmas 5, 10 and 12(b) are false as printed. A solver may of course define the algorithm, with pinned constants, as part of a proof.

Contributions welcome: a library of comparator networks (composition, the 0-1 principle, depth of Batcher's networks), existence of bounded-degree bipartite expanders, the ε-halver lemma, and any complete proof of the goal. The network and expander definitions are independent of this paper and reusable.

Selected references

• M. Ajtai, J. Komlós, E. Szemerédi, Sorting in c log n parallel steps, Combinatorica 3(1) (1983) 1–19. doi:10.1007/BF02579338
• K. E. Batcher, Sorting networks and their applications, Proc. AFIPS Spring Joint Computer Conference 32 (1968) 307–314. doi:10.1145/1468075.1468121
• D. E. Knuth, The Art of Computer Programming, Vol. 3: Sorting and Searching, Addison-Wesley, 1973, §5.3.4.
• G. A. Margulis, Explicit constructions of concentrators, Problems of Information Transmission 9 (1973) 325–332.
• O. Gabber, Z. Galil, Explicit constructions of linear-sized superconcentrators, J. Computer and System Sciences 22(3) (1981) 407–420. doi:10.1016/0022-0000(81)90040-4
• M. S. Paterson, Improved sorting networks with O(log N) depth, Algorithmica 5 (1990) 75–92. doi:10.1007/BF01840378
• M. T. Goodrich, Zig-zag sort: a simple deterministic data-oblivious sorting algorithm running in O(n log n) time, STOC 2014. arXiv:1403.2777

Motivation

The combinatorial diameter of a polyhedron is the largest distance, in its vertex-edge graph, between two vertices. It is a lower bound on the number of pivots any edge-following method such as the simplex method needs in the worst case, which is why the polynomial Hirsch conjecture — the diameter of $P = \{x \in \mathbb{R}^n : Ax \le b\}$ is bounded by a polynomial in $m$ and $n$ — is a central open question of linear optimization and discrete geometry. The best general upper bound is quasi-polynomial, $m^{1+\log n}$ (Kalai–Kleitman 1992); the original Hirsch bound $m - n$ is false for polytopes (Santos 2012).

A different line of work bounds the diameter by the arithmetic of the constraint matrix instead of its size. For an integer matrix $A$ let $\Delta$ be the largest absolute value of a sub-determinant of $A$. Dyer and Frieze (1994) showed that for totally unimodular $A$ ($\Delta = 1$) the diameter is polynomial, $O(m^{16} n^3 (\log mn)^3)$. Bonifas, Di Summa, Eisenbrand, Hähnle and Niemeier (SoCG 2012; Discrete Comput Geom 52, 2014) improved and generalized this to $O(\Delta^2 n^4 \log n\Delta)$ for all polyhedra and $O(\Delta^2 n^{3.5} \log n\Delta)$ for polytopes, bounds that do not depend on the number $m$ of inequalities. This mission formalizes the polytope case.

Setting

Let $A \in \mathbb{Z}^{m\times n}$ with rows $a_1,\dots,a_m$, let $b \in \mathbb{R}^m$, and let $P = \{x \in \mathbb{R}^n : Ax \le b\}$. A vertex of $P$ is an extreme point; for a polyhedron this is a point of $P$ at which $n$ linearly independent inequalities are tight. Two vertices $u \ne v$ are adjacent if the segment $[u,v]$ is an edge (a one-dimensional face) of $P$. This gives the polyhedral graph $G_P = (V, E)$, and the diameter of $P$ is at most $B$ if every two vertices are joined by a walk of at most $B$ edges.

$A$ has sub-determinants bounded by $\Delta$ if every $k\times k$ submatrix, for every $k \ge 1$, has determinant in $[-\Delta, \Delta]$. In particular every entry is at most $\Delta$ in absolute value.

For a vertex $v$ the normal cone $C_v$ is the set of objectives $c$ for which $v$ maximizes $c^T x$ over $P$. With $B_n$ the closed unit ball, the volume of a set $U \subseteq V$ of vertices is

and the neighbourhood $\mathcal N(I)$ of $I \subseteq V$ is the set of vertices outside $I$ adjacent to a vertex of $I$. A spherical cone is $S = C \cap B_n$ with $C$ closed under non-negative scaling; its dockable surface $D(S)$ is the $(n-1)$-dimensional measure of the part of its boundary inside the open ball. A cone of revolution of angle $0<\theta\le\pi/2$ is $\{x \in B_n : v^T x \ge \cos\theta\,\|v\|\,\|x\|\}$. $P$ is non-degenerate if every vertex has exactly $n$ tight inequalities.

Formalization targets

Goal: Theorem 2 (p. 105)

If $A \in \mathbb{Z}^{m\times n}$ has all sub-determinants bounded by $\Delta$ and $P$ is bounded, then

No non-degeneracy, full-dimensionality or rank condition is assumed, and the bound is uniform in $m$ and $b$.

Milestones

1. Lemma 3 (p. 108): for a vertex $v$ of a non-degenerate polytope, $D(S_v) \le \Delta^2 n^3\,\mathrm{vol}(S_v)$, where $S_v = C_v \cap B_n$.
2. Lemma 4 (p. 109): among spherical cones of a given volume, a cone of revolution has minimum dockable surface.
3. Lemma 5 (p. 110): for a cone of revolution, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$.
4. Lemma 6 (p. 111): for every measurable spherical cone with $\mathrm{vol}(S) \le \frac12 \mathrm{vol}(B_n)$, $D(S) \ge \sqrt{2n/\pi}\,\mathrm{vol}(S)$.
5. Lemma 1 (p. 105): for a non-degenerate polytope and $I \subseteq V$ with $\mathrm{vol}(I) \le \frac12\mathrm{vol}(B_n)$,

6. Eq. (1) (p. 105): if $I_j$ is the set of vertices at graph distance at most $j$ from a vertex $v$ and $\mathrm{vol}(I_j) \le \frac12\mathrm{vol}(B_n)$, then $j \le \sqrt{2\pi}\,\Delta^2 n^{2.5}\ln(2^n/\mathrm{vol}(I_0))$.

Significance

The result. Theorem 2 bounds the diameter of every integral polytope by a polynomial in the dimension and the largest sub-determinant, independently of the number of facets. For totally unimodular matrices, which cover network-flow, bipartite matching and transportation polytopes, it gives $O(n^{3.5}\log n)$, improving the Dyer–Frieze bound by a large polynomial factor. It shows that the obstruction to a polynomial Hirsch bound, if any, must come from matrices with large sub-determinants. The volume-expansion method — measuring breadth-first search by the volume of the normal fan it has covered — was later refined, for instance in the shadow-vertex analysis of Dadush–Hähnle, which improves the dependence on $n$.

Formalizing it. The theorem is proved (2012/2014); no machine-checked proof is known. A formal development needs, on top of Mathlib, the normal fan of a polytope and its relation to the vertex-edge graph, a Hausdorff-measure calculus for cones (surface of a cone in terms of its base), Lévy's isoperimetric inequality on the sphere in a measure-theoretic form, and explicit Gamma-function estimates. Each of these is reusable well beyond this paper.

Difficulty

The combinatorial side is short; the geometry is not. Lemma 4 is the spherical isoperimetric inequality of Lévy, which Mathlib does not have in any form, and which the paper cites rather than proves; the relations between the volume of a spherical cone, the area of its base, its lateral surface and the length of the base's boundary (Eq. (3), "basic integration") are also absent. Lemma 3 depends on the structure of the normal cone of a vertex of a non-degenerate polytope (full-dimensional, simplicial, generated by rows of $A$), none of which is available for Mathlib's extreme points. Lemma 1 depends on the normal fan of a polytope: the normal cones have pairwise disjoint interiors, cover $\mathbb{R}^n$, and share a facet exactly when their vertices are adjacent. The step from non-degenerate to arbitrary polytopes perturbs $b$ and needs the diameter not to decrease, a statement about the vertex-edge graph under perturbation. A shortcut through a finite graph abstraction is not available: the constant depends on the geometry of the normal cones, not only on the graph.

Formalization scope

The polyhedron is Hirsch.Hpoly (rowVec A) b, with rowVec A i the $i$-th row of $A \in$ Matrix (Fin m) (Fin n) ℤ as a vector of EuclideanSpace ℝ (Fin n). Vertices are Set.extremePoints ℝ P, adjacency is Hirsch.Adj, "diameter at most $B$" is Hirsch.DiamLE P B, all from the published Hirsch_model. The normal cone is the published FirstOrderOpt.ConvexTheory.normalCone. Volumes are Lebesgue measure with values in $[0,\infty]$; the dockable surface uses μHE[n-1], the Hausdorff measure normalized to agree with Lebesgue measure on hyperplanes, applied to frontier S ∩ Metric.ball 0 1. $\Delta$ is a natural number and the sub-determinant bound ranges over all sizes $k \ge 1$.

Explicit constants. The paper writes $O(\Delta^2 n^{3.5}\log n\Delta)$ in Theorem 2; the proof on pp. 105–106 yields $2\lfloor K\rfloor + 2$ with $K = \sqrt{2\pi}\,\Delta^2 n^{5/2}\ln(2^n n!\, n^{n/2}\Delta^n)$, from Eq. (1), the bound $\mathrm{vol}(I_0) \ge 1/(n!\,n^{n/2}\Delta^n)$ and the fact that the diameter is at most twice the number of breadth-first-search iterations needed to cover more than half of $B_n$. This explicit bound is the goal. The ratios $D/\mathrm{vol}$ of Lemmas 3, 5, 6 are stated in multiplicative form.

Non-degeneracy is a hypothesis of Lemma 3, Lemma 1 and Eq. (1) only, as in the paper's §1.1, and never of Theorem 2. The neighbourhood $\mathcal N(I)$ excludes $I$; including it would make Lemma 1 trivial, since its constant is below $1$. Lemma 4 is stated against every competitor: for every measurable spherical cone $S$ and every cone of revolution $S^*$ of the same volume, $D(S^*) \le D(S)$; it does not assert existence of a cone of a prescribed volume. The goal is Theorem 2 about the polytope and its graph, not an abstract statement about set families with a volume-expansion property; integrality of $A$ and the bound on minors of every size are both essential (scaling a real matrix down makes $\Delta$ arbitrarily small), and the raw Hausdorff measure μH[n-1] would put Lemmas 3 and 6 on incompatible scales.

Contributions are welcome at every level: the normal fan and its adjacency structure, cone surface formulas, the Gamma estimate $\Gamma(x+\frac12)/\Gamma(x) \ge \sqrt{x-\frac14}$, and a formal Lévy inequality.

Selected references

• N. Bonifas, M. Di Summa, F. Eisenbrand, N. Hähnle, M. Niemeier, On Sub-determinants and the Diameter of Polyhedra, Discrete Comput Geom 52 (2014) 102–115. https://doi.org/10.1007/s00454-014-9601-x
• M. Dyer, A. Frieze, Random walks, totally unimodular matrices, and a randomised dual simplex algorithm, Math. Program. 64 (1994) 1–16. https://doi.org/10.1007/BF01582563
• G. Kalai, D. J. Kleitman, A quasi-polynomial bound for the diameter of graphs of polyhedra, Bull. Amer. Math. Soc. 26 (1992) 315–316. https://doi.org/10.1090/S0273-0979-1992-00285-9
• F. Santos, A counterexample to the Hirsch conjecture, Annals of Math. 176 (2012) 383–412. https://doi.org/10.4007/annals.2012.176.1.7
• T. Figiel, J. Lindenstrauss, V. Milman, The dimension of almost spherical sections of convex bodies, Acta Math. 139 (1977) 53–94 (Lévy's isoperimetric inequality, Theorem 2.1). https://doi.org/10.1007/BF02392234
• D. Dadush, N. Hähnle, On the shadow simplex method for curved polyhedra, Discrete Comput Geom 56 (2016). https://arxiv.org/abs/1412.6705

Motivation

Ramsey's theorem says that every red/blue colouring of the pairs of an infinite set has an infinite monochromatic subset. For well-ordered sets one can ask for more: the monochromatic set should have the same order type as the whole set. Erdős and Rado introduced the partition relation $\alpha \to (\beta, c)^2$ to measure exactly this, and asked which countable ordinals $\alpha$ satisfy $\alpha \to (\alpha, 3)^2$ — every colouring either has a red copy of the whole order or a blue triangle. Such ordinals are called partition ordinals. Every partition ordinal $\alpha>1$ is a power of $\omega$, so the question becomes: for which countable $\beta$ is $\omega^\beta$ a partition ordinal? This is Erdős Problem 592.

The question is a basic test case for ordinal Ramsey theory: it is the smallest nontrivial "unbalanced" relation (a whole order type against a finite clique), and progress on it has repeatedly required new combinatorial methods.

Timeline (as recorded on erdosproblems.com/592):

• 1957 — Specker. $\omega^2 \to (\omega^2,3)^2$, and $\omega^n \not\to (\omega^n,3)^2$ for every finite $n \ge 3$.
• 1972 — Chang. $\omega^\omega \to (\omega^\omega,3)^2$ (the subject of Erdős Problem 590). Milner extended this to $\omega^\omega \to (\omega^\omega,m)^2$ for all finite $m$; Larson (1973) gave a short proof.
• 1974 — Galvin and Larson. If $\beta \ge 3$ and $\omega^\beta$ is a partition ordinal then $\beta$ is additively indecomposable, so $\beta=\omega^\gamma$. They conjectured that every such $\beta\ge3$ works.
• 2010 — Schipperus. Writing $\beta=\omega^\gamma$: the relation holds when $\gamma$ is a sum of one or two indecomposable ordinals, and fails when $\gamma$ is a sum of four or more. This refutes the Galvin–Larson conjecture in general.

The case where $\gamma$ is a sum of exactly three indecomposable ordinals appears to be the remaining open case.

Setting

An ordinal $\alpha$ is identified with a well-ordered set $X_\alpha$ of order type $\alpha$. A red/blue colouring of the complete graph $K_\alpha$ on $X_\alpha$ assigns to every pair of distinct vertices exactly one of two colours; equivalently, it is a pair of complementary simple graphs (red, blue) on $X_\alpha$.

For ordinals $\alpha,\beta$ and a cardinal $c$, the partition relation $\alpha \to (\beta,c)^2$ holds when every red/blue colouring of $K_\alpha$ has

• a set $S \subseteq X_\alpha$, all of whose pairs are red, whose order type (with the order inherited from $X_\alpha$) is exactly $\beta$, or
• a set $T \subseteq X_\alpha$, all of whose pairs are blue, with $|T| = c$.

The Lean predicate is Erdos592.OrdinalCardinalRamsey α β c, following the encoding used by the Formal Conjectures project. A partition ordinal is an $\alpha$ with $\alpha \to (\alpha,3)^2$.

An ordinal is additively indecomposable if it is nonzero and $a+b<\beta$ for all $a,b<\beta$; the additively indecomposable ordinals are exactly the powers $\omega^\delta$. An ordinal $\gamma$ is the sum of $k$ indecomposable ordinals when

i.e. its Cantor normal form has $k$ terms counted with multiplicity. The Lean predicate is Erdos592.IsSumOfIndecomposables k γ.

Formalization targets

Goal: the three-term case

This is the positive answer in the open case, as predicted by the Galvin–Larson conjecture. Because the truth is unknown, a formal disproof (exhibiting a countable $\gamma$ with three Cantor-normal-form terms for which the relation fails) is an equally valid resolution of the goal. Together with the milestones below, a proof of the goal gives a complete answer to Problem 592: for countable $\beta$, $\omega^\beta$ is a partition ordinal iff $\beta\le2$ or $\beta=\omega^\gamma$ with $\gamma$ a sum of at most three indecomposables.

Milestones (known results)

1. Specker: $\omega^2 \to (\omega^2,3)^2$.
2. Specker: $\omega^n \not\to (\omega^n,3)^2$ for $3 \le n < \omega$.
3. Chang: $\omega^\omega \to (\omega^\omega,3)^2$.
4. Galvin–Larson: $\beta \ge 3$ countable and $\omega^\beta \to (\omega^\beta,3)^2$ imply that $\beta$ is additively indecomposable.
5. Schipperus: $\gamma$ countable and a sum of one or two indecomposables imply $\omega^{\omega^\gamma} \to (\omega^{\omega^\gamma},3)^2$.
6. Schipperus: $\gamma$ countable and a sum of $k \ge 4$ indecomposables imply $\omega^{\omega^\gamma} \not\to (\omega^{\omega^\gamma},3)^2$.

Significance

The result itself. A resolution of the three-term case would, together with the results above, finish the classification of countable partition ordinals of the form $\omega^\beta$ asked for in Problem 592. Either answer is informative: a positive answer shows the threshold between the positive and negative cases lies between three and four terms, and a negative answer shows it lies between two and three.

Formalizing it. The drafter is not aware of any of the milestone results in Mathlib. The Formal Conjectures entry for Problem 590 links an external Lean formalization of Chang's theorem; the other results (Specker's positive and negative theorems, Galvin–Larson, Schipperus) have, to the best of the drafter's knowledge, no public machine-checked proofs. Formalizing them is a substantial project on its own, independent of the open case, and the goal itself is an open research problem.

Difficulty

The property is not monotone in $\beta$: it holds for $\beta=2$, fails for every finite $\beta\ge3$, holds again for $\beta=\omega$, and, by Schipperus, both holds and fails for various larger $\beta=\omega^\gamma$ depending on the number of terms in the Cantor normal form of $\gamma$. So no induction on $\beta$ can settle the question, and a naive transfer of the argument for a smaller exponent to a larger one can fail. The known positive and negative results use different arguments, and the three-term case lies exactly on the boundary between the ranges they cover.

Formalization scope

• Ordinals and cardinals are Mathlib's Ordinal.{u} and Cardinal.{u} in an arbitrary universe u; "countable" is γ.card ≤ ℵ₀.
• The graph lives on α.ToType, the canonical well-ordered type of order type α; a colouring is a pair of complementary SimpleGraphs (IsCompl red blue). A red $K_\beta$ is a red clique s with typeLT s = β; a blue $K_3$ is a blue clique of cardinality exactly 3.
• IsSumOfIndecomposables k γ requires a non-increasing list of exponents of length exactly k; without the ordering requirement, "sum of $k$" would not be well defined, since for instance $\omega+\omega^2=\omega^2$.
• ω ^ ω ^ γ means $\omega^{(\omega^\gamma)}$.
• The Galvin–Larson milestone states additive indecomposability directly as $\forall a,b<\beta,\ a+b<\beta$ (for $\beta \ge 3$ this is equivalent to $\beta=\omega^\gamma$).

The goal is not trivially satisfiable: the hypotheses hold, for example, for $\gamma=3$ and $\gamma=\omega^2+\omega+1$, and the conclusion is a genuine partition relation on an infinite ordinal.

Useful reusable infrastructure includes Cantor-normal-form combinatorics for countable ordinals, order-type calculations for subsets of $\omega^\beta$, and a library of the classical colourings (Specker-type constructions). Contributions formalizing any milestone are welcome.

Selected references

• T. F. Bloom, Erdős Problem #592, erdosproblems.com. https://www.erdosproblems.com/592 (this page lists the original references [Sp57], [Ch72], [GaLa74], [Sc10] cited below).
• E. Specker, Teilmengen von Mengen mit Relationen, Comment. Math. Helv., 1957.
• C. C. Chang, A partition theorem for the complete graph on $\omega^\omega$, J. Combinatorial Theory Ser. A, 1972.
• J. A. Larson, A short proof of a partition theorem for the ordinal $\omega^\omega$, Ann. Math. Logic, 1973/74.
• F. Galvin and J. Larson, Pinning countable ordinals, Fund. Math., 1974/75.
• R. Schipperus, Countable partition ordinals, Ann. Pure Appl. Logic, 2010.
• Formal Conjectures (Google DeepMind), Erdős Problems 590–592. https://github.com/google-deepmind/formal-conjectures

Motivation

Many approximation problems resist the standard PCP toolkit: the best known NP-hardness factors for Max-Cut, Vertex-Cover and approximate graph colouring are far from the best known polynomial-time algorithms. To explain this gap, Khot (CCC 2002) proposed the Unique-Games Conjecture and the family of $d$-to-1 Games Conjectures. The $d$-to-1 conjectures assert perfect completeness: the hard instances are either fully satisfiable, or satisfiable only to a vanishing extent. Perfect completeness is what makes these conjectures usable for colouring problems, where a "yes" instance must be genuinely $3$-colourable rather than almost so.

A line of work culminating in Khot–Minzer–Safra and Dinur–Khot–Kindler–Minzer–Safra established the almost-perfect completeness version for $2$-to-1 games: for every $\varepsilon>0$ there is an alphabet bound $r$ such that distinguishing value $\ge 1-\varepsilon$ from value $\le\varepsilon$ is NP-hard. Their route goes through Håstad's hardness for linear equations, which cannot have perfect completeness, so the loss is intrinsic to the technique. The source paper of this mission removes that loss for $d = 4$.

Setting

A label-cover instance $\Psi$ (Definition 1.1 of the source) consists of a bipartite graph $G = (L \sqcup R, E)$, two finite alphabets $\Sigma_L, \Sigma_R$, and for each edge $e = (u,v)$ a constraint $\Phi_e \subseteq \Sigma_L \times \Sigma_R$. The constraint is a projection constraint if there is $\varphi_e : \Sigma_L \to \Sigma_R$ with $\Phi_e = \{(\sigma, \varphi_e(\sigma))\}$, and a $d$-to-1 constraint if in addition $|\varphi_e^{-1}(\sigma)| = d$ for every $\sigma \in \Sigma_R$. Given assignments $A_L : L \to \Sigma_L$ and $A_R : R \to \Sigma_R$, the fraction of satisfied edges is $\mathrm{val}_\Psi(A_L, A_R)$, and

An instance all of whose constraints are $d$-to-1 is a $d$-to-1 game.

For $0 < s < c \le 1$, $\mathrm{Gap\text{-}}d\mathrm{\text{-}to\text{-}}1_r(c,s)$ is the promise problem: given a $d$-to-1 game with both alphabets of size at most $r$, distinguish $\mathrm{val}(\Psi) \ge c$ from $\mathrm{val}(\Psi) \le s$. Writing $\mathrm{GapPLC}_r(c,s)$ for the same promise problem over all projection instances, the PCP theorem together with the parallel repetition theorem gives that $\mathrm{GapPLC}_{r}(1,\varepsilon)$ is NP-hard for a suitable $r = r(\varepsilon)$ (Theorem 1.2 of the source); this mission takes that statement as an external input.

Formalization targets

Goal — Theorem 1.6 of the source

In Lean this is stated as a polynomial-time gap-preserving reduction: for every $\varepsilon > 0$ there is a soundness threshold $s \in (0,1)$ such that for every source alphabet bound $r_0$ there is a target alphabet bound $r$ and a polynomial-time computable map sending projection label-cover instances with alphabets of size at most $r_0$ and value $1$ to $4$-to-1 games with alphabets of size at most $r$ and value $1$, and instances of value at most $s$ to $4$-to-1 games of value at most $\varepsilon$. Combined with the NP-hardness of $\mathrm{GapPLC}_{r_0}(1,s)$, this is exactly Theorem 1.6.

Supporting targets

The milestone list follows the source's own numbering: the hardness of approximate colouring of $3$-uniform hypergraphs that starts the construction (Theorem 3.1), the two Grassmann decoding theorems the inner PCP rests on (Theorems 3.2 and 3.3), the sunflower bound on zoom-outs (Lemma 3.8), and the linear-algebraic layer connecting NAE-satisfying bilinear forms with their tensor decompositions (Propositions 4.13, 4.14 and Corollary 4.15).

Significance

Theorem 1.6 confirms the $4$-to-1 Games Conjecture, the first of Khot's $d$-to-1 conjectures to be settled with perfect completeness. Via known reductions it yields: for every $k$, it is NP-hard to $k$-colour a $3$-colourable graph (previously known for $k = 5$); for every $\delta>0$, it is NP-hard to find an independent set of relative size $\delta$ in a $2$-colourable $3$-uniform hypergraph; and hardness results for low-rank matrix completion.

None of this material is formalized today. Mathlib has no label cover, no PCP machinery, no Grassmann graph and no complexity classes beyond the computability layer. A complete development therefore contributes reusable infrastructure — finite two-prover games and their value, gap-preserving reductions, the Grassmann graph over $\mathbb{F}_2$ and its agreement tests — well beyond this single theorem.

Difficulty

The obvious attempt is to redo the $2$-to-1 construction with a perfectly complete outer PCP, namely hardness of systems of quadratic equations over $\mathbb{F}_2$ in place of linear ones. This fails at composition: the Grassmann agreement test, the only known device that produces $d$-to-1 constraints, is a test for linear functions and cannot certify quadratic constraints. Linearizing the quadratic equations by a low-rank test destroys the covering property of the outer PCP, which is what makes the composed soundness analysis work. The source paper's answer is a three-layer construction (outer, middle and inner PCP) with a lazy parallel repetition in the middle layer and an inner PCP based on a tensor of the standard Grassmann encoding with Golowich's low-rank variant.

Formalization scope

All objects are finite and explicit. A label-cover instance carries left vertices $\{0,\dots,n_L-1\}$, right vertices $\{0,\dots,n_R-1\}$, alphabets $\{0,\dots,|\Sigma_L|-1\}$ and $\{0,\dots,|\Sigma_R|-1\}$, a finite edge set, and a projection map for every pair of vertices; only projection instances are representable, as in Definition 1.1. The value is the supremum over all pairs of assignments of the fraction of satisfied edges, taken in $\mathbb{R}$; when there are no edges, or no assignments at all, the convention gives value $0$. A tripled set (Definition 4.1) is modelled as $\iota \times \{0,1,2\}$, with the triple indexed by $i$ being $\{(i,0),(i,1),(i,2)\}$. The Grassmann objects live in $\mathbb{F}_2^n$ modelled as $\mathrm{Fin}\,n \to \mathbb{Z}/2$, and all probabilities are ratios of cardinalities of finite sets of subspaces, with the convention that an empty denominator gives $0$.

Hardness is not stated as "NP-hard" — no notion of NP is available — but as the existence of a reduction. This matters: a reduction required only to preserve the gap, with no computability condition, would be trivially satisfiable by a map that inspects the value of its input and returns one of two fixed instances. The formalization therefore requires the reduction map to be computed by a Turing machine within a polynomial time bound, using Mathlib's Turing.TM2ComputableInPolyTime together with an explicit binary encoding of instances. The NP-hardness of the source problem $\mathrm{GapPLC}_{r_0}(1,s)$ (Theorem 1.2, i.e. the PCP theorem plus parallel repetition) is an external input and is not part of this mission.

Contributions of intermediate infrastructure are welcome: the games of Sections 4–6 (Game1a, Game1b, Game2a, Game2b, Game2c, Game3) and their completeness and soundness lemmas are the natural next layer of milestones, as are the covering properties of Appendix C and the list-decoding bounds of Appendix E.

Selected references

• Yumou Fei, Dor Minzer, Shuo Wang, On the Hardness of 4-to-1 Games with Perfect Completeness, ECCC TR26-179 (2026), https://eccc.weizmann.ac.il/report/2026/179/
• Subhash Khot, On the power of unique 2-prover 1-round games, STOC 2002, https://doi.org/10.1145/509907.509985
• Irit Dinur, Subhash Khot, Guy Kindler, Dor Minzer, Muli Safra, Towards a proof of the 2-to-1 games conjecture?, STOC 2018, https://doi.org/10.1145/3188745.3188804
• Subhash Khot, Dor Minzer, Muli Safra, Pseudorandom sets in Grassmann graph have near-perfect expansion, FOCS 2018, https://doi.org/10.1109/FOCS.2018.00062
• Louis Golowich, New Explicit Constant-Degree Lossless Expanders, FOCS 2023, https://arxiv.org/abs/2306.07551

Superlinear or exact bounds for planar distinct distances

Motivation

This mission asks how restrictions on collinear and cocircular points limit the reuse of distances in the plane. Its central question is Erdős Problem 98: must the minimum number of distances grow faster than the number of points?

Setting

For each positive integer n, let h(n) be the minimum number of distinct positive Euclidean distances determined by an n-point set in the plane with no three collinear points and no four cocircular points. Write D(P) for the number of distinct positive Euclidean distances determined by P.

Target

The mission is to establish a superlinear lower bound, or determine this extremal function exactly. The superlinear target is Erdős Problem 98:

Concretely, for every real A > 0, prove that there is an integer n_A such that every general-position configuration P with |P| = n >= n_A satisfies D(P) > A n. A fixed improvement of the coefficient 1/3, or an additive sublinear improvement above n/3, does not complete this objective.

The alternative completion target is an exact determination of h(n), proved by a universal lower bound and general-position constructions attaining that bound. State the range of n explicitly. An asymptotic estimate or a counterexample to superlinearity alone must be labeled with its actual scope; neither is an exact determination of h(n).

Significance and supporting results

A formally verified supporting result, an n^(1/4) additive bound for distinct distances, is

for some absolute c > 0 and all sufficiently large n. A complete Lean proof of this supporting theorem has been accepted on this platform. The n^(1/4), n^(1/5), and n^(1/6) theorem targets and their existing milestones are supporting results, not the mission's terminal goal. Resolving the superlinear target would establish a lower bound above every fixed linear coefficient. Determining h(n) exactly would settle the corresponding extremal problem with matching constructions.

Difficulty and research priorities

The n^(1/4) proof constructs an algebraic curve from a small distinct-distance count, proves pair separation, and constructs intrinsic curve cells to obtain the curve bound D(S) >= c d^(-4/3) |S|^(4/3) for finite samples S on noncircular, irreducible and absolutely irreducible, maximally circular curves of degree d, under |S|^2 >= T d^5 for absolute constants c,T > 0. The final calculation yields an additive n^(1/4) term. Stronger additive bounds count as intermediate progress; they must not be reported as a superlinear lower bound.

• Develop an argument that excludes D(P) <= A n for every fixed A > 0. A fixed-coefficient distance-energy gap is one sufficient route.
• Investigate additional structure of the Newton carriers and interactions between their factors, or another geometric or combinatorial route that can control the superlinear target.
• Investigate constructions and universal lower bounds together when pursuing an exact extremal determination.
• Preserve and formalize useful intermediate theorems while keeping their statements and remaining premises explicit.

Formalization scope

Configurations are finite subsets of the Euclidean plane. In the indexed formalization, a configuration is an injective map p : Fin n → ℝ²; write P = image(p) before using D(P). Both general-position hypotheses apply to the image. D(P) counts distinct positive distance values, not pairs or ordered multiplicities. The superlinear quantifier ranges over every real A > 0 and every sufficiently large general-position configuration.

The superlinear target and exact-determination target remain open here. Distinguish conjectures, conditional reductions, audited prose proofs, and kernel-checked Lean results. A completed supporting formalization does not by itself complete this mission.

Selected references

• Erdős Problem 98 — extremal question and bibliography.

• Proof of a fourth-root additive bound for planar distinct distances (dated 2026-09-13; revision 2026-09-14 UTC; Git revision 9e63c1648017becfc717d7e0e4f2877925ace28d; file SHA-256 8ceaca7bad8c07ce3d56f8bf726a0d273ddc41fd300b777fae1eb6525e087d29), manuscript, revised 2026-09-14.

• Independent audit of the fourth-root additive bound (dated 2026-09-14 UTC; Git revision 9e63c1648017becfc717d7e0e4f2877925ace28d; file SHA-256 911a06495542d5b4b6cf9f6a41418e4baf4ecd8800b80001b3cc3748f82b0e7b; target SHA-256 8ceaca7bad8c07ce3d56f8bf726a0d273ddc41fd300b777fae1eb6525e087d29), 2026-09-14.

Motivation

The weak pentagon problem asks for a five-label structure on the edges of every triangle-free cubic graph. Although its wording resembles proper edge coloring, properness is not part of the conjecture. Instead, each individual color class must meet enough odd cycles that deleting that class leaves a bipartite spanning graph. The problem connects odd-cycle transversals, cut structure, and homomorphisms to a fixed sixteen-vertex graph.

Robert Šámal recorded the conjecture on the Open Problem Garden in 2007. DeVos and Šámal proved that sufficiently high-girth subcubic graphs map to the Clebsch graph, with an explicit girth threshold in their theorem; that does not cover all triangle-free cubic graphs. The mission separates the general existence question from two exact reformulations that can be verified independently.

Setting

Let $G$ be a finite simple triangle-free cubic graph. A five-edge coloring here is any symmetric assignment

It need not be proper or surjective. For a color $i$, delete all edges with label $i$ while retaining every vertex. The coloring is a weak-pentagon coloring when each of the five resulting spanning graphs is bipartite.

Equivalently, each color class is an odd-cycle edge transversal: it meets the edge set of every simple odd cycle. The cycles are not required to be induced. This last distinction matters because an odd cycle may have a chord in the original graph and still survive in a deleted-edge spanning subgraph.

A second representation uses the sixteen four-bit vectors. Two vectors are adjacent when their Hamming distance is three or four. This graph is a model of the Clebsch graph. A graph homomorphism sends every edge of $G$ to an adjacent pair in this target.

Formalization targets

Weak pentagon conjecture

The root target is

No condition is imposed on adjacent edges receiving different labels.

Odd-cycle equivalence

For every fixed graph and fixed five-edge labeling,

This theorem is graph-general: triangle-freeness and cubicity delimit the root but are not needed for the equivalence.

Sixteen-vertex homomorphism formulation

For every finite simple graph $G$,

where $H_{16}$ has vertex set $\{0,1\}^4$ and edges at Hamming distance three or four. The statement concerns existence of some coloring and some homomorphism; it does not preserve an arbitrarily prescribed coloring.

Significance

The root theorem would establish a uniform parity decomposition for all triangle-free cubic graphs. The transversal form makes every odd cycle use all five colors. The homomorphism form replaces edge labels and five separate bipartitions by one bounded vertex certificate, allowing structural and computational methods to share an exact target.

Formalization prevents several nearby but inequivalent conjectures from being conflated. A weak-pentagon coloring can be improper. Checking only induced odd cycles of the original graph is insufficient. Mapping to a five-cycle is stronger and fails even for familiar positive examples. The explicit four-bit model also avoids relying on the name “Clebsch graph” without fixing its adjacency convention.

Difficulty

The equivalences reorganize the problem but do not create the required object. Five odd-cycle transversals must be pairwise compatible as color fibers; finding one small transversal is not enough. Local deletion and gluing methods must preserve existence of a whole homomorphism, not one chosen boundary assignment.

High-girth results leave finitely many short-cycle configurations only when the girth hypothesis is present. Triangle-free graphs may still contain overlapping five- and seven-cycles, and naive local recoloring can repair one odd cycle while breaking another color complement. Minimum-counterexample arguments also require care because deleting vertices preserves subcubicity but not cubicity.

Formalization scope

Colors are Fin 5. The coloring stores a symmetric value on ordered endpoint pairs, with nonedge values ignored. Cubic means every neighbor set has extended cardinality exactly three. A simple odd cycle is a cyclic list of at least three distinct vertices of odd length; it need not be induced. Bipartiteness is witnessed by a Boolean side assignment after one color is deleted.

The sixteen-vertex relation is defined directly on four-bit functions by Hamming distance, so its cardinality and adjacency are not hidden behind an imported graph name. The repository's transversal proof, normalization, and local homomorphism studies are candidate_only; the mission publishes their clean statements as proof obligations. Contributions may close either equivalence, formalize known high-girth results, prove restricted graph classes, or attack the root. A finite benchmark or a failure of one extension strategy is not a counterexample to the conjecture.

Selected references

• R. Šámal, Weak pentagon problem, Open Problem Garden, 2007. https://www.openproblemgarden.org/op/weak_pentagon_problem
• M. DeVos and R. Šámal, High-girth cubic graphs are homomorphic to the Clebsch graph, Journal of Graph Theory 66 (2011), 241–259. https://arxiv.org/abs/math/0602580
• P. Kolman, B. Lidický, and J.-S. Sereni, On Minimum Fair Odd Cycle Transversal, 2010. https://kam.mff.cuni.cz/kamserie/clanky/2010/s956.pdf
• Open Problem Garden / UnsolvedMath, OPG-434. https://www.unsolvedmath.com/problems/OPG-434

Motivation

The dichromatic number of a digraph is the directed analogue of chromatic number: vertices of one color may be adjacent, but each color class must induce an acyclic digraph. The Two Color Conjecture asks whether every orientation of a planar graph has dichromatic number at most two. It is a natural directed-coloring counterpart to planar graph coloring, with the key difference that forbidden monochromatic objects are directed cycles rather than undirected edges.

Critical-digraph theory gives general degree restrictions on minimal counterexamples, and Li and Mohar proved two-colorability under the additional hypothesis that the directed girth is at least four. The unrestricted planar-orientation problem permits directed triangles, so that theorem is a genuine partial result rather than a solution. The project candidate develops the elementary least-order-counterexample consequences needed before any planar structural argument.

Setting

Let $G$ be a finite simple planar graph. An orientation $D$ assigns exactly one direction to every edge of $G$, with no loops, parallel arcs, or pair of opposite arcs. For $X\subseteq V(D)$, the induced digraph $D[X]$ retains every arc whose two endpoints lie in $X$.

A two-coloring is a map

It is valid when both induced digraphs $D[c^{-1}(0)]$ and $D[c^{-1}(1)]$ contain no directed cycle. The color classes need not be independent and either color may be unused.

Planarity belongs to the underlying undirected graph. Lean represents it by an injective straight-line embedding with noncrossing nonincident edges. Directed reachability is reflexive, so a singleton orientation is strongly connected under the usual length-zero convention, although it is also acyclic and hence cannot be a counterexample.

Formalization targets

Two Color Conjecture

The goal is

Disconnected graphs and empty color classes are included.

Least-order counterexample structure

A supporting theorem states that every counterexample of minimum vertex order is nonempty and strongly connected, and its underlying graph has minimum degree at least three:

The minimum is taken over the full class of finite planar orientations, not over one embedding or an arc-minimal subclass.

Semidegree candidate

A stronger open milestone asks whether every vertex of such a least-order counterexample has at least two incoming and at least two outgoing neighbors. This is recorded separately because it is stronger than the degree-three conclusion and its repository proof remains candidate_only.

Significance

The root theorem would establish a universal two-color bound for planar orientations while allowing directed triangles and arbitrary local degree. A counterexample would demonstrate a sharp obstruction specific to directed cycles, not visible to ordinary planar coloring.

The formalized minimal-counterexample package is reusable regardless of the ultimate answer. Strong connectivity permits arguments inside one component, while the degree and semidegree restrictions narrow discharging configurations and finite searches. Encoding the full induced color classes prevents an invalid shortcut in which only a selected acyclic spanning subdigraph is checked.

Difficulty

Deleting a low-degree vertex is safe only if a valid coloring of the smaller graph can be extended without creating a monochromatic directed cycle through the restored vertex. For a chosen color, obstruction depends on both an incoming and an outgoing neighbor of that color together with a directed return path in the old color class. Merely seeing same-colored in- and out-neighbors is not sufficient.

Strongly connected components can be colored separately because their condensation is acyclic, but that observation only reduces a minimal counterexample to one component. Planarity alone does not eliminate directed triangles or the return paths that block both colors. Results assuming directed girth at least four therefore leave the central case untouched.

Formalization scope

A directed graph is a binary relation, coupled to a SimpleGraph by an orientation predicate that requires exactly one direction on every edge and forbids arcs on nonedges. A directed cycle is a cyclic list of at least three distinct vertices. A color class is acyclic when no such list lies entirely in that class. Strong connectivity is nonempty mutual reflexive-transitive reachability.

The least-order predicate quantifies over every smaller finite planar orientation in the same universe. It does not assert that a counterexample exists. Consequently, its structural theorems may be true vacuously if the root conjecture is true; the read-back must expose that conditional form.

Repository arguments, finite tables, and transport receipts are not machine-checked proofs. Contributions may formalize component gluing, exact vertex-extension criteria, degree or semidegree restrictions, planar reducible configurations, or the root. Any stronger minimum-degree claim must remain distinct from the admitted degree-three target until proved.

Selected references

• Open Problem Garden / UnsolvedMath, OPG-169: The Two Color Conjecture. https://www.unsolvedmath.com/problems/OPG-169
• B. Mohar, Eigenvalues and colorings of digraphs, Linear Algebra and its Applications, 2010. https://www.sfu.ca/~mohar/Reprints/Inprint/BM09_LAA09_Mohar_EigenvaluesandColorings.pdf
• Z. Li and B. Mohar, Planar digraphs of digirth four are 2-colourable, Journal of Combinatorial Theory, Series B, 2017. https://arxiv.org/abs/1606.06114

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

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

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$,

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

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. 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:

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:

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

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
• 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
• 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
• Open Problem Garden, Star chromatic index of subcubic graphs, OPG-37271. Problem page
• Vibe Mathing candidate repository, OPG-37271 star chromatic index of subcubic graphs, candidate-only artifacts at commit ddc49c1978a196490702150bb75264793a658457. Repository

That the prime numbers, thinning out as they climb yet never quite vanishing, should nonetheless contain arithmetic progressions of every finite length is one of the most celebrated discoveries of twenty-first-century mathematics. Ben Green and Terence Tao proved it in 2004 (published in the Annals of Mathematics in 2008), resolving a question whose roots reach back to Lagrange and Waring around 1770 and which had crystallized in the Erdős–Turán conjecture. The primes have density zero, so Szemerédi's theorem — which guarantees long progressions only in positive-density sets — does not apply directly; the genius of the proof was a transference principle extending Szemerédi's theorem to sets sitting densely inside a 'pseudorandom' host, built from the sieve ideas of Goldston, Pintz, and Yıldırım. The result was a centerpiece of the citation for Tao's 2006 Fields Medal and opened a whole industry, including the Tao–Ziegler extension to polynomial progressions. Unusually for a headline problem, this theorem is already proved — which makes it an ideal flagship formalization mission: a deep, decomposable argument whose pieces, from Szemerédi's theorem to the transference principle, the community can rebuild and verify in Lean.

Motivation

In auctions with interdependent values, the value an agent assigns to an outcome depends not only on her own private information but on the information of the others: a bidder for drilling rights values a tract according to every bidder's geological survey, and a buyer of a used asset values it according to every inspector's report. Each agent observes only her own signal, while the mechanism designer knows how values depend on the full signal profile. Maximizing welfare truthfully is then much harder than with private values: the VCG mechanism no longer applies, and without structural assumptions on the valuations no ex-post truthful mechanism gives a good approximation of the optimal welfare (the source's Examples 1.2–1.3).

Eden, Feldman, Fiat, Goldner and Karlin (arXiv:1903.08384) identify submodularity over signals (SOS) as a condition under which constant or near-constant approximations become possible, including for combinatorial auctions, where agents value bundles of items. For single-dimensional signals that take $k$ values, they give a $(k+3)$-approximation under SOS (Theorem 6.1) and, under the stronger condition strong-SOS, a $(2\log_2 k+4)$-approximation (Theorem 6.5). This mission formalizes the second result.

Timeline. Milgrom and Weber (1982) introduced the interdependent value model for auctions; Dasgupta and Maskin (2000) studied efficient auctions under the single-crossing condition. The computer science literature then gave approximation results for simple single-parameter settings (mostly single-item auctions or matroid constraints), again largely under single crossing or its variants, e.g. Roughgarden and Talgam-Cohen (2016) and Eden, Feldman, Fiat and Goldner (2018), as surveyed in the source. The SOS paper (arXiv v2, 2019; journal version in Mathematics of Operations Research, 2024) drops single crossing and gives, in its own words, the first welfare approximation guarantees for multi-dimensional combinatorial auctions with interdependent values.

Setting

There are $n$ agents and $m$ items. Agent $i$ holds a signal $s_i\in\{0,1,\dots,k-1\}$, and $\mathbf s=(s_1,\dots,s_n)$ is the signal profile. For every bundle $T\subseteq[m]$, agent $i$'s value is $v_{iT}(\mathbf s)\ge0$, with $v_{i\emptyset}=0$; for nonempty $T$ it is weakly increasing in every signal and strictly increasing in $s_i$.

A function $w$ of the profile is strong-SOS if for every coordinate $j$, every $\delta\ge0$ and profiles $\mathbf s'\le\mathbf s$ coordinate-wise,

Raising one signal helps less the higher the profile, including the raised coordinate itself; in particular the effect of an agent's own signal is concave. SOS asks this only when the raised coordinate starts from the same value in both profiles.

An allocation $T=(T_1,\dots,T_n)$ gives pairwise disjoint bundles. A deterministic mechanism maps reported signals to an allocation and payments; it is ex-post IC if, whatever the true signals and with the others truthful, no agent gains by misreporting, and ex-post IR if truthful utility is nonnegative. A randomized mechanism is universally ex-post IC-IR if every deterministic mechanism in its support is.

Let $k=2^q$. Random Bucket picks $\ell\in\{1,\dots,\log_2 k\}$ uniformly, calls $N_{B_\ell}=\{i:s_i\ge2^{\ell-1}\}$ the high agents, and allocates to them a bundle assignment maximizing $\sum_{i\in N_{B_\ell}}v_{iS_i}(\mathbf s_{N_{\neg B_\ell}},\mathbf{2^{\ell-1}}_{N_{B_\ell}})$, the values with every high signal lowered to $2^{\ell-1}$; agent $i$ receiving $\bar T_i$ pays $v_{i\bar T_i}(\mathbf s_{-i},2^{\ell-1}-1)$. Random Sampling splits the agents uniformly at random into $A$ and $B$, allocates to $B$ a bundle assignment maximizing $\sum_{i\in B}v_{iS_i}(\mathbf s_A,\mathbf 0_B)$, and charges nothing. k-SS runs Random Bucket with probability $p_{RB}=\frac{\log_2 k}{\log_2 k+2}$ and Random Sampling otherwise.

Formalization targets

Goal: Theorem 6.5

For strong-SOS valuations, k-SS is universally ex-post IC-IR and, for every grid profile $\mathbf s$ and every feasible allocation $T^*$,

Milestones

1. Strong-SOS implies SOS (p. 19).
2. Display (9), corrected: with $\mathsf{SELF}=\sum_{\ell=1}^{k-1}\sum_{i:s_i=\ell}v_{iT_i}(\mathbf 0_{-i},s_i)$,

3. Lemma 6.4: Random Bucket is ex-post IC-IR and $\mathsf{SELF}\le 2\log_2 k\cdot\mathbb E[\text{welfare of Random Bucket}]$.
4. The combination: $\mathsf{SELF}+\mathsf{OTHER}\le(2\log_2 k+4)\,\mathbb E[\text{welfare of k-SS}]$, where $\mathsf{OTHER}=\sum_i v_{iT_i}(\mathbf s_{-i},0_i)$.

Significance

The theorem shows that the price of truthfulness in combinatorial auctions with interdependent values grows only logarithmically in the number of signal values once values are concave in the agents' own signals, compared with the linear $(k+3)$ of the SOS mechanism. It also exhibits a decomposition of optimal welfare into a part driven by the other agents' signals (OTHER) and a part driven by the agent's own signal (SELF), each covered by a different randomized mechanism; this template recurs in later work on interdependent values.

The result is proved in the paper; no machine-checked version exists. Formalizing it fixes the exact model behind a proof that is stated in a few lines and checks it against the paper's own appendix: the printed display (9) omits a factor 2 (it fails for one agent with $v(\mathbf s)=s_1$, $k=4$, $s_1=3$), and the mission states the corrected inequality, which is the $d=1$ case of the paper's display (12) and is what the ratio $2\log_2 k$ requires.

Difficulty

The obvious route compares the mechanism's allocation with the optimal one agent by agent, but the mechanisms allocate by proxy values computed from modified signal profiles, and the optimal allocation's value at the true profile is not directly comparable with any single proxy. Covering SELF requires bounding an agent's own-signal contribution within a bucket by its value at the bucket floor, which needs concavity in the own signal and is false under SOS alone. Covering OTHER requires the Key Lemma 3.1 on random zeroing of signals. Incentive compatibility needs the argmax to be read off the proxy profile alone; an argmax with tie-breaking on the full report fails it.

Formalization scope

Signals are natural numbers and every hypothesis (nonnegativity, monotonicity, SOS, strong-SOS, the selectors' optimality) is quantified over the grid $\{0,\dots,k-1\}^n$ only. $k=2^q$ with $\log_2 k=q$ is a disclosed reading: the buckets cover $\{1,\dots,k-1\}$ only for powers of two. The empty bundle is worth $0$, and the monotonicity clauses apply to nonempty bundles. The argmax of each mechanism is an arbitrary selector that sees only the bucket index (or $B$) and the proxy profile and returns a feasible maximizer; theorems quantify over all such selectors. Random Sampling zeroes all of $B$, the agent's own signal included (the paper's "$v_{ij}$" is read as $v_{iT}$). Expectations are finite uniform averages; at $q=0$ Lean's $0^{-1}=0$ makes the Random Bucket term vanish, matching $p_{RB}=0$.

The approximation is stated for every feasible allocation and with true values at the truthful profile, not with proxy values or a supremum; IC and IR are stated for each deterministic component, not for the mixture's expectation. Replacing the average over partitions by an existential, or the explicit payments by existence of payments, would not be this theorem.

The model layer (signal grid, combinatorial valuations, SOS, ex-post IC-IR, OTHER and SELF, Random Sampling) is shared with the companion missions and lives in InterdepSOS.KHL and InterdepSOS.RSV; strong-SOS, Random Bucket and k-SS are defined in InterdepSOS.KSS. Lemma 6.3 and the decomposition (7), which the proof uses, are posed in the companion mission on k-HL. Proofs of the milestones, and reusable lemmas on concavity in the own signal and on random zeroing, are welcome. The source is the arXiv v2 preprint; the journal version in Mathematics of Operations Research (2024) is not what the mission cites.

Selected references

• A. Eden, M. Feldman, A. Fiat, K. Goldner, A. R. Karlin, Combinatorial Auctions with Interdependent Valuations: SOS to the Rescue, arXiv:1903.08384v2, 2019. https://arxiv.org/abs/1903.08384v2
• P. Milgrom, R. Weber, A Theory of Auctions and Competitive Bidding, Econometrica 50(5), 1982. https://doi.org/10.2307/1911865
• P. Dasgupta, E. Maskin, Efficient Auctions, Quarterly Journal of Economics 115(2), 2000. https://doi.org/10.1162/003355300554737

Motivation

The stochastic block model (SBM), introduced by Holland, Laskey and Leinhardt (1983), is the standard random model for networks with community structure, and the basic benchmark for community-detection algorithms (Abbe 2018). In its two-community form the nodes are split into two equal halves, edges inside a half appear with probability $p$, and edges across with probability $q<p$. The task of exact recovery is to identify the hidden halves from the graph alone.

The maximum a posteriori estimator for this model is the minimum bisection problem (find a balanced cut with the fewest crossing edges), which is NP-hard in general. Abbe, Bandeira and Hall (2016) determined when it recovers the planted bisection, and showed that a semidefinite relaxation is as good as the integer program. Del Pia, Khajavirad and Kunisky (arXiv:2006.03213, Mathematics of Operations Research 2023) ask the same question for the cheapest standard relaxation: the metric linear programming relaxation, defined by triangle inequalities. This mission is their positive result in the very dense regime.

Setting

Let $V=\{1,\dots,n\}$ with $n$ even. A bisection is a partition $V=V_1\cup V_2$ with $|V_1|=|V_2|=n/2$. For a graph $G=(V,E)$ let $a_{ij}=1$ if $(i,j)\in E$ and $0$ otherwise. The metric relaxation (LP-P) is

the first constraint for all distinct $i,j,k$ with $i<j$, the second for all $i<j<k$, and $x_{ji}:=x_{ij}$. The cut vector $\bar x$ of a bisection has $\bar x_{ij}=0$ for $i,j$ on the same side and $\bar x_{ij}=1$ otherwise. (LP-P) recovers the planted bisection when $\bar x$ is its unique optimal solution.

In the Erdős–Rényi model $\mathcal G_{n,p}$ every pair of nodes is an edge independently with probability $p$. In the SBM $\mathcal G_{n,p,q}$ a bisection $V_1,V_2$ is first chosen uniformly at random; then pairs inside $V_1$ or inside $V_2$ are edges with probability $p$, pairs between them with probability $q$, all independently. $\mathcal G_{n,0,q}$ is the random bipartite graph across a random bisection. An event occurs with high probability (w.h.p.) if its probability tends to $1$ as $n\to\infty$. The graph is very dense when $p$ and $q$ are constants.

For a finite graph $G=(V,E)$ and $b\in\mathbb Z_{\ge0}^V$, a $b$-factor (or $f$-factor) is a set $F\subseteq E$ with exactly $b_v$ edges of $F$ at each node $v$; $N(U,U')$ counts edges with one endpoint in $U$ and one in $U'$; $d_{\min}$, $d_{\max}$ are the minimum and maximum degrees; and the node connectivity $\kappa(G)$ is the minimum number of nodes whose deletion disconnects $G$ (the number of nodes, for a complete graph).

Formalization targets

Goal: Theorem 6 (p. 15)

For constants $0<q<p<1$,

Milestones

1. Proposition 6 (p. 20): for $G\sim\mathcal G_{2m,0,q}$ there is $C>0$ with $d_{\max}\le qm+C\sqrt{m\log m}$ w.h.p.
2. Proposition 5 (p. 20; Schrijver, Cor. 21.4a): a bipartite graph has a $b$-factor iff $N(U,U)\ge b(U)-\frac12 b(V)$ for every $U\subseteq V$.
3. Proposition 3 (p. 14): there is $C_{\mathrm{reg},2}>0$ such that for every $q\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,0,q}$ is a subgraph of a regular bipartite graph with the same bipartition, of degree $d_{\mathrm{reg}}=\frac{qn}2+C_{\mathrm{reg},2}\sqrt{\frac n2\log\frac n2}$ (rounded down).
4. Proposition 8 (p. 24): for $G\sim\mathcal G_{n,p}$ there is $C>0$ with $d_{\min}\ge pn-C\sqrt{n\log n}$ w.h.p.
5. Proposition 9 (p. 24; Bollobás–Thomason): for $G\sim\mathcal G_{n,p}$, $\kappa(G)=d_{\min}$ w.h.p.
6. Proposition 7 (p. 24; Tutte's $f$-factor theorem).
7. Proposition 4 (p. 14): there is $C_{\mathrm{reg},1}>0$ such that for every $p\in(0,1)$, w.h.p. $G\sim\mathcal G_{n,p}$ contains a spanning regular subgraph of degree $d_{\mathrm{reg}}=pn-C_{\mathrm{reg},1}\sqrt{n\log n}$ (rounded up to an even integer).