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

The deterministic recovery criterion that the goal also depends on, Theorem 4 of the paper (regular sandwiching with $d_{\mathrm{in}}-d_{\mathrm{out}}\ge n/4$), is the goal of mission 3 of this series and is not restated here.

Significance

The result. Theorem 6 is the only positive recovery guarantee for the metric LP in the random setting of the paper. Together with the failure results of Theorems 7 and 8 (missions 6 and 7), it locates the LP strictly between trivial and information-theoretically optimal: it recovers in a region of constant $p,q$, but not up to the threshold $p>q$ that the minimum bisection problem and its SDP relaxation reach. Propositions 3 and 4, that dense random graphs sit inside, and contain, regular graphs of nearly their average degree, are of independent interest in random graph theory, as the authors note.

Formalizing it. The result is proved in the paper; none of it is machine-checked. The mission also requires three classical theorems that are not in Mathlib: the $b$-factor criterion for bipartite graphs, Tutte's $f$-factor theorem (Mathlib has only the perfect-matching case $f\equiv 1$), and the Bollobás–Thomason theorem $\kappa=d_{\min}$ for random graphs, together with degree concentration for $\mathcal G_{n,p}$ and the bipartite SBM. Each is reusable well beyond this paper.

Difficulty

The obvious argument for recovery is to exhibit a dual certificate for (LP-P), which needs regularity of the communities and of the cross edges; a random graph is not regular. The paper bridges the gap by sandwiching the random graph between regular graphs of nearly equal degree, and that step is where the difficulty lies: the existence of a regular sub- or supergraph is a global combinatorial property, characterized by factor theorems with exponentially many conditions, each of which must hold simultaneously with high probability. Degree concentration alone, the first idea, controls only the singleton conditions. Tutte's $f$-factor theorem and the bipartite $b$-factor criterion are themselves substantial combinatorial theorems, and the connectivity statement of Bollobás and Thomason is a deep result on random graphs.

Formalization scope

Nodes are Fin n (0-based). A bisection is a Finset $V_1$ with $2|V_1|=n$. Points of $\mathbb R^{\binom n2}$ are symmetric arrays with zero diagonal; (LP-P) has no box constraints $0\le x\le1$ (they are implied by the constraints and adding them would change the LP). Recovery means: $\bar x$ is optimal and every optimal solution equals $\bar x$.

The random-graph laws are finite: a probability is a weighted sum over all graphs on Fin n, with independent edge weights, and for the SBM an average over all bisections; the event may depend on the drawn bisection. Edge probabilities are clamped into $[0,1]$, which is the identity on the parameters used here. "With high probability" is Tendsto … atTop (𝓝 1), along $n=2m$ for the SBM. The standing assumption $p>q$ is not built into the law, so that $\mathcal G_{n,0,q}$ is the case $p=0$.

Disclosed readings: the printed $d_{\mathrm{reg}}$ of Propositions 3 and 4 is not an integer; Proposition 3 is posed with degree $\lfloor d_{\mathrm{reg}}\rfloor$ and Proposition 4 with $2\lceil d_{\mathrm{reg}}/2\rceil$, the least even integer $\ge d_{\mathrm{reg}}$ (the proof assumes $d_{\mathrm{reg}}$ even). $\kappa(K_n)=n$ as on p. 24. Quantifier order follows each page: in Propositions 3 and 4 the constant precedes the probability parameter, in Propositions 6 and 8 it follows it; no constant depends on $n$.

A statement in which "with high probability" is replaced by a positive probability or an eventual bound, in which the bisection is fixed rather than random, or in which the regular degree is compared with an irrational real (an empty event) is not this mission's target.

Infrastructure needed: the finite random-graph laws, Hoeffding-type concentration over them, the two factor theorems, and node connectivity. Proofs of any milestone, and of the classical results as general graph theory, are welcome.

Selected references

• A. Del Pia, A. Khajavirad, D. Kunisky, Linear Programming and Community Detection, Mathematics of Operations Research, 2023; arXiv:2006.03213v2. https://arxiv.org/abs/2006.03213
• E. Abbe, A. S. Bandeira, G. Hall, Exact Recovery in the Stochastic Block Model, IEEE Transactions on Information Theory 62(1), 2016. https://arxiv.org/abs/1405.3267
• E. Abbe, Community Detection and Stochastic Block Models: Recent Developments, Journal of Machine Learning Research 18, 2018. https://arxiv.org/abs/1703.10146
• P. W. Holland, K. B. Laskey, S. Leinhardt, Stochastic Blockmodels: First Steps, Social Networks 5(2), 1983. https://doi.org/10.1016/0378-8733(83)90021-7
• W. T. Tutte, The Factors of Graphs, Canadian Journal of Mathematics 4, 1952. https://doi.org/10.4153/CJM-1952-028-2
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003 (Corollary 21.4a).
• B. Bollobás, A. Thomason, Random Graphs of Small Order, in Random Graphs '83, North-Holland Mathematics Studies 118, 1985 (Theorem 1).
• A. Frieze, M. Karoński, Introduction to Random Graphs, Cambridge University Press, 2016 (Chapter 3). https://doi.org/10.1017/CBO9781316339831

Motivation

In hiring, admissions and procurement, candidates are often judged by scores that are known to be biased: two candidates from different groups, schools or evaluation pipelines cannot be compared by their observed scores, while two candidates from the same pipeline can. Salem and Gupta (SSRN 3444283, published in Management Science, 2023) model this situation as a poset secretary problem. The decision maker sees only a partial order between candidates, namely the comparisons that are trustworthy, and must still make irrevocable online selections.

The classical secretary problem and its $k$-selection variant (Kleinberg, 2005) assume a total order. With only partial comparisons, the natural question is how much the missing comparisons cost. Salem and Gupta answer it in terms of the width of the poset. This mission formalizes their lower bound: no algorithm can do better than a factor of the width.

Setting

A finite set $\mathcal C$ of $N$ candidates carries a partial order $\preceq$. Each candidate $a$ has a true score $w(a)$. The scores are nonnegative and pairwise distinct, and they are consistent with the order: $a\prec b$ implies $w(a)<w(b)$. The pair $\mathcal I=(\mathcal P,w)$ is an instance. Candidates arrive in uniformly random order. An algorithm knows $N$ and a capacity $k$, observes the comparisons of $\mathcal P$ among the candidates that have arrived, and selects at most $k$ candidates, irrevocably. It never observes the scores.

The offline optimum is

An algorithm is $\alpha$-competitive if $\mathbb E[w(\mathsf{Alg}(\mathcal I))]\ge\mathrm{OPT}(\mathcal I)/\alpha$ on every instance (Definition 3.4).

The width $\omega$ of $\mathcal P$ is the largest number of pairwise incomparable candidates (an antichain).

Because an algorithm sees only the poset and the arrival order, on a fixed poset its randomness (arrival order and internal coins) induces a probability distribution $\mu$ on the selected set, supported on sets of at most $k$ elements, and $\mu$ does not depend on the scores. Such a $\mu$ is called a selection rule with capacity $k$. Its expected score is $\mathbb E_\mu[w(\mathrm{Alg})]=\sum_S\mu(S)\sum_{a\in S}w(a)$. The selection probability of $a$ is $p(a)=\sum_{S\ni a}\mu(S)$.

The instance of the lower bound is $\mathrm{Chains}(\omega,k)$: $\omega$ disjoint chains of $k$ elements each, with elements in different chains incomparable (Figure 8 of the paper, with $n=\omega k$).

Formalization targets

Goal: Proposition 5.1 (p. 14, proof in Appendix F, p. 42)

For every $k\ge1$ and $\omega\ge1$ there is a poset $\mathcal P$ of width $\omega$ such that for every selection rule $\mu$ with capacity $k$ and every $\varepsilon>0$ there is a consistent scoring $w$ with $\mathrm{OPT}(w,k)>0$ and

Equivalently, for every algorithm, $\sup_{\mathcal I}\mathrm{OPT}(\mathcal I)/\mathbb E[w(\mathsf{Alg}(\mathcal I))]\ge\omega$, the supremum taken over the scorings of $\mathcal P$.

Milestones (Appendix F, p. 42)

1. The width of $\mathrm{Chains}(\omega,k)$ is $\omega$ for $k\ge1$.
2. For every selection rule with capacity $k$ on $\mathrm{Chains}(\omega,k)$, some chain $i$ has $\sum_j p^i_j\le k/\omega$.
3. If $w$ is a consistent perturbation of the scoring that gives $M/k$ to each element of one chain $i_0$ and $0$ elsewhere, with perturbations below $M/2k$ in absolute value, nonnegative off $i_0$, and summing to $0$ on $i_0$, then $\mathrm{OPT}(w,k)=M$.
4. Given such a chain $i_0$, $M>0$ and $\varepsilon>0$, there is a consistent scoring with $\mathrm{OPT}=M$ and $\mathbb E_\mu[w(\mathrm{Alg})]\le(1+\varepsilon)\mathrm{OPT}/\omega$.

Significance

The result shows that the width of the poset is a genuine barrier: whatever the algorithm, an adversary choosing scores after seeing how the algorithm spreads its selections can force a ratio arbitrarily close to $\omega$. The paper's ProxyLabel algorithm has competitive ratio at most $e(\omega+1)/(1-1/k)^{k-1}\le e^2(\omega+1)$ when the width is known (Corollary 5.1, p. 15). Together the two results show that the best achievable competitive ratio in the poset secretary problem is of order $\omega$, which the paper calls order-optimal. The lower bound also covers the group-bias model of the paper: $\omega$ groups whose members are compared only within their group form exactly the instance used here.

On the formal side, the result is proved in the paper but has no machine-checked proof. The mission produces a formal model of score-independent randomized selection on a finite poset, a formal offline optimum with $k$ selections, and the width of a disjoint union of chains. These can be reused for other lower bounds in online selection.

Difficulty

The argument is short, and the work lies in getting the quantifiers and the encoding right. The printed statement places "there is an instance" before "for any algorithm". Read literally this is false for $\omega\ge2$: on a fixed instance, the algorithm that always selects the $k$ highest-scoring elements achieves ratio $1$. The proof establishes the other order: the poset is fixed, then the algorithm, then the scoring. A formalization must keep the scoring chosen after the algorithm while preventing the algorithm from depending on the scores.

The printed chain of inequalities also needs care. Its middle step drops the term $\sum_j p^\omega_j\varepsilon^\omega_j$, which the stated constraints on the perturbation do not make nonpositive. The bound therefore holds for perturbations chosen small enough, not for every perturbation satisfying the printed constraints. The existence of distinct, order-consistent scores meeting all the constraints at once has to be shown, and so does the identification of the optimum with the heavy chain.

Formalization scope

Elements form a finite type with a partial order. A consistent scoring is a function to $\mathbb R$ that is nonnegative, injective and strictly monotone ($a<b\Rightarrow w(a)<w(b)$). These are the standing assumptions of the model (§3.1, p. 7), not additions. $\mathrm{OPT}$ is a finite maximum over subsets of at most $k$ elements. Width is the published definition AppliedComb.Posets.width, the size of a largest antichain, not a minimum number of chains, so the width milestone is a real claim. Algorithms are represented by selection rules: nonnegative weights on subsets summing to $1$ and vanishing on subsets of more than $k$ elements. This class contains the selected-set law of every online algorithm, so a lower bound for it is a lower bound for online algorithms. Expectations and probabilities are finite sums. Competitiveness is stated as $\mathbb E\le(1+\varepsilon)\mathrm{OPT}/\omega$ together with $\mathrm{OPT}>0$, with no division by an expectation that may vanish. The hypotheses $k\ge1$ and $\omega\ge1$ are standing: with $\omega=0$ the poset is empty, and with $k=0$ every ratio is $0/0$. The instance is the sigma type $\Sigma\,(i:\mathrm{Fin}\,\omega),\mathrm{Fin}\,k$ with Mathlib's disjoint order.

Trivializing formalizations are ruled out explicitly. A selection rule must have total mass $1$, so the zero rule does not make the expected score vanish. It must respect the capacity, so the rule selecting everything is excluded. The scoring is quantified after the selection rule, never before it and never as an input to it. $\mathrm{OPT}>0$ is part of the conclusion.

The development needs finite sums over subsets, the order on sigma types, and antichains. Contributions are welcome on any milestone. The width of a disjoint union of chains and the pigeonhole bound on selection probabilities are reusable beyond this mission.

Selected references

• J. Salem and S. Gupta, Secretary Problems with Biased Evaluations Using Partial Ordinal Information, Management Science, 2023. Preprint: SSRN 3444283 (version of 2022-04-17), https://ssrn.com/abstract=3444283. Published version: https://doi.org/10.1287/mnsc.2023.4926
• R. Kleinberg, A multiple-choice secretary algorithm with applications to online auctions, Proceedings of SODA, 2005. https://dl.acm.org/doi/10.5555/1070432.1070519
• R. P. Dilworth, A decomposition theorem for partially ordered sets, Annals of Mathematics 51(1), 1950. https://doi.org/10.2307/1969503

Why minimum bisection recovery matters

The minimum bisection problem partitions an even-sized graph into two equally large groups while cutting as few edges as possible. In community detection, a graph may have been generated around an unknown, balanced pair of groups. The statistical question is whether an optimizer can identify that planted partition from the edges. Before studying random graph models or relaxations, it is useful to know which properties of a single observed graph suffice for recovery and whether those properties can be weakened.

Del Pia, Khajavirad and Kunisky express a deterministic sufficient condition through two vertex-degree parameters. Their Theorem 1 says that minimum bisection recovers the planted partition when the smallest within-community degree exceeds the largest cross-community degree by more than $n/4-1$. Theorem 2 supplies graphs at or below that boundary where recovery fails. Thus the degree difference has a sharp worst-case boundary within the theorem's stated size and degree ranges. This mission formalizes that second, tightness result.

Graphs, bisections, and degrees

Let $G=(V,E)$ be a simple undirected graph with $n$ vertices. A bisection is a partition $V_1,V_2$ of $V$ with $|V_1|=|V_2|=n/2$. Its cut cost is the number of edges with one endpoint in each side. The planted bisection is a designated partition regarded as the answer the optimizer should recover. Since exchanging $V_1$ and $V_2$ leaves the partition unchanged, uniqueness is always understood up to this exchange.