Combinatorics

Motivation

Several classical theorems of combinatorial optimization say that a family of sets arising from a graph packs: the maximum number of pairwise disjoint members equals the minimum size of a set meeting every member. König's theorem on bipartite graphs, Menger's theorem, the max-flow min-cut theorem of Ford and Fulkerson, Edmonds' branching theorem and the Lucchesi–Younger theorem all have this form (Seymour 1977, (1.1)–(1.5)). In the capacitated version (weights on elements, integral flows) the max-flow min-cut theorem says more: the packing property survives every deletion and replication of elements. Clutters with this stronger property are called Mengerian. For each $0$–$1$ matrix they are exactly the systems whose covering linear program and its dual have integral optima for every integral weight vector, which is why the notion matters to integer programming and polyhedral combinatorics.

Seymour's paper answers the question for the class of binary clutters, the clutters coming from binary matroids, which includes path collections, cut collections and odd-circuit collections of graphs. Earlier, Gallai's theorem implied that ports of regular matroids are Mengerian (Seymour 1977, p. 200); combined with Tutte's excluded-minor characterization of regular matroids, this showed that binary clutters without $Q_6$ or $b(Q_6)$ minors are Mengerian. Seymour shows that the second excluded minor is unnecessary, so a single small clutter is the only obstruction.

Setting

All sets are finite. A clutter $\mathbf L$ is a finite collection of finite sets, no member of which is contained in another; $\emptyset$ and $\{\emptyset\}$ are the two trivial clutters. Its ground set is $E(\mathbf L)=\bigcup_{A\in\mathbf L}A$. The blocker $b(\mathbf L)$ is the collection of minimal subsets of $E(\mathbf L)$ that meet every member of $\mathbf L$, and $\tau(\mathbf L)$ is the minimum cardinality of a member of $b(\mathbf L)$.

$\mathbf L$ is Mengerian if $\mathbf L=\{\emptyset\}$, or if for every weight map $w:E(\mathbf L)\to\mathbb Z^+$ there is an integral packing $q:\mathbf L\to\mathbb Z^+$ with $\sum_{A\ni x}q(A)\le w(x)$ for each $x\in E(\mathbf L)$ and

For a set $Z$, the deletion is $\mathbf L\setminus Z=\{A\in\mathbf L:A\cap Z=\emptyset\}$ and the contraction $\mathbf L/Z$ is the collection of minimal members of $\{A-Z:A\in\mathbf L\}$ (minimal, not minimal nonempty). A minor of $\mathbf L$ is any clutter obtained by a finite sequence of deletions and contractions.

A clutter is binary if $|A\cap B|$ is odd for all $A\in\mathbf L$ and $B\in b(\mathbf L)$; this is condition (3.2)(ii) of the paper, which is equivalent to being a port of a binary matroid. Finally

the triangles of $K_4$ with its edges labelled $1,\dots,6$.

For the structure theory, a circuit of a binary clutter is a minimal nonempty $C\subseteq E(\mathbf L)$ with $|C\cap B|$ even for every $B\in b(\mathbf L)$; $x$ and $y$ are parallel when $\{x,y\}$ is a circuit, and the point $\langle x\rangle$ is the parallel class of $x$. With $mb(\mathbf L)=\{B\in b(\mathbf L):|B|=\tau(\mathbf L)\}$, $\mathbf L$ is critical if $E(mb(\mathbf L))=E(\mathbf L)$. In a critical binary clutter, $x\to y$ means that every member of $mb(\mathbf L)$ containing $x$ contains $y$ while $y\notin\langle x\rangle$, and $y$ is initial if no $x$ has $x\to y$. MBC abbreviates "Mengerian binary clutter".

Formalization targets

Goal: Seymour's theorem (p. 209)

For every binary clutter $\mathbf L$,

Milestones

In the order the proof uses them:

• (2.3) Every minor of a Mengerian clutter is Mengerian.
• Section 1, p. 193. $Q_6$ is not Mengerian. With (2.3) this is the "only if" direction.
• (3.6)(i) Circuits of a binary clutter have at least two elements.
• (3.6)(iii) If $Z\subseteq E(\mathbf L)$ meets every member of $b(\mathbf L)$ evenly, then $Z$ is a disjoint union of circuits. If it meets every member oddly, then $Z$ is a disjoint union of circuits and one member of $\mathbf L$.
• (4.3) In a critical MBC, $x\to y$ implies $y\not\to x$.
• (4.4) In a critical MBC, $x\to y$ gives a circuit $C\ni x,y$ with $|C|\ge3$, $z\to y$ for $z\in C-\{y\}$, and $|B-(C-\{y\})|\ge\tau(\mathbf L)-1$ for $B\in b(\mathbf L)$.
• (4.5) In a critical MBC, a non-initial $x$ lies on a circuit $C$ with $|C|\ge3$ whose other elements are initial and point to $x$, and $|B\cap(C-\{x\})|\le1$ for $B\in mb(\mathbf L)$.
• (4.6) A nontrivial critical MBC has a member consisting of initial elements.
• (5.1) A binary clutter with six elements $x_1,y_1,x_2,y_2,x_3,y_3$ whose only circuits are the three sets $\{x_i,y_i,x_j,y_j\}$, together with a member $A$ that meets each pair $\{x_i,y_i\}$ once and satisfies a minimality condition, has a $Q_6$ minor.

Significance

The theorem is an excluded-minor characterization of the max-flow min-cut property. For binary clutters it decides exactly when the covering system $Mx\ge1$, $x\ge0$ has integral optimal primal and dual solutions for every integral cost vector, and it identifies $Q_6$ as the single obstruction. Its matroid form (the Corollary, p. 220) states that for a matroid $M$ the port $\Omega(M)$ is Mengerian for every element $\Omega$ if and only if $M$ is binary and has no $F_7^*$ minor. Consequences discussed in the paper include the two-commodity setting of (3.5): the clutter of minimal edge sets joining $s$ to $s'$ or $t$ to $t'$ is Mengerian exactly when the graph does not reduce to the configuration of its Figure 2. The theorem is also a basis for later work on ideal and Mengerian clutters, such as Cornuéjols' book Combinatorial Optimization: Packing and Covering (SIAM, 2001).

The result has been proved since 1977. To our knowledge no machine-checked proof exists. Mathlib at the pinned revision has matroids but no clutters, blockers, clutter minors, or matroids representable over GF(2). This mission builds that layer. The minor-closedness of the Mengerian property (2.3), the parity decomposition (3.6)(iii) and the structure theory of critical Mengerian binary clutters (4.3)–(4.6) are results in their own right and are useful beyond the main theorem.

Difficulty

The "only if" direction is short: minors of Mengerian clutters are Mengerian, and $Q_6$ fails with unit weights. The "if" direction is, in the author's words, "very much harder". A natural first idea is to show directly, by LP duality, that the covering polyhedron of a $Q_6$-free binary clutter is integral. This does not work: integrality of the polyhedron is the weak max-flow min-cut property, and $Q_6$ itself has that property while not being Mengerian, so no argument that sees only fractional optima can separate the two cases. The paper's proof works with a minimal counterexample and derives the $Q_6$ minor from the structure of critical Mengerian binary clutters in Section 4; its intermediate claims (5.2)–(5.39) hold only for that minimal counterexample, which is why they are not milestones here.

Formalization scope

Elements form a type α with decidable equality. A clutter is L : Finset (Finset α) with the clutter axiom as a hypothesis, $E(\mathbf L)$ is the union of members, and deletion and contraction take an arbitrary finite set $Z$. Weights $w$ and packings $q$ are $\mathbb N$-valued. The minimum in the Mengerian condition is expressed as "some $B\in b(\mathbf L)$ of least weight has weight equal to the packing value", never as an infimum. $\{\emptyset\}$ is Mengerian by the paper's convention, and $\tau(\{\emptyset\})$, which the paper leaves undefined, has the junk value $0$ in Lean; every item reading $\tau$ excludes $\{\emptyset\}$ or is vacuous there. "Minor" is the reflexive–transitive closure of single deletions and contractions. "Has a $Q_6$ minor" means that some minor equals the image of $Q_6$ (on Fin 6, with the paper's labels shifted down by one) under an injective relabelling Fin 6 ↪ α. Binary clutters are defined by (3.2)(ii); the paper defines them as ports of binary matroids and quotes (3.2) [15, 28] for the equivalence, and Mathlib has no GF(2)-representable matroids at this revision. Circuits are defined intrinsically, which makes (3.6)(ii) hold by definition.

Four readings would change the theorem and are ruled out: real-valued packings $q$ (the weak max-flow min-cut property, which $Q_6$ has, so the goal would be false), a non-minimal blocker or one not restricted to $E(\mathbf L)$, dropping the $\{\emptyset\}$ exception, and reading "$Q_6$ minor" as literal equality instead of isomorphism.

A complete development needs the blocker calculus ((2.1), (2.2), cited from [28] with proofs omitted), the parity theory of binary clutters, and the replication operation $\mathbf L_w$. The clutter layer (blocker, minors, Mengerian, binary, circuits) is reusable for later work on ideal clutters, Lehman's theorem and the Corollary's matroid form. Proofs of any milestone, of the helper facts $b(b(\mathbf L))=\mathbf L$, (2.1) and (2.2), and of the equivalences in (3.2) are welcome.

Selected references

• P. D. Seymour, The Matroids with the Max-Flow Min-Cut Property, J. Combin. Theory Ser. B 23 (1977) 189–222. https://doi.org/10.1016/0095-8956(77)90031-4
• J. Edmonds and D. R. Fulkerson, Bottleneck extrema, J. Combin. Theory 8 (1970) 299–306. https://doi.org/10.1016/S0021-9800(70)80083-7
• L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956) 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. Cornuéjols, Combinatorial Optimization: Packing and Covering, CBMS-NSF Regional Conf. Ser. in Appl. Math. 74, SIAM, 2001. https://doi.org/10.1137/1.9780898717105

Motivation

Max $k$-cover is the basic coverage problem of combinatorial optimization. The input is a collection of subsets of a finite ground set and a number $k$; the task is to choose $k$ subsets that together cover as many points as possible. It models facility and sensor placement, the selection of a small committee or feature set representing a population, and budgeted versions of set cover. It is also the prototype of maximizing a monotone submodular function under a cardinality constraint.

The greedy algorithm covers at least a $1-1/e\approx 0.632$ fraction of the optimum. This bound goes back to Hochbaum and Pathria and, for general submodular functions, to Nemhauser, Wolsey and Fisher (1978). For two decades it was not known whether a polynomial-time algorithm could do better. Uriel Feige answered the question in A Threshold of ln n for Approximating Set Cover (J. ACM 45(4), 1998, pp. 634–652, doi:10.1145/285055.285059), Section 5. His Theorem 5.3 (p. 648) states: "For any $\epsilon > 0$, max $k$-cover cannot be approximated in polynomial time within a ratio of $(1 - 1/e + \epsilon)$, unless $P = NP$." Together with the greedy bound, it makes $1-1/e$ the exact approximation threshold of max $k$-cover.

Timeline:

• 1978: Nemhauser, Wolsey and Fisher prove the greedy $1-1/e$ bound for monotone submodular maximization.
• 1992: Arora, Lund, Motwani, Sudan and Szegedy prove the PCP theorem. With Papadimitriou–Yannakakis (1991) it gives Theorem 2.1.1 of the paper: MAX 3SAT-B has a constant gap unless P = NP.
• 1994: Lund and Yannakakis introduce partition-system reductions from multi-prover proof systems to set cover.
• 1995: Raz proves the parallel repetition theorem (Theorem 2.2.2 of the paper).
• 1998: Feige proves the ln n threshold for set cover (the subject of mission I of this series) and the $1-1/e$ threshold for max $k$-cover.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$, a list of subsets $S_1,\dots,S_s$ of the points, and a number $k$. Its value $\mathrm{opt}$ is the largest number of points covered by at most $k$ of the sets. Instances are written over a three-letter alphabet:

• $n$ in unary;
• each set as its characteristic bit-vector;
• $k$ in unary.

Following p. 648, a polynomial-time algorithm approximates max $k$-cover within a ratio $\delta$ if on every input it outputs a number $v$ with

The algorithm need not name the sets. This is the non-constructive notion of approximation.

The proof is a reduction from the MAX 3SAT-5 problem. A 3CNF-5 formula has exactly three literals per clause, over three distinct variables, and every variable occurs in exactly five clauses. The reduction goes through a $k$-prover proof system for such a formula $\varphi$ with $M$ clauses:

• The verifier picks $\ell$ clauses at random, and a distinguished variable in each; there are $R=(3M)^\ell$ random strings $r$.
• Each prover $P_i$ is attached to a code word of length $\ell$ and weight $\ell/2$; distinct words are at Hamming distance at least $\ell/3$.
• On coordinate $j$, prover $P_i$ receives the clause if its bit is 1, and the distinguished variable if its bit is 0.
• Answers are satisfying assignments of the received clauses and bits for the received variables.
• Two provers are consistent if they assign the same values to the distinguished variables. The verifier weakly accepts if some pair of distinct provers is consistent, and strongly accepts if every pair is.

The max $k'$-cover instance of §5 attaches to every random string $r$ a copy $B_r$ of the explicit partition system. Its points are the vectors in $\{0,\dots,k-1\}^L$ with $L=2^\ell$, so $m=k^L$. Its $L$ partitions are labelled by the $\ell$-bit strings, and each splits the points by the value of one coordinate. There are $N=mR$ points in all. For each prover $i$, question $q$ and answer $a$, the set $S_{(q,a,i)}$ collects, for every $r$ on which $P_i$ receives $q$, the $i$th part of the partition of $B_r$ labelled by the values that $a$ gives to the distinguished variables of $r$. The budget is $k'=kQ$, where $Q$ is the number of questions a single prover can receive.

Formalization targets

Goal: Theorem 5.3

conditional on the two cited results below. The ratio is left free (any $\varepsilon>0$), so the goal records the shape of the threshold and not a particular constant.

Milestones

• Proposition 2.1.2 (p. 640): for some $\varepsilon>0$ it is NP-hard to distinguish satisfiable 3CNF-5 formulas from those in which at most a $(1-\varepsilon)$-fraction of the clauses can be satisfied simultaneously.
• Lemma 2.3.1 (p. 643): a satisfiable $\varphi$ admits a strategy that always strongly accepts; on a far-from-satisfiable $\varphi$ the weak acceptance probability is at most $k^2\,2^{-c\ell}$.
• Coverage of the explicit partition system (p. 649): $j$ subsets from pairwise different partitions cover exactly $(1-(1-1/k)^j)m$ points.
• Proposition 5.4 (p. 649): if at most $kQ$ sets cover a $(1-1/e+\varepsilon)$-fraction of the points, then at least an $\varepsilon/3$-fraction of the random strings are good. Here $r$ is good if $w_r\le3k/\varepsilon$ sets meet $B_r$ and two of them from different provers lie in the same partition.
• Decoding (p. 649): such a covering yields a strategy that weakly accepts with probability at least $(\varepsilon/3)(\varepsilon/3k)^2$.
• Gap (p. 649): a satisfiable formula gives a cover of all $N$ points by $kQ$ sets. If at most a $(1-\varepsilon')$-fraction of the clauses are satisfiable, $kQ$ sets cover at most $(1-1/e+g(k))N$ points, where $g(k)\to0$, for all large $\ell$.
• Proposition 5.1 (p. 647): every greedy run covers at least $(1-1/e)\,\mathrm{opt}$ points.

Significance

The result closes the approximability of max $k$-cover: the greedy algorithm cannot be beaten by any constant unless P = NP. Consequences:

• Submodular maximization. Coverage functions are monotone submodular, so the bound transfers to monotone submodular maximization under a cardinality constraint, whenever the function is given in a form that encodes a coverage instance.
• Other problems. Hardness results for facility location, budgeted allocation, and welfare maximization with coverage valuations reduce from it.
• The reduction itself. The $\ell$-fold $k$-prover system combined with a partition system that is exactly countable is the template for later $1-1/e$ hardness proofs.

Status: the theorem has been proved since 1998. It has not been formalized; neither the reduction nor the underlying proof systems exist in Mathlib or on this platform. This mission produces:

• a machine-checked reduction from MAX 3SAT-5 to max $k$-cover;
• an exact counting lemma for product partition systems;
• the averaging and concavity argument of Proposition 5.4;
• a formal statement of the greedy bound for coverage.

The cited PCP-based gap (Theorem 2.1.1) and parallel repetition (Theorem 2.2.2) remain hypotheses. They are separate, much larger formalization projects.

Difficulty

The obvious argument uses the soundness of the proof system directly: a large cover should force consistent answers. It fails because a cover may spend many sets on a few random strings and cover them completely, while covering the rest partially without any two sets from the same partition. What saves the argument is exact counting. For sets from pairwise different partitions, coverage is exactly $h(j)=(1-(1-1/k)^j)m$, a concave function of the number $j$ of sets used. Since the sets meet a random string $k$ times on average, Jensen's inequality caps the total coverage of such "unstructured" strings at about $(1-(1-1/k)^k)$, which tends to $1-1/e$. A further obstacle is that the reduction must run in polynomial time. The paper therefore takes $\ell$ and $k$ constant (unlike the set-cover reduction, where $\ell=\Theta(\log\log n)$), and the soundness bound $k^2 2^{-c\ell}$ must beat $(\varepsilon/3)(\varepsilon/3k)^2$ at a constant $\ell$. The quantifier order ($k$ large first, then $\ell$ large) is part of the difficulty.

A second obstacle is the machine model. The goal is a statement about polynomial-time Turing machines, so the reduction and the decision procedure built from a hypothetical approximation algorithm must be compiled into Cook's one-tape machines.

Formalization scope

• Machine model. CookPvsNP_defs (a published platform definition): one-tape Turing machines, $\mathrm{P}$, $\mathrm{NP}$, polynomial-time computable functions, CNF formulas and their encoding. "P = NP" is P Bool = NP Bool, the form in which CookPvsNP.P_ne_NP states the open problem.
• Cited results as hypotheses. Theorem 2.1.1 enters as Thm211. Raz's theorem enters as RazRepetition, its consequence stated on p. 642: the $\ell$-fold clause–variable game on a far-from-satisfiable 3CNF-5 formula has acceptance probability at most $2^{-c\ell}$. This is weaker than Raz's general theorem, so the conditional statement is stronger. No hypothesis about max $k$-cover is assumed.
• Approximation. The value form above, with no size threshold. For $\varepsilon>1/e$ the ratio exceeds one and the hypothesis is unsatisfiable on any instance with $\mathrm{opt}>0$; those values are vacuous, as in the paper.
• $\mathrm{opt}$. Taken over at most $k$ sets. This agrees with the paper's "exactly $k$" whenever $k\le s$.
• Probability and counting. Probabilities are uniform counts over the $(3M)^\ell$ random strings. Fractions in lower-bound statements are written as counts compared with multiples of $R$.
• Canonical answers. The type of answers is restricted to satisfying assignments of the received clauses, following the paper's "without loss of generality" (p. 643). All indices are 0-based.
• Partition system. The §4 construction is defined for any partition system with $\ell$-bit partition labels and instantiated with the explicit product system. Its $L=2^\ell$ coordinates are the $\ell$-bit strings themselves.
• Not formalized. The running time of the greedy algorithm, and the constructive variant (Proposition 5.2), which belongs to the set-cover mission.

A trivializing formalization is ruled out: every cited input is a named, satisfiable proposition about 3CNF formulas or the two-prover game, never about max $k$-cover, and the approximation hypothesis is satisfiable for ratios up to $1$.

Needed infrastructure, reusable beyond this mission:

• composition and simulation lemmas for Cook's machines;
• the uniformity of the verifier's questions on 3CNF-5 formulas;
• concavity of $j\mapsto 1-(1-1/k)^j$;
• $(1-1/k)^k\to 1/e$ bounds.

Contributions to any of these, or to either cited theorem, are welcome.

Selected references

• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4) (1998) 634–652. https://doi.org/10.1145/285055.285059
• R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3) (1998) 763–803 (STOC 1995). https://doi.org/10.1137/S0097539795280895
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3) (1998) 501–555. https://doi.org/10.1145/278298.278306
• C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. System Sci. 43(3) (1991) 425–440. https://doi.org/10.1016/0022-0000(91)90023-X
• C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5) (1994) 960–981. https://doi.org/10.1145/185675.306789
• G. L. Nemhauser, L. A. Wolsey, M. L. Fisher, An analysis of approximations for maximizing submodular set functions—I, Math. Programming 14 (1978) 265–294. https://doi.org/10.1007/BF01588971
• S. Cook, The P versus NP problem, Clay Mathematics Institute. https://www.claymath.org/wp-content/uploads/2022/06/pvsnp.pdf

Motivation

Set cover is the problem of covering a finite ground set with as few members of a given family of subsets as possible. It models facility location, crew scheduling, test-suite minimization and many other selection problems in operations research, and it is one of the canonical NP-hard problems. The greedy algorithm, which repeatedly picks the subset covering the most uncovered points, finds a cover at most about $\ln n$ times larger than the optimum on an instance with $n$ points (Johnson 1974; Lovász 1975; Chvátal 1979). Whether any efficient algorithm does substantially better was open for two decades.

Timeline of the lower bounds:

• 1992. The PCP theorem (Arora, Lund, Motwani, Sudan, Szegedy) implies that set cover cannot be approximated within some constant $1+\varepsilon$ unless P = NP.
• 1994. Lund and Yannakakis showed that set cover cannot be approximated within $\tfrac14\log_2 n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\mathrm{polylog}\, n)})$, and within $\tfrac12\log_2 n\approx 0.72\ln n$ under a randomized assumption.
• 1998. Feige showed that for every $\varepsilon>0$, set cover cannot be approximated within $(1-\varepsilon)\ln n$ unless $\mathrm{NP}\subseteq\mathrm{TIME}(n^{O(\log\log n)})$ (J. ACM 45(4), 634–652). This matches the greedy bound up to lower-order terms.
• 2014. Dinur and Steurer replaced the assumption by P ≠ NP (STOC 2014).

This mission formalizes Feige's theorem, the result that fixed $\ln n$ as the threshold.

Setting

An instance consists of $n$ points $\{0,\dots,n-1\}$ and a list of subsets $S_1,\dots,S_s$. A cover is a set of indices whose subsets together contain every point. The instance is coverable if every point lies in some $S_i$. It is written as a string: $n$ in unary, then each subset as its characteristic vector.

A deterministic polynomial-time algorithm approximates set cover within $\rho(n)$ if, for some threshold $n_0$ and every coverable instance with $n \ge n_0$ points, the value $v$ it outputs satisfies $\mathrm{OPT}\le v\le\rho(n)\cdot\mathrm{OPT}$, where $\mathrm{OPT}$ is the size of a smallest cover.

$\mathrm{TIME}(n^{O(\log\log n)})$ is the class of languages that a deterministic one-tape Turing machine decides within $|w|^{c(\log_2\log_2|w|+1)}+c$ steps, for some constant $c$. Machines, $\mathrm{P}$ and $\mathrm{NP}$ are those of the published definition CookPvsNP_defs.

The proof passes through three objects, each defined in the mission:

1. 3CNF-5 formulas: CNF formulas in which every clause has three literals on distinct variables and every variable occurs in exactly five clauses.
2. The $k$-prover proof system of §2.3. A verifier picks $\ell$ random clauses and a distinguished variable in each. Each prover, according to its code word, receives some of these clauses and the distinguished variables of the others. Under the weak acceptance predicate, some two provers give consistent answers on the distinguished variables. Under the strong acceptance predicate, all provers do.
3. Partition systems $B(m,L,k,d)$ (Definition 3.1). These are $L$ partitions of $m$ points, each into $k$ parts, such that covering the points with parts taken from pairwise different partitions needs at least $d$ parts.

Formalization targets

Goal: Theorem 4.4

The statement fixes no constant beyond $\varepsilon$. The parameters $k$, $\ell$ and $m$ of the reduction are choices made inside the proof. The goal carries three cited results as hypotheses: Theorem 2.1.1 (MAX 3SAT-B gap), the consequence of Raz's parallel repetition theorem for the clause–variable game, and the Naor–Schulman–Srinivasan construction of partition systems.

Milestones, in the order the proof uses them

1. Proposition 2.1.2: MAX 3SAT-5 is gap NP-hard.
2. Proposition 2.2.1: the one-round clause–variable game has value $1-\varepsilon/3$.
3. Lemma 2.3.1: the $k$-prover system is complete with strong acceptance and has soundness $k^2 2^{-c\ell}$ for weak acceptance.
4. Lemma 3.2: partition systems with $d=(1-2/k)k\ln m$ exist.
5. Propositions 4.2 and 4.3: a cover with $(1-\delta)kQ\ln m$ subsets yields a prover strategy that is weakly accepted with probability at least $2\delta/(k\ln m)^2$.
6. Lemma 4.1: the gap between $kQ$ and $(1-2f(k))kQ\ln m$.

Significance

The result. Combined with the greedy algorithm, Theorem 4.4 shows that $\ln n$ is the approximation threshold of set cover under a mild complexity assumption. Set cover reduces approximation-preservingly to many covering problems, so the threshold transfers to them. Examples are dominating set, several facility-location and group Steiner problems, and hitting-set formulations used in scheduling and testing. The $k$-prover system with two acceptance predicates and the partition-system gadget became standard tools for later hardness-of-approximation proofs.

Formalizing it. The theorem is proved and has been strengthened (Dinur–Steurer 2014), but no machine-checked proof of any $\Omega(\log n)$ inapproximability of set cover is known. This mission contributes:

• a Lean model of multi-prover proof systems with uniform-count probabilities;
• partition systems and their probabilistic existence proof;
• a gap-preserving reduction whose running time is analysed on Turing machines, not merely asserted.

Difficulty

• The ratio comes from two gaps at once. One is a gap in acceptance probability. The other is a gap between strong and weak acceptance. A reduction from a two-prover system, as in Lund–Yannakakis, loses a constant factor because a cheating cover can use two parts of the same partition. Feige's analysis must turn every small cover into a strategy under which some pair of provers is consistent (Proposition 4.3), and this averaging argument has to lose only a factor $(k\ln m)^2$.
• Parameters interlock. $\ell=\Theta(\log\log n)$ must make $k^2 2^{-c\ell}$ smaller than $2\delta/(k\ln m)^2$ while keeping the instance of size $n^{O(\log\log n)}$. The time bound must hold for a one-tape machine, including the deterministic partition-system construction.
• Encoding. The reduction must be computed by an explicit machine on string encodings. Showing that a "clearly polynomial" construction meets the time bound on such a machine is substantial work.

Formalization scope

• Cited results as hypotheses. Theorem 2.1.1, Raz's theorem and the Naor et al. construction are not proved in the mission; each is a named proposition (Thm211, RazRepetition, NaorPartitionSystems) and a hypothesis of the goal.
  • RazRepetition is only the consequence of Raz's theorem that the paper uses (p. 642): a $2^{-c\ell}$ error bound for the repeated clause–variable game on 3CNF-5 formulas far from satisfiable.
  • NaorPartitionSystems relaxes "time linear in $m$" to polynomial time and renders "$L$ polynomial in $d$" as $L\le\lfloor\log_2 m\rfloor^a$. Both relaxations weaken the hypothesis.
• Approximation in value form. The algorithm outputs a number $v$ with $\mathrm{OPT}\le v\le\rho(n)\mathrm{OPT}$, and only on coverable instances with $n\ge n_0$. Any algorithm that outputs a cover yields such a value, so this hypothesis is weaker than the paper's. The guard $n\ge n_0$ is needed because $(1-\varepsilon)\ln n<1$ for small $n$.
• Machine model. The machines are Cook's deterministic one-tape machines. Multi-tape simulation costs a quadratic factor, which the class absorbs.
• Probabilities are uniform counts over the $(5n)^\ell$ random strings. Strategies are deterministic. Answers are canonical (satisfying on clause coordinates), as the paper assumes without loss of generality.
• Not formalized. Randomized classes (ZTIME) are not defined here, so the following are omitted: the last sentence of Lemma 3.2, Proposition 6.1, and the randomized variants.
• Ruling out a trivial formalization. The gap notion requires far-from-satisfiable formulas to have at least one clause. Otherwise the empty formula would be both a yes-instance and a no-instance, and Theorem 2.1.1 would hold trivially.
• Infrastructure and reuse. The shared layer can serve other PCP-based hardness proofs: 3CNF-5 formulas, the $k$-prover system, partition systems, and the gap-NP-hardness notion. Welcome contributions include:
  • time bounds for list and table manipulations on one-tape machines;
  • a Hadamard-code construction satisfying the weight and distance conditions;
  • the union-bound and averaging lemmas behind Lemma 2.3.1 and Proposition 4.2.

Selected references

• U. Feige, A threshold of ln n for approximating set cover, J. ACM 45(4), 634–652, 1998. https://doi.org/10.1145/285055.285059
• C. Lund, M. Yannakakis, On the hardness of approximating minimization problems, J. ACM 41(5), 960–981, 1994. https://doi.org/10.1145/185675.306789
• R. Raz, A parallel repetition theorem, SIAM J. Comput. 27(3), 763–803, 1998 (STOC 1995). https://doi.org/10.1137/S0097539795280895
• M. Naor, L. J. Schulman, A. Srinivasan, Splitters and near-optimal derandomization, FOCS 1995, 182–191. https://doi.org/10.1109/SFCS.1995.492475
• S. Arora, C. Lund, R. Motwani, M. Sudan, M. Szegedy, Proof verification and the hardness of approximation problems, J. ACM 45(3), 501–555, 1998. https://doi.org/10.1145/278298.278306
• C. Papadimitriou, M. Yannakakis, Optimization, approximation, and complexity classes, J. Comput. Syst. Sci. 43(3), 425–440, 1991. https://doi.org/10.1016/0022-0000(91)90023-X
• V. Chvátal, A greedy heuristic for the set-covering problem, Math. Oper. Res. 4(3), 233–235, 1979. https://doi.org/10.1287/moor.4.3.233
• I. Dinur, D. Steurer, Analytical approach to parallel repetition, STOC 2014, 624–633. https://doi.org/10.1145/2591796.2591884

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models table formatting, the placement of program segments on pages, and the allocation of files to disc tracks, and it is NP-complete, so exact solutions require search in general. Johnson, Demers, Ullman, Garey and Graham (SIAM J. Comput. 3 (1974)) therefore studied four simple placement heuristics and bounded how far each can be from the optimum in the worst case. Their paper is one of the founding results of the worst-case analysis of approximation algorithms.

This mission concerns the two decreasing heuristics, which sort the items from largest to smallest before placing them. For them the paper proves that at most $\tfrac{11}{9}$ of the optimum, plus an additive constant, is ever used, and that the factor $\tfrac{11}{9}$ cannot be improved.

Timeline.

• 1973: D. S. Johnson's MIT thesis proves $FFD(L)\le \tfrac{11}{9}L^*+4$; the argument exceeds 75 pages.
• 1974: Johnson, Demers, Ullman, Garey and Graham publish the bound for FFD and BFD, with a complete proof of the reduction from BFD to FFD and an outline of the FFD argument.
• 1985: B. S. Baker gives a shorter proof of $FFD(L)\le\tfrac{11}{9}L^*+3$ (J. Algorithms 6).
• 1991: M. Yue publishes a proof of $FFD(L)\le\tfrac{11}{9}L^*+1$.
• 2007: G. Dósa determines the tight additive constant, $FFD(L)\le\tfrac{11}{9}L^*+\tfrac{6}{9}$ (ESCAPE 2007, LNCS 4614).

Setting

A list is a finite sequence $L=(a_1,a_2,\dots,a_n)$ of real numbers in $(0,1]$; values may repeat. A bin has capacity $1$; its level is the sum of the numbers placed in it. The optimum $L^*$ is the least number of bins into which the elements of $L$ can be distributed so that no bin has level exceeding $1$.

The bins $B_1,B_2,\dots$ start empty and the elements are placed one at a time, in list order.

• First-Fit (FF) places $a_i$ into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$.
• Best-Fit (BF) places $a_i$ into a bin whose level $\beta$ satisfies $\beta\le 1-a_i$ and is as large as possible, the one of least index among ties.
• First-Fit Decreasing (FFD) and Best-Fit Decreasing (BFD) first arrange $L$ into nonincreasing order and then apply FF, respectively BF.

$FFD(L)$ and $BFD(L)$ are the numbers of bins that receive at least one element.

Two auxiliary notions from the paper's proof also appear among the milestones. The position $(j,k)$ of an element in a packing means that it is the $k$-th element placed into bin $j$. The weight $W(X)$ of a collection of elements is defined through $k$-pieces, the elements in $(\tfrac1{k+1},\tfrac1k]$. Each element has the weight $w_1(x)=\lfloor 1/x\rfloor^{-1}$. A pair $(x,y)$ with $x$ a $k$-piece and $kx+y\le1$ has the discounted weight $w_2(x,y)=w_1(x)+\tfrac{k-1}{k}w_1(y)$, and any other pair has $w_1(x)+w_1(y)$. $W(X)$ is the least total weight over all ways of grouping $X$ into singletons and pairs.

Formalization targets

Goal: Theorem 3.2

For every list $L$,

The constants are the paper's. Both halves are part of the goal.

Milestones, in the order the argument uses them

1. Lemma 3.3. If $FFD(L)>rL^*+d$ with $r,d\ge1$, the list $L'$ keeping only the elements exceeding $(r-1)/r$ also has $FFD(L')>rL'^*+d$; the same for BFD. With $r=\tfrac{11}{9}$ this reduces the goal to lists in $(\tfrac2{11},1]$.
2. Claims 3.4.5 and 3.4.6, two steps of the proof of Theorem 3.4 that concern only the FFD packing $PF$ and the BFD run. On $[\tfrac16,1]$, BFD places every element exceeding $\tfrac13$ exactly where FFD does. Among the remaining positions of $PF$, the lexicographic order of positions respects the order of the sorted list.
3. Theorem 3.4. If $L\subseteq[\tfrac16,1]$, then $BFD(L)\le FFD(L)$. This transfers the bound from FFD to BFD on $(\tfrac2{11},1]$.
4. Lemma 4.2. For every integer $N\ge4$ and $L\subseteq(\tfrac1N,\tfrac12]$,

5. The reduced assertion (Section 4, p. 314). If $L\subseteq(\tfrac2{11},1]$, then

6. Theorem 3.1, the matching lower bound: for each $k\ge1$ there is a list with $L^*=k$ and $FFD(L)=BFD(L)>\tfrac{11}{9}L^*-2$.

Significance

The bound makes FFD and BFD, which run in $O(n\log n)$ time, the reference heuristics for off-line bin packing. The $\tfrac{11}{9}$ bound and its proof technique of weighting functions were the model for the analysis of many later packing and scheduling heuristics. Theorem 3.1 shows that the factor is exact, so together with the goal it determines $\lim_{k\to\infty}R_{FFD}(k)=\lim_{k\to\infty}R_{BFD}(k)=\tfrac{11}{9}$, where $R_A(k)$ is the largest ratio $A(L)/L^*$ over lists with $L^*=k$.

The result is proved, but the source proves it only in part. The paper gives complete proofs of Lemma 3.3, Theorem 3.4 and Theorem 3.1. For the reduced assertion it gives only an outline, whose central inequalities involve maps the paper never defines, and it refers to the thesis for the details. Lemma 4.2 is proved in the paper through two claims. A formal proof of the goal must therefore either formalize one of the later complete proofs (Baker 1985, Yue 1991, Dósa 2007) or reconstruct the thesis argument. No machine-checked proof of the $\tfrac{11}{9}$ bound is present in Mathlib or on the platform.

Difficulty

The obvious approach, used for First-Fit in Section 2 of the same paper, assigns each element a weight depending only on its size, so that every bin of the algorithm's packing weighs at least $1$ and every bin of an optimal packing weighs at most the target ratio. For FFD no weighting of single elements works at ratio $\tfrac{11}{9}$. Summing $w_1$ over the elements overcharges the FFD packing: a set of elements fitting into one bin can carry total $w_1$-weight well above $\tfrac{11}{9}$. The paper's remedy is a weight defined on pairs, $W(X)$, which discounts elements that could share a bin with a larger one. Even with $W$, the bins of FFD whose largest element exceeds $\tfrac12$ do not fit the scheme. Handling them requires a case analysis that the paper only sketches and that runs to more than 75 pages in the thesis.

The BFD half cannot be obtained by bounding BFD by FFD in general: there are lists with $BFD(L)=\tfrac{10}{9}FFD(L)$. Theorem 3.4 works only because Lemma 3.3 first removes all elements below $\tfrac2{11}$.

Formalization scope

Lists are L : List ℝ with the predicate IsList L ($0<a\le1$ for every element), assumed by every statement. $L^*$ is optBins L, the least b : ℕ admitting a map from the items to Fin b with every bin sum at most $1$. A run keeps the nonempty bins as a List (List ℝ) in index order and opens a new bin at the end exactly when no nonempty bin fits, which matches the paper's "least $j$" over infinitely many empty bins. The fit test is non-strict. FFD and BFD are FF and BF applied to sortDesc L, a stable merge sort into nonincreasing order. They are defined for every list, so the goal is stated for arbitrary, unsorted $L$. Positions are $0$-based pairs (bin, place in bin) read off the run.

$W$ sorts its argument into nonincreasing order, so index is the position in that order. It then minimizes over involutions of the positions, which encode the partitions into one- and two-element sets. Weights are real-valued; the paper's use of rationals is incidental. The range hypotheses are exactly the paper's: $[\tfrac16,1]$ is closed in Theorem 3.4, $(\tfrac2{11},1]$ is open at $\tfrac2{11}$, and Lemma 4.2 has $\tfrac1N<a\le\tfrac12$.

A weakened goal, such as $FFD(L)\le\tfrac{11}{9}L^*+c$ with a larger $c$, a bound for sorted lists only, or the FFD half alone, is a different theorem and does not close the mission. Claims 3.4.1–3.4.4 and 3.4.7 and the inequalities $(*)$, $(**)$ of the outline are not stated: they concern the paper's step-by-step construction and the undefined maps $f$, $g$.

A complete development needs basic lemmas about FF and BF runs (levels stay at most $1$, a new bin opens only when nothing fits, runs on prefixes). It also needs invariance of FFD and BFD under permutations of equal elements, the monotonicity of $L^*$ under deletion, and $L^*\ge\sum_i a_i$. These are reusable in the other missions of this series. Proofs of individual milestones, alternative complete proofs of the goal, and sharper additive constants are all welcome.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, Ph.D. thesis, Massachusetts Institute of Technology, 1973 (reference [8] of the paper above).
• B. S. Baker, A new proof for the first-fit decreasing bin-packing algorithm, Journal of Algorithms 6(1):49–70, 1985. https://doi.org/10.1016/0196-6774(85)90018-5
• M. Yue, A simple proof of the inequality FFD(L) ≤ 11/9 OPT(L) + 1, ∀L, for the FFD bin-packing algorithm, Acta Mathematicae Applicatae Sinica 7(4):321–331, 1991.
• G. Dósa, The tight bound of first fit decreasing bin-packing algorithm is FFD(I) ≤ 11/9 OPT(I) + 6/9, ESCAPE 2007, LNCS 4614:1–11, 2007. https://doi.org/10.1007/978-3-540-74450-4_1

Motivation

A set of integers is a Sidon set if all of its pairwise sums $a+b$ ($a\le b$) are different. Sidon, in connection with Fourier analysis, asked how dense such sets can be, and the question became one of the standard problems of additive combinatorics. Let

A counting argument shows $h(N)\le (1+o(1))\sqrt{2N}$, and the true order was settled early: $h(N)\sim\sqrt N$. What remains open is the size of the error term $h(N)-\sqrt N$. Erdős and Turán asked whether it is smaller than every power of $N$; Erdős offered $1000 for this problem (Erdős Problem #30), and it is also Problem 31 on Green's list of open problems and problem C9 in Guy's Unsolved Problems in Number Theory.

Timeline.

• 1938 — Singer constructs, for every prime power $q$, a set of $q+1$ residues modulo $q^2+q+1$ with all differences distinct. Combined with the density of primes this gives $h(N)\ge(1-o(1))\sqrt N$ (Singer 1938).
• 1941 — Erdős and Turán prove $h(N)\le N^{1/2}+O(N^{1/4})$ (Erdős–Turán 1941).
• 1969 — Lindström gives an alternative proof with the explicit bound $h(N)\le N^{1/2}+N^{1/4}+1$ (Lindström 1969).
• 2021 — Balogh, Füredi and Roy lower the constant: $h(N)\le N^{1/2}+0.998N^{1/4}$ for large $N$ (arXiv:2103.15850).
• 2022 — O'Bryant: $h(N)\le N^{1/2}+0.99703N^{1/4}$ for large $N$ (arXiv:2207.07800).
• 2023 — Carter, Hunter and O'Bryant: $h(N)\le N^{1/2}+0.98183N^{1/4}+O(1)$, with substantial computer assistance (arXiv:2310.20032).

No upper bound with an error exponent below $1/4$ is known, and no lower bound of the form $h(N)\ge\sqrt N-O(N^{\varepsilon})$ for every $\varepsilon>0$ is known either.

Setting

A set $A$ in an additive commutative monoid is Sidon if for all $i_1,j_1,i_2,j_2\in A$,

For a finite set $X$, $\operatorname{maxSidon}(X)$ is the largest size of a Sidon subset of $X$ (the empty set is Sidon, so this is well defined), and

The first values are $h(1),\dots,h(15)=1,2,2,3,3,3,4,4,4,4,4,5,5,5,5$ (OEIS A143824).

Formalization targets

Goal (Erdős Problem #30)

This is a two-sided statement: it asks both for an upper bound $h(N)\le\sqrt N+C_\varepsilon N^\varepsilon$ and for a matching lower bound $h(N)\ge\sqrt N-C_\varepsilon N^\varepsilon$ for large $N$. Erdős asked it as a yes/no question; the goal fixes the conjectured answer yes, so a disproof on the platform settles the question negatively.

Milestones (known results, weakest to strongest)

1. Singer's construction: $h(q^2+q+1)\ge q+1$ for every prime power $q$.
2. Singer's lower bound: $h(N)\ge(1-\varepsilon)\sqrt N$ for every $\varepsilon>0$ and all large $N$.
3. Erdős–Turán / Lindström: $h(N)\le\sqrt N+N^{1/4}+1$ for all $N$.
4. Balogh–Füredi–Roy: $h(N)\le\sqrt N+0.998N^{1/4}$ for all large $N$.
5. O'Bryant: $h(N)\le\sqrt N+0.99703N^{1/4}$ for all large $N$.
6. Carter–Hunter–O'Bryant: $h(N)\le\sqrt N+0.98183N^{1/4}+C$ for an absolute constant $C$.

Significance

The result itself. An affirmative answer would pin $h(N)$ down to $\sqrt N$ up to a sub-polynomial error, in both directions; Erdős even speculated that $h(N)=\sqrt N+O(1)$ might hold, while remarking that this is perhaps too optimistic. A negative answer would show that the Singer-type constructions or the counting upper bounds are off by a power of $N$. Either answer would be the first change in the exponent of the error term since 1941.

Formalizing it. The goal is open. All milestones are published theorems. The platform already contains weaker related results in other formalizations (for example the order-of-magnitude bounds $c\sqrt N\le \max|A|\le\sqrt{2N}+1$ for Sidon subsets of an initial segment, and the Erdős–Turán construction); the sharp bounds listed as milestones are not stated there for this $h$. The upper bounds of Balogh–Füredi–Roy and O'Bryant are elementary but delicate optimizations, and the Carter–Hunter–O'Bryant bound relies on a large computation, so formalizing it is a substantial verification task in its own right.

Difficulty

For the upper bound, every known argument counts differences $a-a'$ in short windows and loses at the scale $N^{1/4}$; improvements since 1941 only change the constant in front of $N^{1/4}$. For the lower bound, the constructions (Singer, Bose, Ruzsa) produce Sidon sets of size about $\sqrt p$ in a modulus $p$ of size about $N$, and the loss comes from the gap between $N$ and the nearest admissible modulus; bringing it below $N^\varepsilon$ requires either new constructions or information about primes in very short intervals that is far beyond current knowledge.

Formalization scope

Sidon sets are formalized for sets in an arbitrary additive commutative monoid, with the definition, the decidability instance and $\operatorname{maxSidon}$ transcribed from the formal-conjectures library (definitions IsSidon, Finset.maxSidonSubsetCard, and Erdos30.h in FormalConjectures/ErdosProblems/30.lean), placed in the namespace Erdos30. The value $h(N)$ is a natural number cast to $\mathbb R$; $\sqrt{\cdot}$ is the real square root and $N^{\varepsilon}$, $N^{1/4}$ are real powers of $N\ge 0$. The goal's $O(\cdot)$ is Mathlib's Asymptotics.IsBigO along atTop on $\mathbb N$. The goal is not trivialized by any junk value: $h$ is a genuine finite maximum, and the $O(\cdot)$ statement concerns all large $N$.

Useful infrastructure: basic lemmas on Sidon sets (hereditary under subsets, translation invariance, distinct differences), finite projective geometry or Bose's construction for the lower bounds, and prime gaps (Bertrand's postulate suffices for $h(N)\ge c\sqrt N$ with $c<1$; a prime number theorem in short intervals is needed for $1-o(1)$). Contributions of reusable Sidon-set lemmas are welcome.

Selected references

• J. Singer, A theorem in finite projective geometry and some applications to number theory, Trans. Amer. Math. Soc. 43 (1938), 377–385. https://doi.org/10.1090/S0002-9947-1938-1501951-4
• P. Erdős and P. Turán, On a problem of Sidon in additive number theory, and on some related problems, J. London Math. Soc. 16 (1941), 212–215. https://doi.org/10.1112/jlms/s1-16.4.212
• B. Lindström, An inequality for $B_2$-sequences, J. Combin. Theory 6 (1969), 211–212. https://doi.org/10.1016/S0021-9800(69)80124-9
• J. Balogh, Z. Füredi and S. Roy, An upper bound on the size of Sidon sets, Amer. Math. Monthly (2023). https://arxiv.org/abs/2103.15850
• K. O'Bryant, On the size of finite Sidon sets (2022). https://arxiv.org/abs/2207.07800
• D. Carter, Z. Hunter and K. O'Bryant, On the diameter of finite Sidon sets (2023). https://arxiv.org/abs/2310.20032
• K. O'Bryant, A complete annotated bibliography of work related to Sidon sequences, Electron. J. Combin. DS11 (2004). https://arxiv.org/abs/math/0407117
• T. F. Bloom, Erdős Problem #30, https://www.erdosproblems.com/30
• Google DeepMind, formal-conjectures, FormalConjectures/ErdosProblems/30.lean. https://github.com/google-deepmind/formal-conjectures

Motivation

Addition and multiplication interact in rigid ways: a finite set of numbers that is highly structured with respect to one operation (an arithmetic progression, say) tends to be unstructured with respect to the other (a geometric progression). The sum–product problem asks for the sharp quantitative form of this principle. It was posed by Erdős and Szemerédi in 1983 (Erdős Problem 52) and has since become a central question of additive combinatorics, with applications in incidence geometry, exponential sum estimates, expanders and randomness extraction.

Timeline.

• 1983 — Erdős and Szemerédi show that $\max(|A+A|,|AA|)\ge c|A|^{1+\delta}$ for some absolute $\delta>0$ and every finite set of integers $A$, and conjecture exponent $2-\varepsilon$.
• 1997 — Nathanson obtains the explicit exponent $1+\tfrac1{31}$; Ford (1998) improves it to $1+\tfrac1{15}$.
• 1997 — Elekes, using the Szemerédi–Trotter incidence theorem, proves $|A+A|\,|AA|\gg|A|^{5/2}$ for finite sets of reals, hence exponent $5/4$.
• 2009 — Solymosi proves $|A+A|^2|AA|\gg |A|^4/\log|A|$ for finite sets of positive reals, hence exponent $4/3$ up to a logarithmic factor.
• 2015–2022 — Konyagin and Shkredov first break the $4/3$ barrier (exponent $4/3+c$ for a small explicit $c>0$); after several improvements, Rudnev and Stevens reach $4/3+2/1167$ up to logarithmic factors.

The conjecture itself remains open.

Setting

For a finite set $A\subset\mathbb Z$ define the sumset and product set

For nonempty $A$ both contain at least $|A|$ elements and at most $\binom{|A|+1}{2}$. The quantity of interest is $\max(|A+A|,|AA|)$ as a function of $|A|$.

Formalization targets

Goal (Erdős–Szemerédi conjecture)

For every $0<\varepsilon<1$ there is $C_\varepsilon>0$ such that for every finite set $A\subset\mathbb Z$,

Known lower bounds (milestones, weakest to strongest)

Sharpness

The $\varepsilon$ cannot be removed: there is no $C>0$ with $\max(|A+A|,|AA|)\ge C|A|^2$ for all $A$ (take $A=\{1,\dots,n\}$; the multiplication table $|AA|$ is $o(n^2)$ by Erdős).

Significance

A proof of the goal would settle the sharp form of the sum–product phenomenon over $\mathbb Z$. Sum–product estimates are an input to incidence bounds, to Bourgain–Katz–Tao-type results over finite fields, and to explicit constructions in theoretical computer science; improvements of the exponent over $\mathbb R$ have come together with new incidence-geometric tools.

Formalization status: the milestones are published theorems (Erdős–Szemerédi, Elekes, Solymosi, Rudnev–Stevens, Erdős's multiplication table bound), but their proofs are not known to be formalized in Lean/Mathlib. The Szemerédi–Trotter theorem, multiplicative energy, and the Elekes and Solymosi arguments are reusable infrastructure. The goal itself is an open problem.

Difficulty

Incidence-geometric methods (Szemerédi–Trotter and its descendants) naturally produce exponents near $4/3$, and passing beyond $4/3$ has required intricate higher-energy arguments yielding only small gains. None of the existing approaches is known to reach exponents close to $2$; even over $\mathbb Z$, where arithmetic structure is available, the best general bounds are the real-number ones.

Formalization scope

Sets are Finset ℤ; $A+A$ and $AA$ are Mathlib's pointwise sumset and product set (open scoped Pointwise), and cardinalities are cast to $\mathbb R$. Powers are real powers (Real.rpow). The empty set is allowed; the hypothesis $\varepsilon<1$ keeps every exponent positive, so the empty set contributes the trivial inequality $0\ge 0$ rather than a junk value $0^0=1$. The constant $C$ may depend on $\varepsilon$ but not on $A$. The Solymosi milestone is stated for $|A|\ge2$ so that $\log|A|>0$.

The statements are for integer sets only; results proved over $\mathbb R$ specialise to them. Contributions of general-purpose infrastructure (Szemerédi–Trotter over $\mathbb R$, multiplicative energy, bounds for the multiplication table) are welcome.

Selected references

• P. Erdős, E. Szemerédi, On sums and products of integers, Studies in Pure Mathematics, Birkhäuser, 1983, 213–218.
• M. B. Nathanson, On sums and products of integers, Proc. Amer. Math. Soc. 125 (1997), 9–16.
• K. Ford, Sums and products from a finite set of real numbers, Ramanujan J. 2 (1998), 59–66.
• G. Elekes, On the number of sums and products, Acta Arith. 81 (1997), 365–367.
• J. Solymosi, Bounding multiplicative energy by the sumset, Adv. Math. 222 (2009), 402–408. https://arxiv.org/abs/0806.1040
• S. V. Konyagin, I. D. Shkredov, On sum sets of sets having small product set, Proc. Steklov Inst. Math. 290 (2015), 288–299. https://arxiv.org/abs/1503.05771
• M. Rudnev, S. Stevens, An update on the sum-product problem, Math. Proc. Cambridge Philos. Soc. 173 (2022), 411–430. https://arxiv.org/abs/2005.11145
• Erdős Problem 52, https://www.erdosproblems.com/52

A Hadamard matrix is a square array of +1s and −1s whose rows are mutually orthogonal — equivalently, one whose determinant attains the absolute maximum that Jacques Hadamard proved in 1893 any ±1 matrix can reach. The story opens earlier, with James Joseph Sylvester's 1867 doubling construction producing such matrices in every power-of-two order; Hadamard himself added orders 12 and 20. The conjecture bearing his name asserts that a Hadamard matrix exists for every order divisible by four. Raymond Paley's 1933 construction from finite fields settled vast new families, and computer searches filled stubborn gaps — beginning with order 92 at JPL in 1962 and reaching order 428 only in 2005, after which 668 became the smallest order whose existence is still unknown. Far from a curiosity, these matrices are workhorses of applied mathematics, underpinning error-correcting codes (the Reed–Muller code that sharpened Mariner spacecraft imagery), spread-spectrum and CDMA signal design, optimal statistical designs of experiments, and coded-aperture spectroscopy. Settling the conjecture would close a 130-year-old gap where combinatorics, number theory, and design theory meet.

Motivation

In the classical secretary problem, candidates arrive one at a time in uniformly random order, and a decision maker must accept or reject each one irrevocably. The decision maker sees exact scores, or at least a total ranking of the candidates seen so far. In hiring, admissions and procurement the observed scores are often biased: evaluations of candidates from different groups, or produced by different evaluators, cannot be compared reliably, even when comparisons inside a group can. Salem and Gupta (SSRN 3444283; Management Science, 2023, doi:10.1287/mnsc.2023.4926) model this by giving the algorithm only the comparisons it can trust. These form a partial order on the candidates, and the true scores remain hidden.

The question is how much is lost when only partial ordinal information is available. The paper's answer is governed by the width of the partial order, the largest number of mutually incomparable candidates. Width 1 is the classical totally ordered problem. Width $N$ means that no comparison is available at all. This mission formalizes the paper's first positive result with explicit constants: an algorithm, ProxyLabel, whose competitive ratio grows linearly in a known estimate of the width.

Setting

A finite set $C$ of $N$ elements carries a partial order $\preceq$. Each element $a$ has a hidden true score $w(a) \ge 0$. The scores are pairwise distinct and consistent with the order: $a \prec b$ implies $w(a) < w(b)$. The width $\omega$ of $(C, \preceq)$ is the largest size of an antichain, a set of pairwise incomparable elements.

The elements arrive in a uniformly random order. The algorithm knows $N$ and a selection capacity $k \ge 1$. At each time it sees the comparisons of $\preceq$ among the elements that have arrived. It may select at most $k$ elements, and every decision is irrevocable. The offline optimum $\mathrm{OPT}$ is the largest total score of at most $k$ elements. An algorithm is $\rho$-competitive if, on every instance,

where $w(\mathrm{Alg})$ is the total score of the selected elements and the expectation is over the arrival order and the algorithm's randomness.

ProxyLabel (Algorithm 1 of the paper) takes a width estimate $\omega' \in \mathbb N$. It works as follows.

1. Each element receives a label $\ell(a) \in \{1, \dots, k\}$, uniformly and independently.
2. It draws $m \sim \mathrm{Bin}(N, \omega'/(\omega'+1))$ and lets the sample $S$ be the first $m$ arrivals. Sampled elements are never selected.
3. A later element $a$ is selected if it is maximal among all previously seen elements with its label, sampled or not, and no element with its label has been selected yet.

Each label class therefore contributes at most one element: the first non-sampled one that beats everything of its label seen before.

Formalization targets

Goal: Proposition 5.2

If $\omega' \ge \omega / c$ for some $c \ge 1$, then ProxyLabel has competitive ratio at most

with the convention $0^0 = 1$. That is, $\mathbb E[w(\mathrm{Alg})] \ge \mathrm{OPT}/\rho$.

Milestones, from the proof (pp. 16–17)

1. Under uniform labels, the $j$-th best element is the maximum of its label class with probability $(1 - 1/k)^{j-1} \ge (1 - 1/k)^{k-1} \ge 1/e$.
2. Display (3): conditional on that event, it is selected with probability at least $\frac{1}{\omega'+1}\big(1 - \frac{1}{\omega'+1}\big)^{\omega}$.
3. If $\omega/c \le \omega'$ with $c \ge 1$, this quantity is at least $1/(e^{c}(\omega'+1))$.
4. Hence each of the top $k$ elements is selected with probability at least $(1 - 1/k)^{k-1}/(e^{c}(\omega'+1))$.
5. $\mathbb E[w(\mathrm{Alg})] \ge \sum_{i=1}^k \mathbb P(a_i \in \mathrm{Alg})\, w(a_i)$ over the top $k$ elements $a_1, \dots, a_k$.

Companion: Corollary 5.1

With the exact width $\omega' = \omega$, the ratio is at most $e(\omega+1)/(1 - 1/k)^{k-1} \le e^2(\omega+1)$, and it is $e(\omega+1)$ for $k = 1$.

Significance

Proposition 5.2 shows that partial ordinal information costs at most a factor linear in the width, provided a width estimate within a constant factor is available. Proposition 5.1 of the same paper shows that no algorithm beats ratio $\omega$, so the bound is order-optimal. ProxyLabel is also the building block of the paper's width-free algorithm PosetLabel (§5.4), which estimates the width from a first sample and then runs ProxyLabel's selection phase.

The result is proved in the paper and has not been machine-checked. A complete development would give a formal model of online selection on a poset under random arrival, with an explicit selection rule and exact finite averages for probabilities. It would also contain a formal use of Dilworth's theorem inside a probabilistic argument, and the elementary inequalities $(1 - 1/k)^{k-1} \ge 1/e$ and $(1 - 1/(\omega'+1))^{\omega} \ge e^{-c}$ in the form the proof needs.

Difficulty

The events of the algorithm are tangled. The sample is a prefix of a random order with a random length. Whether an element is selected depends on everything that arrived before it, on the labels, and on whether an earlier element of the same label was already selected. The bound must be proved for every finite poset and every consistent scoring, with exact constants, on the finite probability space of arrival orders, labellings and sample sizes. The width enters only through the structure of a single label class, a subposet whose width is at most $\omega$, so the argument has to pass from the global width to an arbitrary random subposet.

A tempting simplification lets every passing unsampled element be selected. That algorithm can select several elements of one label, so its expected score is larger and the bound becomes easier. It is not ProxyLabel.

Formalization scope

• Elements are a finite type α with a PartialOrder, so $N$ is Fintype.card α. The width $\omega$ is the published definition AppliedComb.Posets.width α, the maximum size of an antichain. Dilworth's theorem is the published, proved theorem AppliedComb.Posets.dilworth.
• A consistent scoring is $w : \alpha \to \mathbb R$ with $w \ge 0$, $w$ injective, and $a < b \Rightarrow w(a) < w(b)$. These three conditions are the paper's standing assumptions (§3.1, §3.3), not additions.
• Arrival orders are bijections α ≃ Fin N, and labellings are functions α → Fin k. Labels are independent of the order, which is the same distribution as assigning labels on arrival.
• Probabilities and expectations are explicit finite averages with weights $1/N!$, $1/k^N$ and the binomial weights $\binom{N}{m}p^m(1-p)^{N-m}$ with $p = \omega'/(\omega'+1)$.
• The selection rule is encoded exactly. An element is selected iff it is unsampled, no earlier element of its label (sampled or not) is above it, and no earlier unsampled element of its label passed the same test.
• OPT is the maximum of $\sum_{a \in s} w(a)$ over sets with $|s| \le k$, so it is the total score when $k \ge N$.
• The competitive ratio is stated as $\mathrm{OPT}/\rho \le \mathbb E[w(\mathrm{Alg})]$. This agrees with Definition 3.4 when $\mathrm{OPT} > 0$; the page's ratio is undefined when $\mathrm{OPT} = 0$.
• $(1 - 1/k)^{k-1}$ has a natural exponent, so $k = 1$ gives $0^0 = 1$. The width estimate $\omega'$ is a natural number.
• The proposition's "interval order" is a slip of the page: the algorithm and the proof concern arbitrary posets, and the goal is stated for every finite poset.
• The order-optimality clause of Corollary 5.1 refers to Proposition 5.1, the subject of mission II of this series, and is not stated here.
• The goal is a statement about the full expectation of the selected score over arrival order, labels and sample size. It is not the conditional bound (3). A formalization in which several elements per label can be selected, or in which "previously seen" excludes the sample, proves a statement about a different algorithm.