Combinatorics

Establish a separation exponent of at least $2.05$ between block sensitivity and sensitivity of total Boolean functions.

The target is an infinite family $f_k:\{0,1\}^{n_k}\to\{0,1\}$ such that

Here $o(1)$ tends to zero with $k$. Sensitivity is the maximum number of individual coordinate flips that change the output at a common input; block sensitivity allows pairwise disjoint nonempty sets of coordinates instead. Both maxima range over all inputs.

The Lean goal uses the campaign’s shared definition: for every $\varepsilon>0$ and every integer $S\ge2$, there must be a total Boolean function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.05-\varepsilon}$. The decimal $2.05$ means exactly $41/20$.

One sufficient route is a finite function $f$, an input $x$, and integers $A,B>1$ satisfying

The proved theorem SensitivityCampaign.finite_certificate then gives the asymptotic conclusion. Direct family constructions are equally welcome.

The starting milestone is the campaign’s proved exponent $2.0205$. The target $2.05$ is a challenge to prove, not an established campaign record. Further background and construction parameters appear in the campaign proposal.

Establish the separation exponent $\alpha\ge2.007$ for total Boolean functions, improving on the depth-20 specialization of OpenAI's construction.

Precisely, for every $\varepsilon>0$ and every integer $S\ge2$, construct a function $f$ with $s(f)\ge S$ and $bs(f)\ge s(f)^{2.007-\varepsilon}$.

A finite certificate is sufficient: supply a function and an input $x$ with $s(f)\le A$, $bs(f,x)\ge B$, $A,B>1$, and $A^{2.007}\le B$, then apply the shared certificate theorem. Sharper estimates, improved parameters, and different constructions are all eligible; direct family proofs are also welcome.

This is an open research target. The preceding benchmarks are $2$ classically and approximately $2.006470828$ from the depth-20 seed. Numerical searches guide discovery but do not replace certified bounds. Intermediate improvements are welcome as separate campaign entries.

Certify $\alpha\ge2.006470828$ by specializing OpenAI's general seed theorem to $d=20$ and $M=9^{21}$.

The construction gives

Here $bs(f,0)$ is block sensitivity at the all-zero input. The ratio $\log B/\log A$ is approximately $2.006470828227379\ldots$. Prove the exact inequality $A^{2.006470828}\le B$, then reuse the foundation's finite-certificate theorem.

The goal uses the campaign's shared definitions and requires arbitrarily large sensitivity. This is a stronger specialization of the existing construction, not a claim of a new construction or global parameter optimality.

Motivation

The discrete optimal transport problem between two histograms is a linear program, and much of the algorithmic theory of optimal transport is the theory of solving that linear program well. Chapter 3 of Peyré and Cuturi's Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019) surveys the classical combinatorial solvers: the network simplex, dual ascent methods, and the auction algorithm. Dual ascent methods work entirely with the dual variables, the Kantorovich potentials $(f, g)$: they keep a feasible pair of potentials and improve it step by step until it is optimal. The specialisation of this idea to assignment problems is the Hungarian algorithm of Kuhn (1955), and its general form is the primal-dual method for network flow problems presented in Bertsimas and Tsitsiklis, Introduction to Linear Optimization (1997, §7.7), on which §3.6 of the book is modelled.

The mathematical engine of every dual ascent method is one alternative: a feasible pair of potentials is either already optimal, or it can be improved along a direction of a very special, combinatorial form. This mission formalizes that alternative (Proposition 3.6 of the book) together with the results it rests on.

Setting

Fix integers $n, m \ge 1$, a cost matrix $C \in \mathbb{R}^{n\times m}$, and two histograms $a \in \Sigma_n$, $b \in \Sigma_m$, where $\Sigma_n = \{a \in \mathbb{R}^n_+ : \sum_i a_i = 1\}$ is the probability simplex. Write $[\![n]\!] = \{1, \dots, n\}$ for the row indices and, following the book, $[\![m]\!]' = \{1', \dots, m'\}$ for the column indices.

The couplings between $a$ and $b$ form the transportation polytope

and the primal problem is $\mathrm{L}_C(a,b) = \min_{P\in U(a,b)} \langle C, P\rangle$ with $\langle C, P\rangle = \sum_{i,j} C_{i,j}P_{i,j}$. A pair of vectors $(f, g) \in \mathbb{R}^n \times \mathbb{R}^m$ is dual feasible, written $(f,g) \in R(C)$, when $f_i + g_j \le C_{i,j}$ for all $(i, j)$. The dual problem (3.4) is

For a feasible pair $(f, g)$, a pair of indices $(i, j')$ is balanced if $f_i + g_j = C_{i,j}$ and inactive if $f_i + g_j < C_{i,j}$. A matrix $P$ and a pair $(f, g)$ are complementary if $P_{i,j} > 0$ implies $C_{i,j} = f_i + g_j$, that is, $P$ is supported on balanced pairs. For $S \subset [\![n]\!]$ the vector $\mathbb{1}_S \in \mathbb{R}^n$ has ones at the indices in $S$ and zeros elsewhere; likewise $\mathbb{1}_{S'} \in \mathbb{R}^m$ for $S' \subset [\![m]\!]'$.

Formalization targets

Goal: Proposition 3.6 (p. 416)

For $a \in \Sigma_n$, $b \in \Sigma_m$ and $(f,g) \in R(C)$: either $(f, g)$ is optimal for (3.4), or there exist $S \subset [\![n]\!]$, $S' \subset [\![m]\!]'$ and $\varepsilon_0 > 0$ such that for every $0 < \varepsilon \le \varepsilon_0$,

Milestones

1. Proposition 3.3 (p. 405). If $P \in U(a,b)$ and $(f,g) \in R(C)$ are complementary, then $P$ is primal optimal and $(f,g)$ is dual optimal.
2. Proposition 3.5 (p. 415). If every balanced pair $(i, j')$ with $i \in S$ has $j' \in S'$, then $(f,g) + \varepsilon(\mathbb{1}_S, -\mathbb{1}_{S'}) \in R(C)$ for all sufficiently small $\varepsilon > 0$.
3. Objective change (proof of Proposition 3.6, pp. 416–417). The step changes the dual objective by exactly $\varepsilon(\mathbb{1}_S^{\mathsf T}a - \mathbb{1}_{S'}^{\mathsf T}b)$.
4. Labeled sets (proof of Proposition 3.6, pp. 416–417). If no coupling in $U(a,b)$ is complementary to $(f,g)$, then there are $S, S'$ with every balanced pair leaving $S$ landing in $S'$, and

Significance

The result. Proposition 3.6 says that non-optimality of a feasible dual pair is always witnessed by a direction with entries in $\{0, \pm 1\}$, determined by two index sets, which keeps the pair feasible for a positive step and strictly improves the objective. This is what makes dual ascent a finite combinatorial method rather than a generic linear-programming iteration: the search for an ascent direction reduces to a maximum-flow computation on the bipartite graph of balanced pairs. Combined with the step length of Proposition 3.5, it is the primal-dual method, which reduces to the Hungarian algorithm on assignment problems. Milestone 1 is the optimality certificate of complementary slackness, used throughout the book's chapter 3.

Formalizing it. These results are classical and proved in the book and in Bertsimas and Tsitsiklis; no machine-checked proof of them is known to exist. The mission produces a formal statement and proof of the optimality-or-ascent alternative for the discrete Kantorovich dual, together with the complementary-slackness certificate in the transport setting. Milestone 4 is a Hall-type statement (a supply–demand theorem on a bipartite graph) whose formal proof is reusable for other matching and transportation results.

Difficulty

Milestones 1–3 are short computations. The content of the goal is in milestone 4. The obvious argument is linear-programming duality: if $(f,g)$ is not optimal, some feasible direction improves the objective. But LP duality only produces an arbitrary real direction; the claim that a direction of the form $(\mathbb{1}_S, -\mathbb{1}_{S'})$ suffices is a combinatorial statement. The book obtains $S, S'$ as the labeled nodes of a maximal flow (Ford–Fulkerson) and argues through max-flow/min-cut; the flow bookkeeping printed on p. 417 is garbled, so the step from "no complementary coupling exists" to "$\mathbb{1}_S^{\mathsf T}a > \mathbb{1}_{S'}^{\mathsf T}b$ for a set closed under balanced edges" has to be supplied carefully. Separately, connecting "not optimal" to "no complementary coupling exists" needs the converse direction of complementary slackness or strong duality for the transport problem.

Formalization scope

Row and column indices are Fin n and Fin m (0-based); the primed column set $[\![m]\!]'$ is just Fin m. Cost matrices and couplings are Matrix (Fin n) (Fin m) ℝ; histograms and potentials are real functions on Fin n, Fin m; $\Sigma_n$ is Mathlib's stdSimplex ℝ (Fin n). Index sets $S, S'$ are Finsets and $\mathbb{1}_S$ is indicatorVec S. "Optimal for Problem (3.4)" is the predicate IsDualOptimal: feasible, and no feasible pair has a larger objective (no real infimum or supremum is used, so no junk value can enter). The book's "for a small enough $\varepsilon > 0$" is stated as "for every $\varepsilon \in (0, \varepsilon_0]$", which is equivalent because $R(C)$ is convex and the objective is linear.

Standing assumptions, all from the book: $(f, g)$ is dual feasible (p. 415, "In what follows, $(f,g)$ is a feasible dual pair in $R(C)$"); $a, b$ are histograms in the simplex (used for the goal and milestone 4; without equal masses the dual is unbounded and optimality fails for every pair). Milestone 4 replaces the book's flow hypothesis "the throughput is strictly smaller than 1" by the equivalent flow-free statement "no coupling in $U(a,b)$ is complementary to $(f,g)$"; flows, capacities and the labeling algorithm appear in no statement.

The goal admits a trivializing formalization: allowing an arbitrary direction $(u, v)$ instead of $(\mathbb{1}_S, -\mathbb{1}_{S'})$ turns Proposition 3.6 into plain non-optimality of a linear program. The statement here fixes the direction to $(\mathbb{1}_S, -\mathbb{1}_{S'})$ exactly as the book does.

A complete development needs finite LP duality or complementary slackness for the transportation problem, and a max-flow/min-cut or Hall-type theorem on bipartite graphs with vertex capacities. Both are reusable well beyond this mission. Contributions welcome: proofs of the milestones, a self-contained proof of milestone 4 by induction or by a max-flow argument, and alternative proofs of the goal through LP duality plus a vertex argument.

Selected references

• G. Peyré, M. Cuturi, Computational Optimal Transport, Foundations and Trends in Machine Learning 11(5–6):355–607, 2019. https://doi.org/10.1561/2200000073 (§3.1–3.3, §3.6, pp. 400–417)
• D. Bertsimas, J. N. Tsitsiklis, Introduction to Linear Optimization, Athena Scientific, 1997, §7.7 (the primal-dual method) and pp. 305–308 (Ford–Fulkerson and the labeling algorithm).
• H. W. Kuhn, The Hungarian method for the assignment problem, Naval Research Logistics Quarterly 2(1–2):83–97, 1955. https://doi.org/10.1002/nav.3800020109
• L. R. Ford, D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5

Motivation

A basic question of additive combinatorics asks how a set grows under repeated addition. If a finite set $A$ in an abelian group satisfies $|A + B| \le \alpha |A|$ for some finite set $B$, how large can the iterated sumsets $hB = B + \cdots + B$ be? Plünnecke's inequality gives the answer used throughout the subject: some nonempty part of $A$ grows by at most a factor $\alpha$ per added copy of $B$. Combined with Ruzsa's triangle inequality it becomes the Plünnecke–Ruzsa inequality $|mB - nB| \le \alpha^{m+n}|A|$, which underlies Freĭman-type structure theorems, sum–product estimates and the polynomial Freĭman–Ruzsa programme.

Timeline.

• 1970: H. Plünnecke proves the inequality for iterated sumsets in abelian groups with a graph-theoretic method (commutative layered graphs and Menger's theorem).
• 1989: I. Z. Ruzsa simplifies Plünnecke's argument and combines it with the triangle inequality to bound $|mB - nB|$.
• 2011: G. Petridis gives a short elementary proof, without graphs (arXiv:1101.3507, Combinatorica 32, 2012). His argument also shows that one subset $X \subseteq A$ works for every number of summands $h$, and it extends to triple products $CXB$ in non-abelian groups.

Setting

Let $G$ be a group with finite subsets $A$, $B$, $C$. The product set is $AB = \{ab : a \in A,\ b \in B\}$, and $|\cdot|$ denotes cardinality. In an abelian group, written additively, the sumset is $A + B = \{a + b : a \in A,\ b \in B\}$, and for $h \ge 0$ the iterated sumset $hB$ is $B + \cdots + B$ with $h$ summands, $0B = \{0\}$. It is not the dilate $\{hb : b \in B\}$.

A nonempty subset $X \subseteq A$ has minimal growth under $B$ if

Such an $X$ exists whenever $A$ is nonempty, since $A$ has finitely many subsets. In Lean, $G$ is a Group or AddCommGroup with decidable equality, the sets are Finset G with the pointwise operations of Mathlib (A * B, A + B, h • B), and cardinalities are #A cast to ℝ.

Formalization targets

Goal: Theorem 3.1

For finite $A$, $B$ in an abelian group with $A$ nonempty and $|A + B| \le \alpha|A|$, there is a nonempty $X \subseteq A$ with

The point is the order of quantifiers: one $X$ serves all $h$.

Milestones

1. Proposition 2.1 (p. 5). If $|XB|/|X| \le |ZB|/|Z|$ for every $Z \subseteq X$, then $|CXB| \le \frac{|XB|}{|X|}\,|CX|$ for every finite $C$, in any group. This is already on the platform, proved, as FamousTheorems.pluennecke_petridis (additive notation, cross-multiplied), and enters the mission as a reference.
2. Theorem 1.5 (p. 3). In any group, $|AB| \le \alpha|A|$ with $A$ nonempty gives a nonempty $X \subseteq A$ with

3. Inductive step of Theorem 3.1 (p. 7). For $X \subseteq A$ of minimal growth and $|A+B| \le \alpha|A|$:

Significance

Theorem 3.1 is the form of Plünnecke's inequality used in applications. Two consequences follow directly. Taking $A = B$ gives $|hB| \le \alpha^h|B|$ whenever $|2B| \le \alpha|B|$. Combining one $X$ for all $h$ with Ruzsa's triangle inequality gives $|mB - nB| \le \alpha^{m+n}|A|$ (Theorem 1.2 of the paper). With a separate $X$ for each $h$, the second step would need the same set for $m$ and $n$, and that is exactly what Theorem 3.1 provides. Theorem 1.5 is the non-abelian ingredient: missions 2 and 3 of this series apply it to obtain explicit Plünnecke-type bounds for $|B^h|$ and $|SB^h|$ in arbitrary groups.

Formalizing it. The results are proved and classical. Mathlib already contains Proposition 2.1 (Finset.pluennecke_petridis_inequality_mul) and the Plünnecke–Ruzsa inequality Finset.pluennecke_ruzsa_inequality_nsmul_sub_nsmul_add. Its proof runs through a private lemma that bounds $|X + hB|$ for one fixed minimiser, but no public statement in Mathlib or on the platform asserts Theorem 3.1 or Theorem 1.5 in the form "there exists a nonempty $X$ for all $h$" (respectively "for all $C$"). This mission adds those statements as reusable, citable nodes in the paper's numbering.

Difficulty

A first attempt iterates the hypothesis directly: $|A + 2B| \le \alpha|A + B|$ would follow if $A + B$ again grew by a factor $\alpha$ under $B$, but nothing controls the growth of $A + B$. The ratio $|ZB|/|Z|$ is not monotone in $Z$, and passing to subsets of $A$ can only help if the subset is chosen correctly. Choosing a different good subset for each $h$ gives Theorem 1.1 but loses the uniformity. The work is to show that one fixed subset controls all the products $CXB$ simultaneously, and in the non-abelian Theorem 1.5 to keep the order of the factors $C$, $X$, $B$ throughout.

Formalization scope

• Theorem 3.1 and the inductive step are stated in an AddCommGroup with DecidableEq. Theorem 1.5 is stated in a Group, with no commutativity, as on the page. The factor order $C \cdot X \cdot B$ is preserved.
• $hB$ is h • B (the $h$-fold sumset; 0 • B = {0}), and "for all $h$" ranges over all natural numbers, including the true case $h = 0$.
• $\alpha$ is an arbitrary real number; cardinalities are cast to ℝ. No hypothesis $\alpha \ge 1$ is added: it follows from the hypotheses once $A$ and $B$ are nonempty (with $B$ empty they force only $\alpha \ge 0$, and every conclusion is still true).
• Nonempty witness. The page says "there exists $X \subseteq A$". Since $\emptyset + hB = \emptyset$, the empty set would satisfy the printed statements trivially, and that formalization is ruled out: the goal and Theorem 1.5 assume $A$ nonempty and assert $X$ nonempty, matching the paper's choice of $X$ as a minimiser of a ratio defined on nonempty sets.
• Minimal growth in the step milestone is written cross-multiplied, $|X+B|\,|Z| \le |Z+B|\,|X|$, over nonempty $Z \subseteq A$; the step is stated for $h \ge 1$ with natural-number subtraction guarded by that hypothesis.
• Ruzsa's covering lemma and Ruzsa's triangle inequality, quoted in §4, are in Mathlib (Finset.ruzsa_covering_mul, Finset.ruzsa_triangle_inequality_mul_mulInv_mul) and are not items of this mission.
• No new definitions are needed. Welcome contributions: proofs of the three draft statements, and, separately, the deduction of Theorem 1.2 from Theorem 3.1.

Selected references

• G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, arXiv:1101.3507v3, 2011; Combinatorica 32 (2012). https://arxiv.org/abs/1101.3507 , https://doi.org/10.1007/s00493-012-2818-5
• H. Plünnecke, Eine zahlentheoretische Anwendung der Graphentheorie, J. Reine Angew. Math. 243 (1970) 171–183. https://doi.org/10.1515/crll.1970.243.171
• I. Z. Ruzsa, An application of graph theory to additive number theory, Scientia, Ser. A 3 (1989) 97–109 (no online version).
• T. Tao, V. Vu, Additive Combinatorics, Cambridge University Press, 2006. https://doi.org/10.1017/CBO9780511755149

Motivation

A committee that chooses one alternative by voting would like a voting procedure under which no member can gain by misreporting their preferences. Such a procedure is called strategy-proof. Gibbard (Econometrica 41, 1973) and Satterthwaite (J. Econ. Theory 10, 1975) proved independently that, once at least three outcomes are possible, the only strategy-proof procedures are dictatorial. The result is the starting point of the theory of strategy-proof mechanisms: it is why mechanism design restricts preference domains (single-peaked preferences, quasi-linear utilities) or allows randomization.

This mission formalizes Theorem 1 of Satterthwaite's paper, in the version circulated as Northwestern University CMS-EMS Discussion Paper No. 122 (revised December 12, 1974). Its formulation has one feature that the textbook version lacks: the hypothesis is on the range of the procedure, not on the whole alternative set, and the dictatorship is accordingly relative to that range.

Setting

A committee has a finite set $I_n$ of $n\ge 1$ individuals and a finite set $S_m$ of $m$ alternatives. In a strict committee every individual's ballot $B_i$ is a strong order on $S_m$, a ranking without ties; $x\,\bar B_i\,y$ means that $B_i$ ranks $x$ strictly above $y$. The set of strong orders is $\rho_m$, and a ballot set is $B=(B_1,\dots,B_n)\in\rho^n_m$.

A strict voting procedure $v^{nm}$ assigns to each ballot set a single alternative $v^{nm}(B)\in S_m$. Its range $T_p$ is the set of alternatives it selects at some ballot set, and $p=|T_p|$, so $1\le p\le m$.

Individual $i$ can manipulate $v^{nm}$ at $B$ if some ballot $B_i'$ gives

an outcome $i$ strictly prefers by the standard of the original ballot. The procedure is strategy-proof if no individual can manipulate it at any ballot set.

The procedure is dictatorial if some individual $i$ exists such that, at every ballot set $B$, $v^{nm}(B)$ is the element of the range $T_p$ that $B_i$ ranks highest. It is fully dictatorial if in addition $T_p=S_m$ and partially dictatorial if $T_p\subsetneq S_m$.

The proof uses three further notions. Condition U requires that if every $B_i$ ranks the same $x\in T_p$ above all other elements of $T_p$, then $v^{nm}(B)=x$. The procedure is weak alternative-excluding if $T_p\subsetneq S_m$, and strong alternative-excluding if in addition it satisfies Condition U. Finally $\theta_T(B_i)$ is the restriction of $B_i$ to a subset $T$.

Formalization targets

Goal: Theorem 1 (p. 11)

For a strict committee with $n\ge 1$ and $m\ge p\ge 3$,

Milestones

1. Lemma 1 (p. 13): a strategy-proof strict procedure satisfies Condition U.
2. Lemma 2 (p. 15): with one individual and three alternatives, a strategy-proof procedure is fully dictatorial or strong alternative-excluding.
3. Lemma 3 (pp. 16–17): for $n+1$ individuals and three alternatives, individuals $1,\dots,n$ cannot manipulate $v^{n+1,3}$ if and only if each of the procedures $B\mapsto v^{n+1,3}(B,B_{n+1})$, one for each ballot of individual $n+1$, is strategy-proof.
4. Lemma 4 (p. 22): the induction step from $n$ to $n+1$ individuals for three alternatives.
5. Lemma 5 (p. 25): for $n\ge 1$, $m\ge 3$, a strategy-proof procedure is fully dictatorial or strong alternative-excluding.
6. Lemma 6 (p. 26): for $n\ge 2$, if $\theta_{T}(C_i)=\theta_{T}(D_i)$ for all $i$, with $T=T_p$, then $v^{nm}(C)=v^{nm}(D)$.
7. Proof of Theorem 1, (27)–(28) (p. 27): in the case of a strategy-proof, strong alternative-excluding $v^{nm}$ with $m>p\ge 3$, it induces a strategy-proof procedure $v^{np}$ on the alternatives of its range with $v^{np}[\theta_T(B_1),\dots,\theta_T(B_n)]=v^{nm}(B)$.

Significance

Theorem 1 characterizes the strategy-proof strict voting procedures completely: given $p\ge 3$, they are exactly the procedures that let one individual pick, from a fixed menu $T_p$, their favourite element. The classical statement assumes the procedure can select every alternative; Theorem 1 shows that excluding alternatives from the menu does not help, since a procedure with any menu of at least three alternatives is still governed by one individual. The paper's correspondence theorem with Arrow's social welfare functions (its Theorem 2) and its extension to ballots with indifference (Theorem 1') build on this statement.

The full-range case is on the platform already: AGT.gibbard_satterthwaite (Theorem 9.8 of Nisan–Roughgarden–Tardos–Vazirani, Algorithmic Game Theory) is proved and states that an incentive compatible social choice function onto at least three alternatives has a dictator; it is included here as a reference item and is exactly the case $T_p=S_m$ of Lemma 5. The open item MechanismDesign.SocialChoice.gibbard_satterthwaite (Börgers, Proposition 8.1) poses the full-range equivalence. Theorem 1 contains both as the special case $T_p=S_m$. What this mission adds is the range-restricted statement and the paper's own route to it: the induction on the number of individuals for three alternatives (Lemmas 2–4) and the reduction of a procedure with a proper range to its range (Lemma 6 and (27)–(28)). The paper only sketches Lemma 4 and defers the induction on $m$ to Satterthwaite's dissertation, so the formal development fills these gaps.

Difficulty

The "if" direction is immediate. For the "only if" direction the natural first idea is to apply the full-range theorem to the procedure viewed as a map into $T_p$. This fails as stated: the procedure is still defined on rankings of all $m$ alternatives, and nothing yet says that its choice ignores how individuals rank alternatives outside $T_p$. That is the content of Lemma 6, which needs strategy-proofness and Condition U; only after it does the procedure factor through rankings of $T_p$, and only then is the factor itself strategy-proof. The full-range case itself is the classical theorem, whose known proofs (via Arrow's theorem, or by pivotal-voter arguments) are combinatorial and long.

Formalization scope

• Individuals and alternatives are finite types ι and A; $n$ = Fintype.card ι, $m$ = Fintype.card A, and the $n+1$ individuals of Lemmas 3–4 are Option ι, with none the individual $n+1$.
• Strict ballots and strategy-proofness come from the published definition agt_social (namespace AGT): a ballot is a relation r with IsStrictTotalOrder A r, r x y is the paper's $x\,\bar B_i\,y$, and strategy-proofness is AGT.IncentiveCompatible, which is the paper's definition (1) on $\rho^n_m$.
• The range is taken over strict ballot sets only, and $p$ is its Set.ncard. Theorem 1 assumes $n\ge 1$ and $p\ge 3$; $m\ge p$ holds automatically, so $m\ge 3$ is not a separate hypothesis.
• Dictatorial reads the paper's dictator function $f^i_T$ as "the $B_i$-maximal element of $T_p$", which for strong orders is unique.
• $\theta_T(C_i)=\theta_T(D_i)$ is encoded as agreement of the two strict relations on $T\times T$, and the procedure $v^{np}$ of (28) lives on the subtype of the range.
• Lemmas keep their printed hypotheses ($m\ge 3$, $p\ge 1$, Lemma 6's $n\ge 2$), even where the conclusion would hold without them. The range restriction milestone keeps the proof's case assumptions of strong alternative exclusion and $m>p\ge 3$.

Two encodings would trivialize the goal and are excluded: a range taken over all relation profiles (junk values would make $p\ge 3$ meaningless), and a dictatorship that only constrains ballot sets at which the dictator's overall favourite lies in $T_p$, or that asks for the dictator's favourite in all of $S_m$ (false whenever $T_p\subsetneq S_m$). The bound $p\ge 3$ is needed: a procedure with two possible outcomes, such as majority vote between two fixed alternatives, is strategy-proof and not dictatorial, and an imposed procedure ($p=1$) is dictatorial only vacuously.

Contributions are welcome at every milestone, and the restriction-to-range step (Lemma 6 and (27)–(28)) is reusable for any statement that transfers results from full-range to range-restricted procedures.

Selected references

• M. A. Satterthwaite, Strategy-proofness and Arrow's Conditions: Existence and Correspondence Theorems for Voting Procedures and Social Welfare Functions, Northwestern University CMS-EMS Discussion Paper No. 122, rev. Dec. 12, 1974; published in J. Econ. Theory 10(2) (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
• A. Gibbard, Manipulation of Voting Schemes: A General Result, Econometrica 41(4) (1973) 587–601. https://doi.org/10.2307/1914083
• N. Nisan, Introduction to Mechanism Design (for Computer Scientists), Chapter 9 of N. Nisan, T. Roughgarden, É. Tardos, V. V. Vazirani (eds.), Algorithmic Game Theory, Cambridge University Press, 2007. https://doi.org/10.1017/CBO9780511800481
• T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Chapter 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001

Motivation

An online learner predicts a binary label for each instance before seeing that instance's correct label. Its guarantee is usually measured by its worst possible number of mistakes against a target function. Such guarantees can differ greatly across target functions: an algorithm might learn one target quickly while taking much longer on another. Littlestone and Warmuth's analysis of the Weighted Majority Algorithm asks which collections of individual mistake guarantees can coexist for one deterministic learner. In Section 7 of their 1994 paper, they isolate a condition under which these guarantees obey a strict numerical constraint. The condition concerns how the target functions vary together over the instance domain, so the result applies without a probability distribution on instances or labels.

The theorem also supports the paper's comparison between arbitrary deterministic learners and Weighted Majority. Given individual mistake bounds, its inequality is the numerical condition that makes a suitable initial weighting of the target functions possible in Theorem 7.1 and Corollary 7.1 of the same paper. The present mission centers on the inequality itself, which is independent of a particular implementation of Weighted Majority.

Setting

Let $X$ be an instance domain, possibly finite or infinite, and let $\varphi_1,\ldots,\varphi_n:X\to\{0,1\}$ be a finite family of target functions. A trial presents an instance $x\in X$ to a learner, asks it to predict either $0$ or $1$, and then reveals a label. A finite sequence is consistent with $\varphi_i$ when each revealed label equals $\varphi_i(x)$ at that trial's instance. The learner may use the current instance and the complete history of earlier labeled trials when predicting; it does not see the current label first. No sampling or independence assumption is made.

The family is shattered by its domain when every pattern $b=(b_1,\ldots,b_n)\in\{0,1\}^n$ appears as the vector of function values at some instance:

This is a dual notion of shattering. The familiar VC condition asks whether a class of functions realizes every labeling of chosen instances. Here the domain realizes every joint value pattern of a chosen family of functions. The two conditions should not be interchanged.

Let $A$ be any deterministic online learner. Write $M_i$ for the supremum of the number of mistakes made by $A$ over every finite sequence consistent with $\varphi_i$. Since mistake counts are natural numbers, a finite supremum is an attained natural-number maximum. The theorem assumes each $M_i$ is finite. In the Lean representation, this is a separate finiteness condition on each target's extended-natural mistake bound.

Formalization targets

Strict constraint on individual mistake bounds

The goal is Theorem 7.2 of Littlestone and Warmuth, pp. 244–245. For every domain, every finite family shattered by that domain, and every deterministic online learner with finite individual mistake bounds,

The inequality is strict. Replacing it by a weak inequality would lose the stated result and the threshold used in the paper's later comparison with Weighted Majority. The theorem quantifies over the learner itself; it does not select a specially behaved learning rule.

Arithmetic milestones

Lemma 7.1 concerns positive real numbers with integral adjacent quotients. When a positive target $s$ is no larger than their sum and $s/r_1$ is integral, some prefix sums exactly to $s$. Lemma 7.2 concerns positive powers of two with integer exponents. If a power $2^\ell$ lies at least as high as each individual weight and at most as high as the total weight, some subset sums exactly to $2^\ell$. Both statements and their exact source wording are recorded as the mission's milestones; they are the numbered arithmetic results used in Theorem 7.2.

Significance

The theorem limits the set of claims that one deterministic learner can make simultaneously. Small $M_i$ contribute large terms to the sum, so a learner cannot have arbitrarily small worst-case mistake counts for all members of a domain-shattered family. This is a worst-case statement about every finite consistent trial sequence, rather than an average-case statement about a chosen data distribution. The paper's Corollary 7.1 uses the resulting inequality to select initial weights for a Weighted Majority comparison, but that later algorithmic statement is outside this mission's goal.

Formalizing this result adds a reusable dual-shattering predicate and an exact constraint on per-target online mistake bounds to the existing online-learning definitions. The paper proves the theorem, while the mission's Lean goal and its two milestone lemmas are open proof obligations. The separate published online-learning module provides the definitions of deterministic predictors, trial histories, mistake counts, and extended-natural worst-case bounds; it does not already prove this theorem.

Difficulty

For a single target, an arbitrary learner may have a small finite mistake bound. The difficulty is relating those bounds across different targets without placing extra restrictions on the learner. Domain shattering gives the adversary control over the simultaneous predictions of all functions at an instance, but the labels of one trial sequence must still remain consistent with a target. A simple count of targets or of possible patterns does not directly produce the strict weighted sum, particularly when the different $M_i$ are unequal. The two arithmetic lemmas address exact sums of structured weights; the main theorem must also connect such weights to the learner's worst-case mistakes.

Formalization scope

The function family is indexed by Fin n, with zero-based Lean indices corresponding to the paper's $1,\ldots,n$. The domain $X$ is an arbitrary type and may be infinite. Labels and predictions are Bool. ShatteredByDomain states that every Boolean pattern is realized by some domain point. The published UnderstandingML_Online definition gives OnlineAlg X Bool, finite trial histories, mistakes, and mistakeBound. The latter is valued in $\mathbb N\cup\{\infty\}$ and ranges over all finite sequences labeled by the target. Each $M_i$ is converted to a natural number only after assuming its bound is finite. The powers $2^{-M_i}$ and their finite sum are real numbers. The $n=0$ conclusion is the empty sum $0<2$; the shattering predicate itself then requires an instance to realize the unique empty pattern.

The two milestones use real-valued weights. Lemma 7.1 assumes $n\ge1$ because the source refers to $r_1$. Lemma 7.2 represents the source's integral base-two logarithms by equations $r_i=2^{k_i}$ with integer $k_i$, which also enforce positivity. Its maximum hypothesis is written pointwise, so an empty family is harmless: the other inequality $2^\ell\le0$ cannot hold. A coordinate family on $X=\{0,1\}^n$ is verified locally to satisfy the shattering predicate, ruling out a vacuous encoding of that central assumption. Contributions proving either arithmetic milestone or the main theorem within these exact definitions are in scope.

Selected references

• Nick Littlestone and Manfred K. Warmuth, The Weighted Majority Algorithm, Information and Computation 108(2), 212–261, 1994. DOI: 10.1006/inco.1994.1009.
• Shai Shalev-Shwartz and Shai Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 21. DOI: 10.1017/CBO9781107298019.

Motivation

The Chinese postman problem, posed by Meigu Guan (Kwan Mei-Ko) in 1962, asks for a shortest closed walk in a graph that traverses every edge at least once: the route of a postman who must cover every street and return to the post office. It is the basic model of arc routing (street sweeping, snow ploughing, meter reading, inspection of networks), and it is one of the first combinatorial optimization problems shown to be solvable in polynomial time by matching methods.

Edmonds and Johnson, Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), reduce the postman problem to a parity problem: choose nonnegative integers $x_e$, the number of extra traversals of each edge, so that every node becomes even, at minimum total length. Their §3 gives a complete linear description of this parity problem. The description is the first instance of what is now called the $T$-join polyhedron (with $T$ the set of odd-degree nodes), a standard object of polyhedral combinatorics and a frequent example of total dual integrality.

Timeline:

• 1962: Guan states the postman problem and an optimality criterion for it.
• 1965: Edmonds proves the matching polyhedron theorem and gives the blossom algorithm for weighted matching (Edmonds 1965).
• 1973: Edmonds and Johnson specialise both to the postman problem, giving the polyhedron in the edge variables alone (this mission) and a blossom algorithm that solves it (Edmonds–Johnson 1973).

Setting

A graph $G$ has a finite set $N$ of nodes and a finite set $E$ of edges; each edge meets two different nodes, and several edges may meet the same pair of nodes. The degree of a node $n$ is the number of edges meeting it, $\sum_{e\in E} a_{ne}$, where $a_{ne}=1$ if $e$ meets $n$ and $0$ otherwise. Set $b_n=1$ when the degree of $n$ is odd (an odd node) and $b_n=0$ otherwise.

An edge $e$ meets a set $S\subseteq N$ when exactly one of its two ends lies in $S$. A set $S\subseteq N$ is an odd set when it contains an odd number of odd nodes, and any number of even nodes.

The parity points $X\subseteq\mathbb R^E$ are the vectors with

the conditions (3.1), (3.2), (3.6) of the paper. Adding $x_e$ copies of each edge $e$ to $G$ makes every degree even, and an Euler tour of the enlarged graph is a postman tour of $G$. The postman polyhedron is

the conditions (3.2) and (3.5). For lengths $c\in\mathbb R^E$ the objective is $z=\sum_e c_e x_e$. The dual linear program has a variable $y_S$ for each odd set, constraints $y_S\ge 0$ and $\sum\{y_S: e\text{ meets }S\}\le c_e$, and objective $v=\sum_S y_S$.

Formalization targets

Goal: the polyhedron theorem (p. 93)

Both inclusions are claimed. The equality is between subsets of $\mathbb R^E$, so it also asserts that the convex hull of $X$ is closed.

Milestones

In the paper's order of argument:

1. (3.13), p. 95: an integer solution of (3.6) has $\sum\{x_e : e\text{ meets }S\}\equiv 1 \pmod 2$ for every odd set $S$.
2. p. 95: $\operatorname{conv}X\subseteq P$.
3. (3.10), p. 94: weak duality, $v\le z$ for $x\in P$ and $y$ dual feasible.
4. (3.11)–(3.12), p. 95: complementary slackness makes $x$ and $y$ optimal.
5. p. 95: for $c\ge 0$ there is an integral parity point $x$ and a dual feasible $y$ satisfying (3.11) and (3.12). The paper proves this with the algorithm of §4.
6. p. 96: if some $c_e<0$, $z$ is unbounded below on $P$ and on $X$.
7. (3.19), p. 96: for $c\ge 0$, the minimum of $z$ over $P$ is attained at a parity point.

There are two companion statements. The first (pp. 93–94) says that in $\sum_e a_{ne}x_e-2w_n=b_n$ with $x\ge 0$, integrality of $w_n$ already forces $w_n\ge 0$. The second (p. 91) is the polyhedron theorem in the variables $(x,w)$: the convex hull of the integer solutions of (3.1)–(3.3) is the set of solutions of (3.2), (3.2′), (3.3), (3.5).

Significance

The theorem turns the parity problem, an integer program, into a linear program over an explicitly described polyhedron. Optimal postman tours therefore come with dual certificates: a packing of odd cuts whose total value matches the tour's extra length. The same description underlies the theory of $T$-joins and $T$-cuts (Schrijver 2003, Chapter 29).

No machine-checked proof of the $T$-join polyhedron theorem exists, on Prove2Me or, to our knowledge, in Mathlib. This mission states it in the multigraph setting of the paper. Milestones 1–4 and 6 are elementary and can serve as warm-ups. Milestone 5, total dual integrality of the odd-cut system, is the substantive step. The paper obtains it from a blossom algorithm; the milestone is stated as an existence result, so any proof of it closes it.

Difficulty

The inclusion $\operatorname{conv}X\subseteq P$ is a parity count. The reverse inclusion is the theorem. Two first ideas fail. Total unimodularity does not apply, because the odd-cut constraint matrix is not totally unimodular and $P$ has many constraints whose tightness interacts. Reading the result off the matching polyhedron theorem needs the auxiliary loops $w_n$ and an elimination step, and the 1965 matching polyhedron describes perfect matchings of a simple graph, not this parity system on a multigraph. Some argument for integrality of the minimum for every $c\ge 0$ is needed, and the paper's is an algorithm with a dual certificate. A further point is that $P$ and $X$ are unbounded: equality of hulls is not just agreement of minima over bounded objectives, and the case of objectives with a negative coefficient has to be handled separately (milestone 6).

Formalization scope

A graph is the local ChinesePostman.Polyhedron.Graph V E: a map ends : E → Sym2 V with a proof that no edge is a loop, over finite types V and E. Mathlib's SimpleGraph is not used, because the paper allows parallel edges. Degrees, odd nodes and $b_n$ are computed from the graph; the set of odd nodes is never a free parameter. "$e$ meets $S$" means exactly one end in $S$. Odd sets range over all subsets $S\subseteq N$ with an odd number of odd nodes, with no nonemptiness or properness condition. Parity points are real images of integer vectors E → ℤ, so integrality is part of $X$. Dual variables are functions Finset V → ℝ whose values matter only on odd sets: the sign condition and every sum are restricted to the odd sets. Lengths $c$ are arbitrary reals except where the page assumes $c_e\ge 0$ (milestones 5 and 7).

Trivializing readings are ruled out: (3.5) taken over nonempty proper sets only, "meets" read as "has at least one end in", the odd nodes taken as an arbitrary set $T$, or $X$ allowed to contain non-integral points would each give a different, and in some cases false or trivial, statement.

Every definition the statements need is in one file, ChinesePostman.Polyhedron.Setting. A complete development needs finite-dimensional convexity (Mathlib's convexHull) and linear programming duality or an integrality argument. A Lean proof of total dual integrality for odd-cut systems would be reusable for matching and $T$-join problems beyond this paper. Proofs of any milestone, and alternative proofs of milestone 5, are welcome.

Selected references

• J. Edmonds and E. L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973) 88–124. https://doi.org/10.1007/BF01580113
• J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965) 125–130. https://doi.org/10.6028/jres.069B.013
• M. Guan (Kwan Mei-Ko), Graphic programming using odd or even points, Chinese Mathematics 1 (1962) 273–277.
• A. Schrijver, Combinatorial Optimization: Polyhedra and Efficiency, Springer, 2003, Chapter 29 (T-joins and T-cuts). https://doi.org/10.1007/978-3-540-44389-6

Motivation

Delivering goods from one depot to many customers with a fleet of trucks is the vehicle routing problem. Dantzig and Ramser formulated it in 1959 as the "truck dispatching problem" (Management Sci. 6 (1959), doi:10.1287/mnsc.6.1.80). Five years later Clarke and Wright proposed the savings procedure (Oper. Res. 12 (1964), 568–581, doi:10.1287/opre.12.4.568): start with one truck per customer and repeatedly join two routes where joining saves the most distance, as long as the trucks can still carry the loads. On the twelve-customer example of Dantzig and Ramser it reached 290 units against their 294.

The savings procedure became the standard construction heuristic for vehicle routing. It appears in every textbook treatment of the problem, is the initial solution of many metaheuristics, and is the benchmark against which later construction methods are compared. The paper states the procedure and its bookkeeping (the half matrix, the vector $Q$, Table II) but proves nothing about it. That every run of the procedure ends, and ends in a feasible allocation, is left to the reader.

Setting

A depot $P_0$ serves customers $P_1,\dots,P_M$. The distance $d_{y,z}$ between every two points is given, and customer $P_j$ requires a load $q_j$. Trucks come in $n$ capacity classes: $x_i$ trucks of capacity $C_i$ are available, with $C_1<\dots<C_n$, and the trucks of the smallest capacity are unlimited, $x_1=\infty$ (p. 569).

A run is the ordered list of customers $P_{a_1},\dots,P_{a_k}$ served by one truck, which drives $P_0P_{a_1}\cdots P_{a_k}P_0$. Its load is $\sum_i q_{a_i}$. A state of the procedure is a list of runs; its mileage is the total length of its runs. A list of runs is an allocation if every customer lies on exactly one run, and it is feasible if each run can be given a truck of capacity at least its load without using more trucks of any class than are available.

The saving of the cell $(y:z)$ is $d_{0,y}+d_{0,z}-d_{y,z}$. The half matrix records $t_{y,z}=1$ if $P_y$ and $P_z$ are adjacent on a run, and $t_{y,0}\in\{0,1,2\}$ counts how many ends of runs lie at $P_y$. Table II counts, for each capacity level $C_i$, the runs with load above $C_i$ and the trucks with capacity above $C_i$.