Combinatorics

Motivation

Additive combinatorics studies what arithmetic structure follows from statistical signals. The Balog–Szemerédi–Gowers theorem is its central regularity statement: a pair of finite sets with large additive energy (many additive quadruples) contains large subsets whose sumset is small. Balog and Szemerédi proved the first version in 1994 using the regularity lemma, which gave a tower-type dependence between the parameters; Gowers obtained a polynomial dependence in 1998. The theorem powers results across the field — from sum-product estimates to the structure of sets with small doubling — and its proof assembles three reusable machines: dependent random choice, the popular-sum graph, and Ruzsa calculus.

Setting

Work in an arbitrary abelian group $G$ (Lean: AddCommGroup G). For finite $X, Y \subseteq G$, the additive energy $E(X,Y)$ counts quadruples $(x,x',y,y')$ with $x + y = x' + y'$; the trivial maximum is $|X|^3$ when $|X| = |Y|$. The sumset $X + Y$ is $\{x + y\}$, and the difference set $X - Y$ is defined pointwise. A set has small doubling when $|X + X|$ is linear in $|X|$. The Lean development uses Finset.addEnergy and Finset.addConvolution from Mathlib.

A bipartite graph here is an edge set $E$ of type Finset (G × G) with $E \subseteq A \times^s B$, not a Mathlib SimpleGraph; solvers should state graph hypotheses that way. Given such an $E$, the partial sumset $A +_E B$ is $\{a + b : (a,b) \in E\}$, following Tao–Vu Definition 2.28.

Target

The mission goal is the two-set (equal-cardinality) form:

$$E(X,Y) \ge \eta |X|^3 \implies \exists X' \subseteq X, Y' \subseteq Y,\ |X'|,|Y'| \ge c|X|,\ |X' - Y'| \le C|X|.$$

This statement is assembled from the sources rather than quoted from them: Tao–Vu Lemma 2.30 supplies the energy-to-graph step, Fox–Sudakov §5.1 (the same theorem as Tao–Vu Theorem 2.29) supplies the graph-level bound, and Ruzsa calculus converts a sumset bound into the difference-set bound above. No cited work states this exact form, and the goal deliberately keeps $c$ and $C$ existential; the explicit-constant variant is proved separately in the mission with $c = \eta/16$.

The four milestones follow the sources' own numbering and are, in dependency order, Fox–Sudakov Lemma 5.1, Fox–Sudakov Lemma 5.2, the Fox–Sudakov §5.1 / Tao–Vu Theorem 2.29 graph bound with explicit constants, and Tao–Vu Lemma 2.30. The first three lie on the goal's proof path; the fourth is the reusable packaging of the energy-to-graph step.

Significance

The result converts a purely statistical hypothesis (many additive quadruples) into genuine algebraic structure (a large subset with a small difference set) with polynomial losses — the step that makes energy methods usable. It is a standard tool behind quantitative Freiman-type arguments.

Formalizing it matters because the constants are the content: the development tracks explicit constants through dependent random choice (graph level $c = \delta/8$ and $C = 2^{13}K^3/\delta^5 + 2^{12}/\delta^5$; energy level $c_0 = \eta/16$ and $C_0 = 2^{13}(4/\eta)^3/(\eta/2)^5 + 2^{12}/(\eta/2)^5$), which paper proofs often leave implicit. Fox–Sudakov state the application for sets of integers; the formalization is over an arbitrary AddCommGroup, with no further hypothesis on the group. Mathlib at the pinned revision (v4.33.1) contains no BSG statement, so this fills a genuine upstream gap.

Difficulty

The hard step is dependent random choice: sampling a random vertex subset of the popular-sum graph must simultaneously keep many vertices and keep the induced subgraph dense, and the two requirements fight each other. The naive first idea — take the densest neighborhood — loses control of the vertex count; the fix is a two-stage Markov-plus-payoff selection whose density analysis needs the exact path-count lower bound, not just an order estimate.

Two places where the formalization departs from Fox–Sudakov are recorded on the affected statements rather than hidden: the length-three path count admits degenerate paths (the source's $a' \ne a$ and $b' \ne b$ terms are dropped, which weakens the conclusion and is sound for the BSG use), and the density parameter is instantiated at a guaranteed lower bound rather than the exact edge density.

Formalization scope

Sets are Finset G in an AddCommGroup G with DecidableEq; energy is Finset.addEnergy; graphs are edge sets Finset (G × G), with the pointwise sumset and difference operations from open scoped Pointwise. Density hypotheses are stated with explicit real constants. The counting lemmas at the bottom of the development (sum_addConvolution_eq_card_product, path3_count_le_triple_rep_count, restricted_sumset_via_multiplicity) are unconditional; the statements that need them carry the nonemptiness, equal-cardinality and density hypotheses that exclude degenerate zero-energy configurations. Welcome contributions: the single-set polynomial Freiman–Ruzsa consequences, and non-abelian variants.

Selected references

• A. Balog and E. Szemerédi, A statistical theorem of set addition, Combinatorica 14 (1994), 263–268.
• W. T. Gowers, A new proof of Szemerédi's theorem for arithmetic progressions of length four, Geom. Funct. Anal. 8 (1998), 529–551.
• J. Fox and B. Sudakov, Dependent random choice, Random Structures & Algorithms 38 (2011), 68–99 (Lemmas 5.1/5.2 and §5.1 BSG application).
• T. Tao and V. Vu, Additive Combinatorics, Cambridge Univ. Press (2006), Definition 2.28 (partial sumsets), Theorem 2.29 (BSG, p. 79) and Lemma 2.30 (energy to partial sumset, p. 80).
• C. Reiher and T. Schoen, Note on the theorem of Balog, Szemerédi, and Gowers, Combinatorica 44 (2024), no. 3, 691–698 (arXiv:2308.10245).
• I. Ruzsa's inequalities via Mathlib's Finset.pluennecke_ruzsa_inequality_nsmul_add; see G. Petridis, New proofs of Plünnecke-type estimates for product sets in groups, Combinatorica 32 (2012), 721–733 (arXiv:1101.3507).
• McKenna, Lean formalization (mathlib-only, axiom-clean), lean-formalizations, modules Combinatorics/Additive/BalogSzemerediGowers and BSGEnergyToGraph.

Motivation

The first two missions in this programme counted order-three squares. Mission I proved MacMahon's magic count $M_{3}(3e)=2e^{2}+2e+1$ and Mission II his semi-magic count $H_{3}(t)=3\binom{t+3}{4}+\binom{t+2}{2}$. What neither does is classify: counting tells you how many squares there are, but not what they look like.

This mission closes that gap for the most classical case of all. A normal magic square of order three is a $3\times3$ array containing each of $1,2,\dots,9$ exactly once, whose rows, columns and two main diagonals all sum to the magic constant $15$. The statement to be proved is the uniqueness of the Lo Shu square:

every normal magic square of order three is one of the eight images of $\begin{pmatrix}4&9&2\\3&5&7\\8&1&6\end{pmatrix}$ under the symmetry group of the square.

In particular there are exactly $8$ of them, and they form a single orbit under the dihedral group $D_{4}$.

Setting

MacMahon's parametrization (already formalized in MagicSquaresParam3) writes every order-three magic square of line sum $3e$ as

$$\mathrm{mkMagic3}(e,a,c)= \begin{pmatrix} a & 3e-a-c & c\\ e+c-a & e & e+a-c\\ 2e-c & a+c-e & 2e-a \end{pmatrix},$$

with $(a,c)$ ranging over the finite admissible set paramSet e. For a normal square the magic constant is $15$, so $e=5$ and the centre entry is $5$.

Normality (IsNormal) means every entry lies in $[1,9]$ and the nine entries are pairwise distinct — equivalently, they are a permutation of $1,\dots,9$.

Formalization targets

Goal — Lo Shu uniqueness

\\#\\{(a,c)\in \\mathrm{paramSet}\\ 5 : \\mathrm{mkMagic3}(5,a,c)\\ \\text{is normal}\\} = 8,

together with the identification of those eight parameter pairs. By the bijection magic_three_param_bij this is exactly the statement that there are eight normal magic squares of order three, i.e. that Lo Shu is unique up to the symmetry group of the square.

The route

1. Normality bounds the parameters. If $\mathrm{mkMagic3}(5,a,c)$ is normal then $1\\le a\\le 9$ and $1\\le c\\le 9$, because $a$ and $c$ are corner entries. This reduces the classification to a finite search over $81$ pairs.
2. Classification (magic_three_normal_classify). Within that range, $\mathrm{mkMagic3}(5,a,c)$ is normal exactly when $(a,c)$ is one of

$$\\{(2,4),(2,6),(4,2),(4,8),(6,2),(6,8),(8,4),(8,6)\\}.$$

The eight surviving pairs are precisely those with $a,c$ distinct corners of the Lo Shu square; the excluded ones are those with $a+c=10$, for which the $(2,1)$ entry $a+c-5$ collides with the centre $5$. 3. Converse (magic_three_normal_converse). Each of the eight pairs really does give a normal square.

Significance

The result itself. The uniqueness of Lo Shu is the oldest non-trivial classification in combinatorics — it is the order-three case of the classification problem for magic squares, and the reason $n=3$ is special: for $n=4$ there are $880$ normal squares (up to symmetry) and for $n\ge 5$ no classification is known. Formalizing it shows that the counting machinery of Missions I and II can be turned around and used as a classification tool: the parametrization plus a finite verification give the complete list, not just the cardinality.

Formalizing it. The whole proof is a finite case check over $81$ parameter pairs, so the mathematical content is small and the formalization difficulty is concentrated in making the finiteness usable. Two things have to be arranged before automation can see the problem:

• IsNormal is stated with a Function.Injective, which is not decidable as stated; it must first be rewritten into an explicit conjunction of entrywise bounds and pairwise inequalities over Fin 3.
• The quantifiers over Fin 3 do not unfold by simp alone; one needs Fin.forall_fin_succ to expand them before norm_num can decide the $81$ resulting ground instances.

Difficulty

Finiteness must be manufactured. Nothing in IsNormal mentions a bound on $a$ or $c$, so the first step is to derive $1\le a,c\le 9$ from the entrywise bounds of normality. Skipping it leaves an infinite search that interval_cases cannot start.

Truncated subtraction. The parametrization is written over $\mathbb{N}$, so entries such as $a+c-5$ and $15-a-c$ truncate at zero. Every ground instance must be evaluated with the truncation in place — which is why the classification is carried out by evaluating the actual entries rather than by manipulating symbolic inequalities.

Formalization scope

• Normal means: entries in $[1,n^{2}]$ and pairwise distinct (IsNormal).
• The classification is over MacMahon parameters, so it inherits the parametrization of MagicSquaresParam3 and the bijection of Mission I.
• Trivializing formalizations are ruled out: the goal is not a declaration that some finite set has eight elements, but a derived classification — normality must be characterized by an explicit list of parameter pairs.
• Reusable beyond this mission: the decidable reformulation of IsNormal for Fin 3 (and the Fin.forall_fin_succ technique for unfolding finite quantifiers), the list of the eight Lo Shu parameters, and the order-three classification itself.

Selected references

• P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916.
• M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717. https://arxiv.org/abs/math/0201013
• W. S. Andrews, Magic Squares and Cubes, 2nd ed., Dover, 1960 (the classical enumeration for $n=4$).

Motivation

Set cover is the standard worked example of the primal-dual method, and Chapter 2 of Buchbinder's thesis uses it that way: it is where the machinery of §2.1 is first turned on a concrete NP-hard problem. Two analyses appear. The greedy algorithm, analysed by dual fitting, buys the set with the best cost-per-newly-covered-element ratio and charges the price to the elements it covers; the resulting element prices form an infeasible dual that becomes feasible after scaling by $H_n$. The primal-dual algorithm instead raises the price of an uncovered element until some set's constraint goes tight, buys that set, and repeats; the resulting dual is feasible, and each bought set is paid for by elements of frequency at most $f$, giving an $f$-approximation.

Both analyses have the same shape, and it is the shape that matters for the rest of the series: the algorithm never sees the optimum. It maintains a dual solution, and the approximation ratio falls out of comparing the primal it built against the dual it accumulated.

Setting

An instance consists of a finite type $E$ of elements, a finite type $S$ indexing available sets, an assignment $s \mapsto A_s \subseteq E$, and a nonnegative cost $c : S \to \mathbb{R}$. Every element is assumed to lie in at least one available set; the source leaves this implicit, and without it no cover exists and the approximation statements are vacuous. The covering LP and its packing dual are

$$(P)\quad \min \sum_{s} c_s x_s \ \text{ s.t. } \sum_{s : e \in A_s} x_s \ \ge\ 1 \ \ (\forall e \in E), \quad x \ge 0,$$ $$(D)\quad \max \sum_{e} y_e \ \text{ s.t. } \sum_{e \in A_s} y_e \ \le\ c_s \ \ (\forall s \in S), \quad y \ge 0.$$

The frequency of an element is the number of sets containing it, and $f$ denotes the maximum frequency over all elements.

The two standing assumptions — nonnegative costs, and every element lying in some available set — are carried by a bundled SetCoverInstance, not passed as loose hypotheses. Every source-facing statement in the mission takes such an instance and reads those facts off its fields, so none of them can be instantiated at data violating either. The two indicator lemmas are the exceptions and are labelled as generalized assisting results: one has no cost function in scope at all, and the other's hypothesis that a given $C$ covers is strictly stronger than coverability of the family.

Costs are permitted to be zero and the ground type is permitted to be empty. No Nonempty E hypothesis appears anywhere; when $E$ is empty, $f = 0$ and the $f$-approximation bound reads $\mathrm{cost}(C) \le 0$, which the certificate's tightness clause forces to be $0 \le 0$ rather than anything false.

Formalization targets

The results are stated about certificates, not about executable algorithms. This is the central modelling decision of the mission and it is deliberate: the mathematical content of the source's proofs is entirely a statement about the invariants the output satisfies, and separating that from the question of whether a particular procedure produces such output keeps each half provable on its own.

A primal-dual certificate is a pair $(C, y)$ where $C \subseteq S$ covers $E$, $y$ is dual-feasible, and every $s \in C$ has a tight dual constraint, $\sum_{e \in A_s} y_e = c_s$.

Goal — the primal-dual $f$-approximation

For any primal-dual certificate $(C,y)$ and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{s \in S} c_s x_s .$$

Since this holds against every fractional cover, it holds in particular against an optimal one, so the cover $C$ costs at most $f$ times the fractional optimum and a fortiori at most $f$ times the integral optimum.

The double-counting step

The one substantive step of the goal is split out as its own target: for a primal-dual certificate,

$$\sum_{s \in C} c_s \ \le\ f \cdot \sum_{e \in E} y_e .$$

Tightness rewrites the cover's cost as a double sum over chosen sets and their elements; exchanging the order groups it by element, each charged at most $f$ times. With this and weak duality, the goal is two lines.

The greedy bound

A greedy certificate at ratio $\rho$ is a cover $C$ and a nonnegative $y$ with $\sum_{s \in C} c_s = \sum_{e} y_e$ and $\sum_{e \in A_s} y_e \le \rho\, c_s$ for every $s$. For such a certificate and any fractional cover $x$,

$$\sum_{s \in C} c_s \ \le\ \rho \cdot \sum_{s} c_s x_s .$$

Instantiating $\rho = H_n$ is what recovers the source's greedy guarantee; the harmonic bound itself is already in Mathlib.

Set-cover weak duality and LP attainment

Every dual packing is bounded by every fractional cover, $\sum_e y_e \le \sum_s c_s x_s$; the fractional optimum is at most the integral optimum; and both optima are attained, not merely bounded below. Attainment of the fractional optimum is a genuine linear-programming fact and is the hardest supporting item in the mission.

Significance

This is where the series first converts a dual-feasibility invariant into an approximation ratio on a concrete combinatorial problem, and the two certificate predicates are reused verbatim by the online covering missions later in the series. Set cover approximation has, as far as we can determine, no prior formalization in Mathlib or in any public Lean library: there is no set-cover problem statement, no greedy analysis, and no $f$-approximation result to build on.

Difficulty

The two certificate bounds are finite-summation arguments of moderate length — the work is in a double-counting step that reindexes a sum over chosen sets into a sum over elements, weighted by frequency. Attainment of the fractional optimum is different in kind: it needs a compactness or vertex argument about the covering polytope and is the item most likely to need real work. Zero-cost sets are permitted throughout, so any later algorithm definition that divides by a cost must handle that case explicitly.

Formalization scope

Definitions cover §2.2 of the source, excluding §2.2.2 (randomized rounding), which is deferred to a separate mission because its expected-cost and failure-probability analysis is measure-theoretic and shares no infrastructure with the deterministic results.

Two theorems are not in this mission: that the greedy algorithm produces a greedy certificate, and that the primal-dual algorithm produces a primal-dual certificate. Those require defining the algorithms and proving termination and coverage, and are planned as a second wave. Until that wave lands, the source's Theorems 2.4 and 2.6 should not be described as fully formalized — what this mission establishes is the certificate-to-ratio half of each.

Selected references

• Niv Buchbinder, Designing Competitive Online Algorithms via a Primal-Dual Approach, PhD thesis, Tel Aviv University, 2008, §2.2, pp. 10–14. https://www.tau.ac.il/~nivb/download/phd-thsis.pdf
• Vijay V. Vazirani, Approximation Algorithms, Springer, 2001, Chapters 2 and 15 — the standard treatment of the greedy and primal-dual set-cover analyses.

Motivation

This is the second mission in the magic-squares formalization programme, and it takes up the case the first one deliberately left open.

Counting semi-magic squares — arrays of nonnegative integers whose rows and columns all share a common line sum, with the diagonals unconstrained — is the "honest" version of the enumeration problem. For order three the magic count $M_{3}(t)$ (mission I) is only a quasi-polynomial: it vanishes unless $3\mid t$ and equals $2e^{2}+2e+1$ on $t=3e$. The semi-magic count $H_{3}(t)$ has no such periodicity. MacMahon computed it in 1915:

$$H_{3}(t)\;=\;3\binom{t+3}{4}+\binom{t+2}{2}.$$

It is an honest polynomial in $t$ of degree $4=(3-1)^{2}$, and that degree is not an accident: Ehrhart and Stanley proved that for every order $n$ the function $H_{n}(t)$ is a polynomial of degree $(n-1)^{2}$ satisfying the reciprocity law $H_{n}(-n-t)=(-1)^{n-1}H_{n}(t)$. The order-three formula above is the smallest nontrivial instance of that theorem, and the only one small enough that every step of the derivation can still be exhibited explicitly.

So this mission is the natural companion to mission I: same objects, same platform vocabulary, but the counting step is genuinely harder — the parameter space is four-dimensional rather than two, and the parametrization is not injective until it is normalized.

Setting

Fix $n$ and a line sum $t$. A square of order $n$ is an $n\times n$ array $M$ of nonnegative integers.

• $M$ is semi-magic with line sum $t$ if every row and every column sums to $t$. No condition is imposed on the two diagonals, and entries need not be distinct.
• $H_{n}(t)$ is the number of such squares. Every entry is at most $t$, so $H_{n}(t)$ is the cardinality of a finite set.

For $n=3$ the whole family is governed by the six permutation matrices. Split them into the three even ones — the identity and the two $3$-cycles — whose supports are the transversals

$$D=\{00,11,22\},\qquad E=\{01,12,20\},\qquad F=\{02,10,21\},$$

and the three odd ones — the transpositions — with supports

$$A=\{00,12,21\},\qquad B=\{02,11,20\},\qquad C=\{01,10,22\}.$$

Adding them with multiplicities $u,v,w$ (even) and $x,y,z$ (odd) gives

$$M=\begin{pmatrix} u+x & v+z & w+y\\ w+z & u+y & v+x\\ v+y & w+x & u+z\end{pmatrix},$$

whose six line sums all equal $u+v+w+x+y+z$; so this is a semi-magic square of line sum $t$ whenever the multiplicities sum to $t$.

Formalization targets

Goal — MacMahon's semi-magic count

$$H_{3}(t)\;=\;3\binom{t+3}{4}+\binom{t+2}{2}\qquad\text{for every }t\ge 0 .$$

This is the goal because it is the weakest statement that still pins down the answer: it asserts the shape of $H_{3}$ without naming the parametrization, and it survives verbatim as the $n=3$ case of Stanley's theorem that $H_{n}$ is a polynomial of degree $(n-1)^{2}$.

The route

1. Canonical decomposition (sm3_canonical). Every $3\times3$ semi-magic square arises from the display above, and the representation becomes unique after normalizing: put $u=\min D$, $v=\min E$, $w=\min F$, subtract the corresponding even permutation matrices, and the residual odd multiplicities satisfy $\min(x,y,z)=0$. The normalization is necessary — without it the single relation

$$D+E+F=A+B+C\;(=J)$$

identifies distinct $6$-tuples — and it is exactly what makes the count a partition rather than an inclusion–exclusion. 2. Bijection (sm3_bij). The map from normalized coefficient vectors to semi-magic squares is a bijection, so $H_{3}(t)=\mathrm{sm3Count}(t)$. 3. Stars and bars (comps_card). The number of $k$-tuples of nonnegative integers summing to $n$ is $\binom{n+k-1}{n}$; the case $k=5$ is what the count needs. 4. Evaluating the parameter count (sm3_params_card). Partitioning the normalized vectors according to the first zero among $(x,y,z)$ writes $\mathrm{sm3Count}(t)$ as

$$\binom{t+4}{4}+\binom{t+3}{4}+\binom{t+2}{4},$$

which collapses to $3\binom{t+3}{4}+\binom{t+2}{2}$ by two applications of Pascal's identity.

Significance

The result itself. $H_{3}$ is the $n=3$ case of a theorem that launched a subject: Stanley's proof that $H_{n}(t)$ counts lattice points in the Birkhoff polytope $t\cdot B_{n}$ makes $H_{n}$ an Ehrhart polynomial, and the order-three formula is the first nontrivial value of it. Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717) revisited exactly this computation on the way to their quasi-polynomial theorem for the magic counts, and Beck and Zaslavsky later pushed the same technique to the panmagic and symmetric refinements. Getting $H_{3}$ machine-checked therefore validates the whole hierarchy at its base.

Formalizing it. Nothing here is open; the mathematics is a century old. What is missing is the formalized artifact, and the difficulty is concentrated in two places that are formalization difficulties rather than mathematical ones.

First, surjectivity of the permutation-matrix parametrization. The usual proof quotes Birkhoff–von Neumann, which in turn needs Hall's marriage theorem. For order three one can instead do it by hand: subtract the three even transversal minima and show that the residual satisfies $M_{01}=M_{10}$. That last step is a six-case argument in linear arithmetic — if $b=M_{01}>c=M_{10}$ then each of the three ways for the transversal $E$ to have minimum zero forces $c\ge b$ — and it is precisely the kind of step that is invisible on paper and must be made explicit in a proof assistant.

Second, the counting step. The parameter set is a filtered finset of functions Fin 6 → Fin (t+1), while the formula is stated with binomial coefficients over $\mathbb{N}$. Connecting them requires stars-and-bars, proved from scratch (by induction on the number of parts plus the hockey-stick identity), because the available library results count sub-multisets rather than compositions. And the final collapse to MacMahon's form is a chain of Pascal identities that must be applied in the right order to stay inside $\mathbb{N}$, where subtraction is truncated.

Difficulty

Two traps deserve to be named.

Uniqueness needs the normalization. The representation by six multiplicities is not injective: $J=D+E+F=A+B+C$. Any formalization that counts $6$-tuples directly will overcount, and the correction is not a subtraction but a choice of canonical representative. Deciding "first zero among $(x,y,z)$" is what turns the count into a genuine partition.

Truncated subtraction. The decomposition is expressed over $\mathbb{N}$, so every identity — in particular the recovery of the multiplicities from a square — must be stated with the admissibility inequalities as explicit hypotheses. A truncated subtraction is only correct because normalization forbids the truncation, and that side condition has to be discharged rather than assumed.

Formalization scope

• Squares are indexed by Fin n; semiMagicCount n t is the cardinality of a finset of arrays over Fin (t+1) — lossless, since every entry is at most $t$.
• The parametrization and its normalization are defined over $\mathbb{N}$ with truncated subtraction where necessary.
• Trivializing formalizations are ruled out. The goal is not a statement about a hardcoded small $t$, nor about a finset declared to have the right cardinality: the count must be derived, by an explicit bijection followed by an explicit evaluation of a finite sum.
• Reusable beyond this mission: the canonical decomposition of $3\times3$ semi-magic squares (equivalently, the toric description of the order-three Birkhoff polytope with its single relation), the stars-and-bars lemma for compositions into any number of parts, and the order-three counts themselves.

Selected references

• P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916 (the $H_3$ formula dates to his 1915 work).
• M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717. https://arxiv.org/abs/math/0201013
• M. Beck and T. Zaslavsky, Six little squares and how their numbers grow, J. Combin. Theory Ser. A 113 (2006). https://arxiv.org/abs/math/0502370
• R. P. Stanley, Enumerative Combinatorics, Vol. I, 2nd ed., Cambridge University Press, 2012 (Ehrhart theory and reciprocity for $H_n$).

Motivation

Counting magic squares — arrays of nonnegative integers whose rows, columns and two main diagonals all share a common line sum — is one of the oldest problems in enumerative combinatorics, and the testing ground on which the general theory was built. MacMahon computed the order-three count in 1915 by hand; sixty years later Stanley, and then Beck, Cohen, Cuomo and Gribelyuk (Amer. Math. Monthly 110 (2003), 707--717), showed that for general order $n$ the counting functions are quasi-polynomials in the line sum, by identifying them with Ehrhart quasi-polynomials of rational polytopes. The order-three case is the oldest nontrivial instance of that theory and the one where every step can still be checked by hand.

The subject therefore has a curious status: the enumerative answer for $n=3$ has been known for over a century, and the structural facts behind it (a $3\times3$ magic square is determined by two corner entries; opposite cells sum to twice the centre) are folklore — but none of it has a machine-checked proof. This mission formalizes the classical derivation end to end.

Setting

Fix an order $n$ and a type $\alpha$ of entries. A square of order $n$ is an $n\times n$ array $M$ with entries in $\alpha$; its row sums, column sums, and the two diagonal sums (main and anti-diagonal) are the sums of the entries along those lines.

• $M$ is semi-magic with line sum $s$ if every row and every column sums to $s$.
• $M$ is magic with line sum $s$ if in addition both main diagonals sum to $s$.
• $M$ is panmagic (pandiagonal) if every broken diagonal, in both directions, also sums to $s$.

No distinctness of entries is required. Let $H_n(t)$ denote the number of semi-magic and $M_n(t)$ the number of magic squares of order $n$ with nonnegative integer entries and line sum $t$. Every entry of such a square is at most $t$, so these are finite counts.

For $n=3$ the whole family is parametrized. If $M$ has line sum $3e$ then the centre cell equals $e$, and writing $a=M_{00}$ and $c=M_{02}$ the eight line identities force

$$M=\begin{pmatrix} a & 3e-a-c & c\\ e+c-a & e & e+a-c\\ 2e-c & a+c-e & 2e-a \end{pmatrix}.$$

All nine entries are nonnegative exactly when

$$e\le a+c\le 3e,\qquad a\le e+c,\qquad c\le e+a,$$

and substituting $p=a-e$, $q=c-e$ turns these into $|p|+|q|\le e$: the $\ell_1$ ball of radius $e$ in $\mathbb{Z}^2$.

Formalization targets

Goal — MacMahon's count

$$M_{3}(3e)\;=\;2e^{2}+2e+1 ,$$

together with the companion vanishing $M_3(t)=0$ when $3\nmid t$. This is the count of $3\times3$ magic squares of line sum $3e$ with nonnegative integer entries (entries need not be distinct). It is the goal because it is the weakest stable statement: it asserts only the shape of the answer, not the intermediate parametrization, and it survives verbatim as the $n=3$ case of the general quasi-polynomial theorem.

Stronger — the parametrization itself

That the map $M\mapsto(M_{00},M_{02})$ is a bijection from the $3\times3$ magic squares of line sum $3e$ onto the admissible parameter pairs, and that the latter are counted by the $\ell_1$-ball cardinality. This is the route the mission actually takes; the count is its corollary.

Further — semi-magic counts

$H_3(t)$, the analogous count for semi-magic squares, is a genuinely different and harder quasi-polynomial. It is listed as a stretch target, not a milestone.

Significance

The result itself. MacMahon's formula is the base case of the Ehrhart-theory reading of magic-square enumeration; Beck--Cohen--Cuomo--Gribelyuk's quasi-polynomial theorem for general $n$ degenerates to it at $n=3$, so it is the sanity check any generalization must pass. The parametrization behind it is what makes the "how many" question finite-dimensional at all: it reduces a search over $t^9$ arrays to a count of lattice points in a two-dimensional ball. Downstream, the same parametrization governs the classification of normal $3\times3$ magic squares (the Lo Shu square and its symmetries) and the associativity identity $M_{ij}+M_{2-i,2-j}=2M_{11}$.

Formalizing it. The mathematics is classical and proved; nothing here is open. What is missing is the formalized artifact. The order-three structural lemmas — the centre identity, the opposite-cell identity, and the two directions of the parametrization — are already machine-checked on this platform. The remaining work is the counting step: exhibiting a concrete bijection between two finsets whose elements live in different types (arrays over Fin (3e+1) versus pairs of naturals) and evaluating a finite sum. That is where the formalization, not the mathematics, is hard.

Difficulty

The obvious attack — "each magic square is determined by $(a,c)$, so just count the pairs" — fails at exactly one point, and it is not a mathematical point. The counting function $M_3$ is defined as the cardinality of a finset of arrays with entries in Fin (3e+1) (a finite type, so that Finset.univ exists), whereas the parametrization lives over $\mathbb{N}$. Proving the counts agree therefore requires a honest Finset.card_bij in both directions:

• forward, extract $(M_{00},M_{02})$ from an array and show the pair is admissible;
• backward, build mkMagic3 from an admissible pair, coerce every entry into Fin (3e+1) using the bound $M_{ij}\le 2e\le 3e$, and show the round trip is the identity.

Neither direction is deep, but the coercions are unforgiving: a truncated subtraction in mkMagic3 is only correct because admissibility forbids the truncation, and that side condition must be discharged explicitly rather than assumed. The second difficulty is the cardinality of the $\ell_1$ ball: the identification $|p+q|\le e\ \wedge\ |p-q|\le e\ \Longleftrightarrow\ |p|+|q|\le e$ needs the elementary identity $\max(|p+q|,|p-q|)=|p|+|q|$, after which the count is $1+4\sum_{k=1}^e k = 2e^2+2e+1$.

Formalization scope

• Entries are indexed by Fin n; the anti-diagonal uses Fin.rev, and broken diagonals use addition modulo $n$. Counting functions are cardinalities of finsets of arrays over Fin (t+1) — lossless, since every entry is at most $t$ — and return natural numbers.
• mkMagic3 is defined over $\mathbb{N}$ with truncated subtraction. Every row/column/diagonal identity therefore carries the admissibility inequalities as explicit hypotheses; no identity is asserted unconditionally.
• Trivializing formalizations are ruled out: the goal is not a statement about a hardcoded small $e$, nor about a finset declared to have the right cardinality. The count must be derived.
• Reusable beyond this mission: the core vocabulary (Square, IsSemiMagic, IsMagic, IsPanMagic, IsAssociative, IsNormal, magicConstant, and the four counting functions $H_n,M_n,P_n,S_n$), the symmetry/affine toolbox, and the order-three structural lemmas. Contributions are welcome on the semi-magic count $H_3$, on panmagic and associative refinements, and on the extension to general $n$.

Selected references

• P. A. MacMahon, Combinatory Analysis, Vol. II, Cambridge University Press, 1916 (the $M_3$ formula dates to his 1915 work).
• M. Beck, T. Cohen, J. Cuomo and P. Gribelyuk, The number of "magic" squares, cubes and hypercubes, Amer. Math. Monthly 110 (2003), 707--717. https://arxiv.org/abs/math/0201013
• M. Beck and T. Zaslavsky, Six little squares and how their numbers grow, J. Combin. Theory Ser. A 113 (2006). https://arxiv.org/abs/math/0502370
• G. Xin, Constructing all magic squares of order three, Discrete Math. 308 (2008). https://arxiv.org/abs/math/0610771

Motivation

A coset partition of a group $G$ is a finite family of left cosets $a_1G_1, \dots, a_kG_k$ that are pairwise disjoint and cover $G$. In 1974 Herzog and Schönheim asked whether the indices $n_i = [G : G_i]$ of such a partition, with $k > 1$, can be pairwise distinct. They cannot when $G = \mathbb{Z}$ — there a coset partition is an exact covering system of the integers, and Davenport–Rado and Mirsky–Newman showed the largest modulus must repeat — but for general groups the question is still open, even for finite solvable groups.

Progress has come in two styles. Structural: Berger, Felzenbaum and Fraenkel settled finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333 and finite pyramidal groups in Fund. Math. 128 (1987) 139–144. Order-bounded: Ginosar and Schnabel (2011) settled every $G$ whose order has at most two prime divisors, and Margolis and Schnabel (2019) verified all $|G| < 1440$.

The paper formalized here, Z.-W. Sun, J. Algebra 273 (2004) 153–175, takes a third route: it constrains the subgroups rather than the group, and simultaneously weakens "partition" to "uniform cover". Its hypothesis — that the $G_i$ be subnormal — costs nothing in the nilpotent case (every subgroup of a nilpotent group is subnormal) yet applies to arbitrary, possibly infinite, ambient groups $G$. It also answers negatively an open question of the same paper, generalizing one of Erdős: the indices of such a cover cannot all be large if each occurs only boundedly often.

Setting

Let $G$ be a group, written multiplicatively. For a finite system

$$\mathcal{A} = \{a_iG_i\}_{i=1}^{k}$$

of left cosets, the covering function counts memberships,

$$w_{\mathcal{A}}(x) \;=\; \bigl|\{\, 1 \le i \le k \;:\; x \in a_iG_i \,\}\bigr| .$$

If $w_{\mathcal{A}}$ is constant, say $w_{\mathcal{A}} \equiv w$, then $\mathcal{A}$ is a uniform cover of $G$ of weight $w$; the case $w = 1$ is exactly a coset partition. A uniform cover is trivial when $G_i = G$ for every $i$, and this is the only degenerate case that must be excluded. Uniform covers are genuinely more general than partitions: one may have no disjoint subcover at all.

A subgroup $H \le G$ is subnormal if some finite chain $H = H_0 \trianglelefteq H_1 \trianglelefteq \cdots \trianglelefteq H_n = G$ reaches $G$, each term normal in the next. Normal subgroups are subnormal; in a nilpotent group every subgroup is; and $\operatorname{Sym}(4)$ shows a subgroup of a solvable group need not be.

Write $n_i = [G : G_i]$ for the indices, always assumed finite, and

$$N \;=\; [\,n_1, \dots, n_k\,]$$

for their least common multiple, whose prime divisors are exactly those of $n_1\cdots n_k$. Let $p_*$ and $p^*$ denote the least and greatest prime divisors of $N$, let $\varphi$ be Euler's totient, and let

$$M \;=\; \max_{1 \le j \le k} \bigl|\{\, 1 \le i \le k : n_i = n_j \,\}\bigr|$$

be the largest multiplicity with which an index is repeated. The Herzog–Schönheim conjecture says $M \ge 2$.

Target

The goal theorem is Theorem 4.3(i) of the source: for a nontrivial uniform cover of any group by cosets of subnormal subgroups of finite index, some index divisible by the largest prime $p^*$ is repeated at least $p_*$ times,

$$\exists\, j, \qquad p^* \mid n_j \quad\text{and}\quad \bigl|\{\, i : n_i = n_j \,\}\bigr| \;\ge\; p_* .$$

In particular $M \ge p_*$. Two weaker consequences are separate targets. Since $p_* \ge 2$, this gives the Herzog–Schönheim conjecture for subnormal uniform covers,

$$\exists\, i \ne j, \qquad [G : G_i] = [G : G_j],$$

and the quantitative step behind it is a Burshtein-type inequality, which after clearing denominators reads

$$p^{*}\prod_{p \mid N}(p-1) \;<\; \bigl|\{\, i : n_i = n_j \,\}\bigr| \prod_{p \mid N} p \qquad\text{for some } j \text{ with } p^* \mid n_j .$$

Significance

The result itself. It is the widest structural class in which Herzog–Schönheim is known, and the only one that does not require $G$ to be finite: subnormality of the $G_i$ is a condition on the subgroups, so $G$ itself is arbitrary. It strictly contains the nilpotent case of Berger–Felzenbaum–Fraenkel, and being quantitative it also yields the Burshtein conjecture in this setting — a bound no purely qualitative statement gives. Because the conclusion is a lower bound on $M$ growing with $p_*$, it answers the paper's open question: one cannot make all the indices of a uniform cover large while keeping every multiplicity bounded.

Formalizing it. Nothing here is open, and the mission is the machine-checked version of a known proof. What it adds is a formal vocabulary for uniform covers — Mathlib has Mathlib/GroupTheory/CosetCover.lean (B. H. Neumann's theorems, $\sum_i 1/[G:H_i] \ge 1$) but no notion of covering multiplicity — and the arithmetic of subnormality, in particular that $[G : \bigcap_i G_i]$ divides $\prod_i [G : G_i]$ when the $G_i$ are subnormal. Mathlib has Subgroup.IsSubnormal with the basic closure properties but nothing about indices of subnormal subgroups, and that divisibility is the whole reason subnormal covers behave. The totient measure this proof runs on is already formalized: Sun's Lemma 3.1 is Berger–Felzenbaum–Fraenkel's equation (14), already proved on the platform as BFFPyramidal.muMeasure_divisorClosure_image_mul, and this mission reuses that definition file rather than duplicating it.

Status disclosure. Complete Lean proofs of the goal and of every milestone below already exist and will be submitted at launch, so this mission is not an open frontier: its value is the verified artifact, the reusable vocabulary, and the fact that the development turned up two places where the published argument needs repair or can be simplified (see Formalization scope). Alternative proofs, sharper variants, and the analytic parts excluded below remain genuinely open contributions.

Difficulty

The reciprocal identity is the first thing anyone writes down and it is not enough: a uniform cover of weight $w$ satisfies $\sum_i 1/n_i = w$, and pairwise distinct $n_i$ can do that.

The real obstruction is that a cover does not descend to a quotient. A part $a_iG_i$ need not lie in one coset of a chosen normal subgroup, so the induction that proves the finite nilpotent case has nothing to induct along once $G$ may be infinite and the $G_i$ are merely subnormal. Sun's replacement is a lower bound for the size of a union of cosets, Theorem 3.1: if $H \le G_i$ for all $i$ and $[G:H] < \infty$, then the number of cosets of $H$ inside $\bigcup_i a_iG_i$ is at least the number of $n < [G:H]$ divisible by some $n_i$. The union is compared not with the $G_i$ but with a purely numerical shadow of itself in $\{0, 1, \dots, [G:H]-1\}$, and it is here that subnormality enters, through the divisibility $[G : \bigcap G_i] \mid \prod [G : G_i]$ (Lemma 2.1) — for arbitrary finite-index subgroups Poincaré gives only the inequality $[G : \bigcap G_i] \le \prod [G:G_i]$, which is too weak.

The second difficulty is arithmetic and is where the source spends its effort. Turning Theorem 3.1 into a bound on multiplicities (Theorem 3.2) requires computing the density of a union $\bigcup_i n_i\mathbb{Z}$, and the identity the paper uses (Lemma 3.4) expresses that density as $\prod_{p \in P}\frac{p-1}{p}$ times an infinite sum of reciprocals over $P$-smooth elements of the union. Along that route the full series is needed: truncating it loses precisely the geometric factors $\bigl(1 - p^{-(1+\delta_p)}\bigr)^{-1}$ that produce the divisor sum $\sum_{d \mid N/g} 1/d$ in the conclusion.

It is worth saying, though, that this analytic detour is avoidable — a solver need not take it. Theorem 3.2 can also be reached by a purely finite argument: bound the density from below by injecting each index $s$ into the divisor $\operatorname{lcm}\{s' : s' \mid x\}/s$, which is sharp in the same cases as the series argument. Lemma 3.4 remains a faithful and separately interesting milestone of the paper, but it is not on the critical path to the goal. The naive version of the finite estimate — bounding the density below by $1/\min_i n_i$ — is genuinely false, as $\{4,6,9,12,18,36\}$ shows, so the injection is the content, not a one-liner.

Formalization scope

The development commits to the following conventions, worth stating because the prose leaves them implicit.

Covers are indexed families rather than sets of cosets: IsUniformCover K a w asserts that for every $x$ the number of indices $i$ with $(a_i)^{-1}x \in K_i$ is exactly w, counted as Nat.card of a subtype so that no decidability hypothesis is needed. Indexing by Fin k keeps multiplicities visible, which matters because every conclusion counts indices, not distinct subgroups. Nontriviality is never folded into the definition; it appears as the explicit hypothesis ∃ i, K i ≠ ⊤, and without it every statement here is false (take $k=1$, $G_1 = G$).

$G$ is an arbitrary group — not assumed finite. Finiteness enters only through Subgroup.FiniteIndex on each $K_i$, which the source assumes implicitly when it writes "the (finite) indices". Indices are Subgroup.index and $[G_i : H]$ is H.relIndex (K i). For a subgroup $H$ that is not assumed normal, G ⧸ H is still the type of left cosets and Nat.card (G ⧸ H) = H.index; Theorem 3.1 is stated with that type, since the $H$ it is applied to is not normal.

Densities are never limits. The density of a union $\bigcup_i n_i\mathbb{Z}$ is taken as the finite ratio $|\{x < N : \exists i,\ n_i \mid x\}| / N$ for an explicit common multiple $N$, which is exactly equal to the asymptotic density and keeps Lemma 3.4 free of any analysis on the left-hand side; the right-hand side genuinely is an infinite sum and is stated with HasSum over $\mathbb{R}$.

Inequalities are cleared of denominators and stated in $\mathbb{N}$ wherever possible, so that $\sum_{d \mid m} 1/d \le c$ appears as $\sum_{d \in m.divisors} d \le c \cdot m$. Readers should check the direction: $\mathbb{N}$ subtraction truncates, so $\prod_{p \mid N}(p-1)$ is only the intended quantity because every $p$ here is prime, hence $\ge 2$.

⚠️ Parts (ii)–(iv) of the source's Theorem 4.3 are out of scope. Those bound the primes dividing the indices, their number, and $\log n_1$ by $e^{\gamma}M\log^2 M + O(M \log M \log\log M)$ and similar, and they rest on Mertens' third theorem, $\prod_{p \le x}(1 - 1/p) \sim e^{-\gamma}/\log x$, which Mathlib does not have. It is worth being precise about what Mathlib does have, since the gap is narrower than it looks: the prime counting function Nat.primeCounting, Chebyshev's $\theta$ and $\psi$ with the machinery around them (Mathlib/NumberTheory/Chebyshev.lean), Euler products (Mathlib/NumberTheory/EulerProduct/), and the constant $\gamma$ itself (Real.eulerMascheroniConstant) are all present — what is missing is Mertens' asymptotic tying them together, and the $\pi(x)$ asymptotics. Supplying that is a substantial number-theory project in its own right, so this mission stops at the arithmetic core, part (i), which is what implies Herzog–Schönheim. Contributions adding the analytic parts are welcome and would complete Theorem 4.3.

Two things the development established that the paper does not state. First, Lemma 2.1 is true in a stronger form: $[G : A \cap B] \mid [G:A]\,[G:B]$ needs only $A$ subnormal, not both, and needs no finiteness hypothesis at all (with Mathlib's convention that an infinite index is $0$). Second, Theorem 4.1's passage from the largest prime $p^*$ to the smallest $p_*$ can be isolated as a self-contained arithmetic inequality, $(p_*-1)\prod_{p\mid N}p \le p^*\prod_{p\mid N}(p-1)$, which is tight at prime powers; it is listed as its own milestone for that reason.

Reusable beyond this mission: the uniform-cover vocabulary, the subnormal index divisibility of Lemma 2.1, and Theorem 3.1's union bound, which applies to any attack on Herzog–Schönheim including the still-open solvable case. The source also leaves Conjecture 4.1 open — that for a nontrivial uniform cover by subnormal subgroups the largest index $n$ is repeated at least $p(n)$ times, $p(n)$ its least prime factor — which would be a natural follow-on target.

Selected references

• Z.-W. Sun, On the Herzog–Schönheim conjecture for uniform covers of groups, Journal of Algebra 273 (2004) 153–175. DOI
• M. Herzog, J. Schönheim, Research problem No. 9, Canadian Mathematical Bulletin 17 (1974) 150.
• M. A. Berger, A. Felzenbaum, A. S. Fraenkel, The Herzog–Schönheim conjecture for finite nilpotent groups, Canadian Mathematical Bulletin 29 (1986) 329–333. DOI
• M. A. Berger, A. Felzenbaum, A. S. Fraenkel, Remark on the multiplicity of a partition of a group into cosets, Fundamenta Mathematicae 128 (1987) 139–144. DOI
• N. Burshtein, On natural exactly covering systems of congruences having moduli occurring at most M times, Discrete Mathematics 14 (1976) 205–214. DOI
• R. J. Simpson, Exact coverings of the integers by arithmetic progressions, Discrete Mathematics 59 (1986) 181–190. DOI
• Z.-W. Sun, Exact m-covers of groups by cosets, European Journal of Combinatorics 22 (2001) 415–429. DOI
• B. H. Neumann, Groups covered by finitely many cosets, Publicationes Mathematicae Debrecen 3 (1954) 227–242.
• L. Margolis, O. Schnabel, The Herzog–Schönheim conjecture for small groups and harmonic subgroups, Beiträge zur Algebra und Geometrie 60 (2019) 399–418. arXiv

Motivation

A coset partition of a group $G$ is a finite family of left cosets $a_1K_1, \dots, a_tK_t$ of subgroups $K_i \le G$ that are pairwise disjoint and cover $G$. Asking which multisets of indices $[G:K_i]$ can occur is a question with two independent origins. For $G = \mathbb{Z}$ the cosets are arithmetic progressions and a coset partition is an exact covering system of the integers; Erdős asked whether the moduli of such a system can be pairwise distinct, and Davenport and Rado, and independently Mirsky and Newman, showed they cannot — the largest modulus must repeat. For general groups, Herzog and Schönheim (1974) asked the same question: in any coset partition with $t > 1$, must two of the indices coincide? That question is still open.

Progress has come by restricting the group. Berger, Felzenbaum and Fraenkel proved the conjecture for finite nilpotent groups in Canad. Math. Bull. 29 (1986) 329–333, and the paper formalized here extends it to a wider class defined by a chain condition. Later work bounds the order instead of the structure: Ginosar and Schnabel (2011) settle every $G$ whose order has at most two prime divisors, and three prime divisors when $6 \nmid |G|$, while Margolis and Schnabel (2019) verify all $|G| < 1440$. The conjecture remains open even for finite solvable groups.

Setting

Let $p(m)$ denote the least prime factor of $m$ and $P(m)$ the greatest, and let $\varphi$ be Euler's totient function.

A finite group $G$ is pyramidal if it admits a chain of subgroups

$$\{1\} = G_n \subseteq G_{n-1} \subseteq \cdots \subseteq G_1 \subseteq G_0 = G$$

in which every step has index equal to the least prime factor of the order of the preceding term:

$$[G_{k-1} : G_k] = p\!\left(|G_{k-1}|\right), \qquad 1 \le k \le n.$$

A subgroup whose index is the smallest prime dividing the order is automatically normal, so the chain is a composition series; consequently every pyramidal group is solvable, and every supersolvable group is pyramidal. Pyramidality is therefore a chain condition sitting between supersolvability and solvability.

Given a coset partition $a_1K_1, \dots, a_tK_t$ of $G$, write

$$l \;=\; \frac{|G|}{\gcd\!\left(|K_1|, \dots, |K_t|\right)} .$$

Target

The goal theorem is the multiplicity lower bound of Berger–Felzenbaum–Fraenkel. If $G$ is pyramidal and the cosets $a_iK_i$, $1 \le i \le t$, partition $G$ with $t > 1$, then at least

$$x \;=\; \left\lfloor \frac{P(l)\,\varphi(l)}{l} \right\rfloor + 1$$

of the subgroups $K_i$ have the same order.

Two consequences are separate targets. Since $x \ge 2$ whenever $l \ge 2$, the bound yields the Herzog–Schönheim conjecture for pyramidal groups:

$$\exists\, i \ne j, \qquad [G : K_i] = [G : K_j],$$

and it likewise settles Burshtein's conjecture in this setting, which concerns the case $\gcd(|K_i|) = 1$ and bounds the primes dividing $|G|$ in terms of the largest multiplicity.

Significance

The bound is quantitative where the Herzog–Schönheim conjecture is qualitative: it does not merely assert that a repetition exists but forces a repetition of prescribed multiplicity, growing with the largest prime factor of $l$. That is what makes it strong enough to also imply Burshtein's conjecture, which no purely qualitative statement does.

The class it covers is also of independent interest. Nilpotent groups are pyramidal, so the result subsumes the authors' earlier theorem, and it reaches groups that are solvable but far from nilpotent. It remains, more than three decades later, among the structural (as opposed to order-bounded) cases in which the conjecture is known.

No part of this development is currently formalized: Mathlib has the ingredients — Sylow theory, Hall subgroups of solvable groups, Euler's totient with Gauss's identity $\sum_{d \mid m}\varphi(d) = m$ — but neither coset partitions as a structure, nor pyramidality, nor any case of Herzog–Schönheim. The mission produces the first machine-checked proof of a structural case of the conjecture, together with a reusable formal vocabulary for coset partitions.

Difficulty

The reciprocal identity $\sum_i [G:K_i]^{-1} = 1$ is immediate and useless on its own: distinct indices can satisfy it, so no counting argument over the indices alone can succeed.

The natural attack — induct along the chain, quotienting by $G_1$ — fails because a coset partition does not descend to a quotient. A part $a_iK_i$ need not lie inside a single coset of $G_1$: if $K_iG_1 = G$ then it meets every coset of $G_1$, and the induced family on $G/G_1$ is a cover with multiplicity rather than a partition. Controlling that dichotomy is the first obstacle, and it is precisely where the definition of pyramidality is used, the index $[G:G_1]$ being the least prime factor of $|G|$ rather than an arbitrary one.

The second obstacle is that the conclusion counts subgroups of equal order, so the induction must carry a lower bound on the size of a union of cosets that is sensitive to the orders $|K_i|$ and not merely to their number. The paper's device is a measure $\mu$ on the naturals with $\mu(\{m\}) = \varphi(m)$, evaluated on the divisor closure of the set of orders; Gauss's identity makes $\mu$ interact correctly with divisibility, and the required inequality is genuinely a statement about the group, not about the multiset of orders. The final step splits off the Sylow $P(|G|)$-subgroup against a Hall complement, which exists only because pyramidal groups are solvable.

Formalization scope

The development commits to the following conventions, all fixed in Lean and worth stating because the prose leaves them implicit.

Coset partitions are indexed families rather than sets of cosets: IsCosetPartition K a asserts that for every $x$ there is a unique index $i$ with $(a_i)^{-1}x \in K_i$. Indexing by Fin t keeps multiplicities visible, which matters since the conclusion counts indices, not distinct subgroups; and uniqueness encodes disjointness and covering simultaneously. Groups are finite via [Finite G], and orders and indices are Nat.card and Subgroup.index.

Pyramidality is stated as the existence of a length $n$ and a chain c : ℕ → Subgroup G with c 0 = ⊤, c n = ⊥, and Subgroup.relIndex (c (k+1)) (c k) = Nat.minFac (Nat.card (c k)) for k < n. Normality of each step is a consequence, not a hypothesis, and is deliberately not assumed. The greatest prime factor is maxPrimeFac m = m.primeFactors.sup id, which is $0$ for $m \in \{0,1\}$; the floor in $x$ is natural-number division, so the goal statement is (maxPrimeFac l * Nat.totient l) / l + 1 ≤ …. Note that the bound is vacuous at $l = 1$ — there $P(1)\varphi(1)/1 = 0$ and $x = 1$ — so $t > 1$ is a necessary hypothesis and is present in every statement that needs it; a formalization omitting it would be trivially true and is ruled out.

A complete development needs, beyond the goal: the coset intersection lemma; the least-prime-index dichotomy; uniqueness of the Sylow $P(|G|)$-subgroup of a pyramidal group; the scaling law $\mu(D(kR)) = k\,\mu(D(R))$ for the divisor-closure measure; the union lower bound; and solvability of pyramidal groups. The coset-partition vocabulary and the union bound are reusable for any other case of Herzog–Schönheim, including the still-open solvable case, and contributions of alternative proofs or sharper variants are welcome.

Selected references

• M. A. Berger, A. Felzenbaum, A. S. Fraenkel, Remark on the multiplicity of a partition of a group into cosets, Fundamenta Mathematicae 128 (1987) 139–144. DOI
• M. A. Berger, A. Felzenbaum, A. S. Fraenkel, The Herzog–Schönheim conjecture for finite nilpotent groups, Canadian Mathematical Bulletin 29 (1986) 329–333. DOI
• M. Herzog, J. Schönheim, Research problem No. 9, Canadian Mathematical Bulletin 17 (1974) 150.
• N. Burshtein, On natural exactly covering systems of congruences having moduli occurring at most M times, Discrete Mathematics 14 (1976) 205–214. DOI
• I. Korec, Š. Znám, On disjoint covering of groups by their cosets, Mathematica Slovaca 27 (1977) 3–7.
• Z.-W. Sun, On the Herzog–Schönheim conjecture for uniform covers of groups, Journal of Algebra 273 (2004) 153–175. DOI
• L. Margolis, O. Schnabel, The Herzog–Schönheim conjecture for small groups and harmonic subgroups, Beiträge zur Algebra und Geometrie 60 (2019) 399–418. arXiv

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.

$$\exists\, C\in\mathbb R,\ \forall n\ge 1,\ \forall A\in\{0,1\}^{n\times n},\ \exists\,\varepsilon\in\{-1,1\}^n,\ \forall i,\ \Bigl|\sum_{j=1}^n A_{ij}\varepsilon_j\Bigr|\le C\sqrt n.$$

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

$$\mathrm{ex}(n, H) = O\!\left(n^{2-1/r}\right).$$

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

$$\mathrm{ex}(n, H) \ \ge\ c\,n^{3/2 + \varepsilon}$$

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

$$A(\tau) = \kappa + \tau\log_2 3, \qquad C(\tau) = 2h(\tau) - 1,$$

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

$$\mathrm{ex}(n,\mathcal{F}) = O\!\left(n^{4/3-1/48}\right) \qquad\text{while}\qquad \mathrm{ex}(n,F) = \Omega\!\left(n^{4/3}\right) \ \ (F \in \mathcal{F}).$$

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.