Combinatorics

Motivation

Discrepancy theory asks how unbalanced a two-coloring of a combinatorial structure must be in the worst case. Concretely: given $n$ sets over an $n$-element ground set, color each element $+1$ or $-1$ so that every set is as close to balanced as possible. The question is classical (Beck–Fiala 1981; Spencer 1985) and the answer for general (dense) set systems is one of the sharpest gaps between a naive probabilistic bound and the truth known in combinatorics: assigning colors uniformly at random only guarantees discrepancy $\Theta(\sqrt{n\log n})$, yet a coloring with discrepancy $O(\sqrt n)$ always exists — the logarithmic factor is an artifact of the naive argument, not of the problem. This mission formalizes that removal, following T. Rothvoß's lecture-note exposition of J. Spencer's entropy method (MIT 18.095, "Discrepancy theory"), the standard modern presentation of the technique (see also Matoušek, Geometric Discrepancy, Ch. 4). The entropy method is the ancestor of the whole "partial coloring" family of arguments used throughout discrepancy theory and combinatorial algorithm design, so a machine-checked account of its base case is reusable well beyond this one theorem.

Setting

Fix $n\ge 1$ and an $n\times n$ matrix $A$ with entries in $\{0,1\}$, thought of as the incidence matrix of $n$ sets $S_1,\dots,S_n$ over an $n$-element ground set: $A_{ij}=1$ iff element $j$ lies in set $S_i$. A coloring is a map $\varepsilon:\{1,\dots,n\}\to\{-1,+1\}$, and the discrepancy of row $i$ under $\varepsilon$ is $\bigl|\sum_j A_{ij}\varepsilon_j\bigr|$, the signed imbalance of set $S_i$. The discrepancy of the matrix is the value achieved by the best coloring, minimizing the worst row.

The entropy method bounds this via the partial coloring lemma: rather than coloring all $n$ elements at once, one repeatedly colors a constant fraction of the currently uncolored elements while keeping every row's contribution small, then recurses on what remains. Each round is itself produced by an entropy/pigeonhole argument: quantize each row's signed sum (under a uniformly random coloring) into $O(1)$ "shells" of width $\Theta(\sqrt m)$ (where $m$ is the number of active elements); a short computation shows this quantization carries very little Shannon entropy $H(Z)=\sum_x \Pr[Z=x]\log_2\frac{1}{\Pr[Z=x]}$ once the shell width exceeds a threshold; subadditivity of entropy across the $n$ rows then bounds the joint quantization entropy, which by pigeonhole forces an exponentially large set of colorings landing in the same joint shell; Kleitman's theorem on the diameter of a large subset of the Hamming cube then extracts two such colorings that are far apart in Hamming distance, and their difference is the sought partial coloring.

Formalization targets

Goal.

This is the qualitative, constant-suppressed form of Spencer's theorem: it asserts $O(\sqrt n)$ discrepancy with a single universal constant, and deliberately leaves that constant unspecified. This is the right goal for this mission because it is the weakest statement that is still stable: any future improvement to the constant (down to Spencer's sharp $6$, or beyond) refines this theorem rather than invalidating it.

Significance

The removal of the $\sqrt{\log n}$ factor is the entire content of Spencer's theorem: it is what separates discrepancy theory from a corollary of concentration inequalities, and the partial-coloring/entropy method it introduced underlies later results throughout the field (Beck–Fiala-type bounds, the Komlós conjecture literature, and constructive/algorithmic discrepancy minimization). Formalizing it is formalizing the base case that every later partial-coloring argument specializes.

This mission's goal theorem, spencer_discrepancy_sqrt_n_bound, is already proved (zero sorrys), by a from-scratch entropy-method development: the per-row shell-entropy bound, the joint pigeonhole-and-Kleitman assembly for one round, and the outer geometric iteration and induction combining rounds into a full coloring. What remains open in this mission is shannonEntropy_shellFin_le (Lemma 9 in Rothvoß's notes) — the per-row entropy bound is currently imported as an assumption by the one-round lemma lemma8_partial_coloring_round, which is therefore only conditionally proved pending it. A separate, harder mission on this platform (Komlos.spencer_six_deviations) targets Spencer's sharp constant $6$ via a tighter, non-standard numeric derivation; that is a distinct, substantially harder target and this mission does not duplicate it.

Difficulty

The obvious argument is: fix a target bound $t=\lambda\sqrt n$, use a Chernoff/Hoeffding bound to show each row fails with probability at most $2e^{-\lambda^2/2}$, union-bound over the $n$ rows, and take a coloring outside the bad event. This works to prove a single good coloring exists — but it is not strong enough to survive being iterated to remove the entire uncolored set, because a per-row union bound loses a factor of $n$ that a fixed $\lambda$ cannot always absorb once the active column count $m$ is close to $n$: for the scaling family where the row count and the active set shrink together, the naive union bound's failure probability grows linearly in $m$, not exponentially, exactly canceling the exponential decay one is trying to exploit. The fix is to bound the joint entropy of all $n$ rows' quantizations at once (subadditivity of Shannon entropy), rather than union-bounding row-by-row failure events; this is genuinely a different technique, not a tightening of the same one, and it is the reason the entropy method is presented as its own tool rather than a Chernoff-bound corollary.

Formalization scope

Matrices are Fin n → Fin n → ℝ with an explicit ∀ i j, A i j = 0 ∨ A i j = 1 hypothesis; colorings are represented two ways in this development — Fin m → Bool internally (via the platform definition RSign converting to $\pm1$) during the entropy/Kleitman argument, and directly as Fin n → ℝ constrained to $\{-1,1\}$ pointwise in the goal theorem's statement, matching the usual $\{\pm1\}$-coloring convention. The row-sum shell quantization is the platform definitions rowSumB, shellIdx, shellFin (an integer-valued "round to nearest shell" construction, packaged into a fixed Fin (2m+3) type for entropy purposes). The active column set during the outer iteration is tracked as a shrinking Finset (Fin n) of the original index type throughout, rather than moving between different Fin m types round to round, which keeps the induction free of type-level bookkeeping.

Reusable, already-Proved infrastructure this development builds on: shannonEntropy_pi_le (subadditivity across independent rows), shannonEntropy_pigeonhole, choose_sum_le_exp_mul_binEntropy, and kleitman_diameter, all already Proved on the platform independent of this mission. The one genuinely open piece — and the mission's standing invitation — is shannonEntropy_shellFin_le (Lemma 9): a self-contained Shannon-entropy computation about the shellFin quantization that does not depend on anything else in this mission and can be attempted independently.

Selected references

• J. Spencer, Six standard deviations suffice, Trans. Amer. Math. Soc. 289 (1985), 679–706. DOI
• T. Rothvoß, Discrepancy theory, or: how much balance is possible?, MIT 18.095 lecture notes. PDF
• J. Matoušek, Geometric Discrepancy: An Illustrated Guide, Algorithms and Combinatorics 18, Springer, 1999.
• J. Beck, T. Fiala, "Integer-making" theorems, Discrete Appl. Math. 3(1) (1981), 1–8.

A graph $H$ is $r$-degenerate if every nonempty subgraph of $H$ has a vertex of degree at most $r$. Erdős conjectured — this is Erdős problem #146 — that every fixed bipartite $r$-degenerate graph $H$ satisfies

The conjecture was known in several cases: when one bipartition class has maximum degree at most $r$, for $r$-degenerate blow-ups of trees, and, for $r = 2$, for grids and certain critical 2-degenerate graphs. The best general bound was the weaker $\mathrm{ex}(n,H) = O(n^{2-1/(4r)})$ of Alon, Krivelevich and Sudakov.

This mission carries a complete Lean 4 formalisation refuting it at $r = 2$.

Theorem. There exist a fixed connected bipartite 2-degenerate graph $H$ and constants $c, \varepsilon > 0$ such that

for all sufficiently large $n$. Since the conjectured bound at $r = 2$ is $O(n^{3/2})$, the excess is polynomial rather than constant, so the conjecture fails outright. A related conjecture of Erdős (problem #113) asserts that a bipartite graph is 2-degenerate if and only if $\mathrm{ex}(n,H) = O(n^{3/2})$; Janzer had already disproved the reverse implication, and this result refutes the forward one.

The construction. The counterexample $H$ is built in layers: starting from a layer $V_0$ of size $L_0$, each subsequent layer is $V_i = \binom{V_{i-1}}{2}$, and every vertex $\{a,b\} \in V_i$ is joined to its two parents $a, b \in V_{i-1}$. The result is connected, bipartite and 2-degenerate by construction, and is related to the complete degenerate graphs of Grzesik, Janzer and Nagy.

The lower bound comes from a sampled Hamming-ball graph. With $U = \{0,1\}^m$, two disjoint copies $U_L, U_R$ are joined whenever their Hamming distance is at most $k = \lfloor \tau m\rfloor$, and each vertex is retained independently with probability $p = 2^{-\beta m}$. The two parameters are governed by the thresholds

and the construction needs a sampling exponent with $A(\tau) < \beta < C(\tau)$. The lower threshold controls exclusion of the layered graph; the upper one controls whether the sampled host has more than $n^{3/2}$ edges.

Exclusion runs on a conditional-entropy functional $E(u,z) = \frac{1}{m}\sum_j H(Z_j \mid X_j, Y_j)$ over parent and child arrays. An array of conditional entropy $E$ has at most $2^{mME + O(m\log_2 M)}$ realisations, while requiring its $M = \binom{L}{2}$ children to survive sampling costs $2^{-\beta mM}$ — which dominates the $2^{mL}$ possible parent arrays whenever $E < \beta$. An embedding of $H$ would therefore have to raise a bounded entropy potential by a fixed amount at each layer, which is impossible after enough layers. A second-moment argument shows the sampled graph still has $\Omega(n^{3/2+\varepsilon})$ edges, and padding extends the construction to every sufficiently large order.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers", Sections 1.2 and 5–8), and re-verified in this environment: every node is proved from [propext, Classical.choice, Quot.sound] alone, and each staged statement's elaborated type was checked to be identical to the original declaration's. The mission is offered as a curated, closed campaign whose definitions and lemmas — binary entropy and the pair kernel, the layered construction, the Hamming-ball host and its retention measure — are reusable foundations for further work in extremal graph theory.

This is the companion result to Erdős problem #180, the Erdős–Simonovits compactness conjecture, which is formalised in the same source chapter and published as a separate mission.

Erdős and Simonovits conjectured that forbidding a finite family of graphs cannot reduce the extremal number by more than a constant factor compared with forbidding one of its members: for every finite nonempty family $\mathcal{F}$ whose members all contain a cycle, there should be some $F \in \mathcal{F}$ and $C>0$ with $\mathrm{ex}(n,F) \le C\,\mathrm{ex}(n,\mathcal{F})$ for all large $n$. The cycle hypothesis is essential — the folklore family $\{K_{1,2}, 2K_2\}$ already defeats the original formulation — and the corrected conjecture is Erdős problem #180.

This mission carries a complete Lean 4 formalisation refuting it, and refuting it quantitatively: there is a finite family $\mathcal{F}$ of connected bipartite graphs, each containing a cycle, with

The two bounds are separated by a polynomial factor $n^{1/48}$, so no member can dominate the family up to any constant. The family is $\mathcal{F} = \{C_4, C_6\} \cup \mathcal{J} \cup \mathcal{K}$, where $\mathcal{J}$ and $\mathcal{K}$ are the admissible quotients of two properly $2$-coloured templates built from the subdivisions of $K_{3,2}$ and $K_{3,3}$. The upper bound comes from counting short paths in an $\mathcal{F}$-free graph: excluding $\mathcal{J}$ bounds the number of vertices that fail to be centres of a subdivided $K_{3,3}$, and excluding $\mathcal{K}$ forces those vertices to form a vertex cover. The lower bound comes from incidence graphs of symplectic generalized quadrangles $W(q)$, with the characteristic of the underlying field chosen to suit the forbidden member — even $q$ for $\mathcal{J}$, odd $q$ for $\mathcal{K}$ — which is exactly the freedom a family bound does not have.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science (Chapter 10, "Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers"), re-verified in this environment. Every node is proved; the mission is offered as a curated, closed campaign whose definitions and lemmas are reusable foundations for further work in extremal graph theory.

How fast do multicolour Ramsey numbers grow? Write $R_k$ for the least $n$ such that every colouring of the edges of $K_n$ with $k$ colours contains a monochromatic triangle. The classical bounds, essentially unimproved for decades, place $R_k$ between $c^k$ and $e\cdot k!$, and Erdős asked repeatedly whether the truth is closer to the exponential lower end — his Problem 183 asks whether $R_k^{1/k}\to\infty$, i.e. whether the growth is genuinely superexponential.

This mission carries a complete Lean 4 formalisation resolving that question in the affirmative, with an explicit bound: $R_k \ge \left(\tfrac{1}{6e^{38}}\,k^{1/3}/\log k\right)^{k}$ for all sufficiently large $k$, from which $R_k^{1/k}\to\infty$ follows, together with the matching two-sided estimate $\log R_k = \Theta(k\log k)$ pinning the sharp coefficients. The argument is constructive: it builds triangle-free colourings by a recursive palette construction whose colour count grows fast enough to beat every exponential.

The material is transplanted from the Lean 4 formalisation accompanying OpenAI's Ten Advances in Mathematics and Theoretical Computer Science, re-verified in this environment. Every node is proved — the mission is offered as a curated, closed campaign whose milestones map the attack path and whose lemmas are reusable foundations for further work on multicolour Ramsey theory.

Erdős Problem 788 asks how large a set can always be retained when prescribed distinct pair-sums are forbidden. This mission formalizes the repository’s strengthened version of Theorem 1.1: an explicit lower bound valid for every $n\ge 3$, an eventual quantitative upper bound, the conclusion $f(n)=n^{1/2+o(1)}$, and the exact affirmative answer to the original upper-bound question.

Motivation

A tournament is a directed graph in which every two distinct vertices are joined by exactly one arc — the model of a round-robin competition, and the setting of Ramsey theory's oldest questions.

In 1982 Sands, Sauer and Woodrow asked: if the arcs of a tournament are coloured with two colours, must some vertex be reachable from every other vertex along a monochromatic path, one whose arcs all carry the same colour? They answered yes [SSW82, Corollary 2, p. 273], through a theorem on arbitrary digraphs [SSW82, Theorem 1, pp. 271–273]. That theorem is also the two-colour case of kernel theory: kernels are independent dominating sets, they exist in digraphs whose arcs split into two transitive classes, and the stable-marriage theorem is a special case [Ch26, §1].

The tournament statement is the settled case of a question of Erdős that remains open: with three colours, must either a rainbow directed triangle occur, or a vertex reach every other vertex monochromatically [SSW82, PROBLEM, p. 275]? The platform already carries that open problem as the mission "Monochromatic reachability or rainbow triangles" (OPG1808.root_problem). This mission is the two-colour theory beside it, not a duplicate: it collects the results that are known and that any attack on the three-colour question builds on.

Timeline. Sands–Sauer–Woodrow (1982) prove Theorem 1, deduce the two-colour tournament statement, exhibit a three-coloured tournament with no vertex reaching all others, and ask whether three colours force a rainbow triangle or such a vertex [SSW82]. Shen Minggang (1988) proves the theorem for any number of colours when no triangle carries three distinct colours [Mi88]. Galeana-Sánchez and Rojas-Monroy (2005) give a six-vertex four-coloured tournament with neither, so three colours is the last case of the rainbow formulation [GR05]. Bousquet, Lochet and Thomassé (2017) show that a k-coloured tournament has a dominating set of size $O(\ln 2k \cdot k^{k+2})$ built from monochromatic paths — bounded, but not the single vertex of the two-colour case [BLT17]. Chancelier (2026) gives the first machine-checked proof of the general theorem, in Rocq, and records that no Lean formalization exists [Ch26].

Setting

Fix a vertex type $V$. A digraph is a relation $D : V \to V \to \mathrm{Prop}$, written $x \to y$; an arc colouring assigns each ordered pair a colour in $\mathrm{Fin}\,3$; a colouring uses at most two colours when every arc has colour $0$ or colour $1$. A tournament is a loopless digraph in which every two distinct vertices are joined by exactly one arc.

A monochromatic path from $x$ to $y$ has distinct vertices, consecutive ones joined by an arc, all those arcs of one colour; write $x \rightsquigarrow y$ when one exists, and say that $x$ monochromatically reaches $y$. A set $S$ is monochromatically independent when no two distinct members are connected by a monochromatic path in either direction — this is not graph independence: in a tournament a single arc joins any two vertices, so such a set has at most one element. A digraph has no monochromatic infinite outward path when no injective $x : \mathbb{N} \to V$ has all arcs $x_n \to x_{n+1}$ of one colour.

Formalization targets

Goal — the two-coloured tournament theorem (SSW Corollary 2)

$D$ a tournament on a nonempty finite vertex type, its arcs coloured with at most two colours:

Milestone — the two-coloured digraph theorem (SSW Theorem 1)

$D$ any digraph on any vertex type, arcs coloured with at most two colours, with no monochromatic infinite outward path:

Milestone — the source form of the goal

The goal in the orientation of the platform's existing definition, the distinguished vertex reaching the others:

Milestone — the blocked three-coloured theorem (SSW Theorem 3)

$T$ a tournament whose arcs carry three colours and whose vertices are partitioned into blocks, two vertices of different blocks always joined by a red arc and two of the same block by a blue or a green arc; then some vertex is monochromatically reached by every other.

Significance

The result. The goal settles the two-colour case of Erdős's question in the sharp form that one vertex suffices, and it is the base of the known theory: the paper's own block-coloured three-colour theorem is proved from it by iteration, and the kernel and stable-matching corollaries of the general theorem make it standard digraph theory. Without it the three-colour question has no settled case to compare against.

Formalizing it. No Lean formalization of these statements is recorded, for the corollary or for the general theorem [Ch26]; the machine-checked development that exists is in Rocq, for the general theorem, and is the first for the infinite case. This mission produces, in Lean, a classical theorem the platform does not have, together with the definitions it rests on: monochromatic reachability and monochromatic independence over an arbitrary vertex type. Status is stated per target: the goal is a theorem of the source paper, not an open question; the three-colour problem beside it remains open.

Difficulty

The first idea — take a longest monochromatic path and read off its end — does not close the argument. It gives monochromatic reachability only for the vertices on the path; for a vertex outside it, one knows only that the arcs from the path to that vertex cannot continue the path's colour, which yields no path back to the path's end. The source instead takes a maximal element, under a relation mixing the two colours, of a family of monochromatically independent sets — $S \preceq T$ when every $s \in S$ has $s \in T$, or a blue path to some $t \in T$ with no red path back — and shows by a minimal-counterexample argument on red reachability that a maximal element is the required set. Over an arbitrary vertex type the family needs Zorn's lemma, and the no-infinite-outward-path hypothesis, not finiteness, is what bounds the argument. A second trap is definitional: because independence here is monochromatic, the tournament case collapses to one vertex; a formalization using graph independence would state a different and false theorem.

Formalization scope

• Reuses the platform module opg1808_colored_tournaments: Digraph V := V → V → Prop, ArcColoring V := V → V → Fin 3, IsTournament, and MonochromaticallyReaches, the reflexive-transitive closure of one colour's arcs. A new definition supplies monochromatic independence; prose and statements use the same notation.
• Colours are three-valued even when two occur, matching that module; the two-colour hypothesis says every arc has colour $0$ or colour $1$. Relabelling two used colours into $\{0,1\}$ preserves which paths are monochromatic, so nothing is lost.
• The source allows loops and multiple edges; the formalization uses a simple relation. Multiple edges are irrelevant, since reachability depends only on the presence of an arc, and loops are excluded by IsTournament. For the general digraph target loops change nothing, as the source's paths have distinct vertices.
• The source's paths have distinct vertices while MonochromaticallyReaches uses walks; the two agree for reachability, and independence is stated through walks, so no distinctness hypothesis is needed.
• The goal is stated on [Fintype V] [Nonempty V]; nonemptiness is required, the target being false on an empty vertex type. The general target is stated on an arbitrary type, and its hypothesis is vacuous in the finite case, which is the entry point for the goal.
• The platform's IsMonochromaticSource is the reversed orientation of the goal; the goal follows the source paper, which orients paths towards the distinguished vertex.

Needed: the reused module, a definition of monochromatic independence, reachability lemmas for two colour classes, and for the general target Zorn's lemma and infinite outward paths. The reachability and independence layer is reusable by any later mission on coloured digraphs, including the three-colour problem beside this one. Contributions to any target are welcome.

Selected references

• B. Sands, N. Sauer, R. Woodrow, On monochromatic paths in edge-coloured digraphs, J. Combin. Theory Ser. B 33 (1982), no. 3, 271–275. Theorem 1 (pp. 271–273), Corollary 2 (p. 273), Theorem 3 (pp. 274–275), PROBLEM (p. 275). https://doi.org/10.1016/0095-8956(82)90047-8
• S. Minggang, On monochromatic paths in m-coloured tournaments, J. Combin. Theory Ser. B 45 (1988), 108–111. https://doi.org/10.1016/0095-8956(88)90062-2
• H. Galeana-Sánchez, R. Rojas-Monroy, Monochromatic paths and at most 2-colored arc sets in edge-coloured tournaments, Graphs Combin. 21 (2005), 307–317. https://doi.org/10.1007/s00373-005-0627-y
• M. Melcher, K. B. Reid, Monochromatic sinks in nearly transitive arc-colored tournaments, Discrete Math. 310 (2010), 2697–2704. https://doi.org/10.1016/j.disc.2010.05.017
• N. Bousquet, W. Lochet, S. Thomassé, A proof of the Erdős–Sands–Sauer–Woodrow conjecture, arXiv:1703.08123 (2017). https://arxiv.org/abs/1703.08123
• J.-P. Chancelier, A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect, arXiv:2604.21376 (2026). https://arxiv.org/abs/2604.21376
• Open Problem Garden, Monochromatic reachability or rainbow triangles. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles