Motivation

A set of integers is sumfree when no two of its elements, equal or distinct, add up to an element of the set. The Schur number $S(n)$ is the largest $N$ such that $\{1, \dots, N\}$ can be partitioned into $n$ sumfree sets; only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known. For $n \ge 4$ the best theoretical upper bound that Eliahou and Revuelta could cite in 2021 was $S(n) \le R_n(3) - 2$, where the Ramsey number $R_n(3)$ is the least $N$ such that every $n$-colouring of the edges of the complete graph $K_N$ has a monochromatic triangle. The Ramsey numbers satisfy $R_n(3) \le n\,(R_{n-1}(3) - 1) + 2$ for $n \ge 2$ (Greenwood–Gleason 1955); for $S(n)$ the paper knows no recursive upper bound.

Eliahou and Revuelta proposed a conjectural one. They defined a number $L(n)$ through the Schur degree of block-sum sets, proved $S(n) \le n\,L(n)$ (Theorem 5.4) and $S(n-1) + 1 \le L(n) \le R_{n-1}(3) - 1$ (Proposition 5.3), and conjectured $L(n) = S(n-1) + 1$ (Conjecture 5.6). This would give $S(n) \le n\,(S(n-1) + 1)$ (Conjecture 5.7) and $S(6) \le 966$ (Conjecture 5.8), against the range $536 \le S(6) \le 1836$ that they give. For $n = 4$ they proved $14 \le L(4) \le 16$, conjectured $L(4) = 14$, and left the value open.

Timeline.

• 1955: Greenwood and Gleason prove $R_3(3) = 17$ and the recursive bound above.
• 1961: Baumert computes $S(4) = 44$ (cited by Eliahou–Revuelta as reference [2]).
• 2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
• 2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, rev. 18).
• 2018: Heule proves $S(5) = 160$ with a certified SAT computation (arXiv:1711.08076).
• 2020–2021: Eliahou and Revuelta, preprint arXiv:2006.01502 and refereed version, with the same numbering of the items used here.
• 2026: McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49 (Zenodo, doi:10.5281/zenodo.22987189), proves $L(4) = 16$ and $L(5) \ge 49$; its Lean library ClassicalSchur formalizes both, with $L(5) \le 65$.

Setting

All numbers are natural numbers, except in the group $G$ below.

Sumfree sets. A set $S$ is sumfree when the sum of two of its elements, equal or distinct, is never in $S$. A set $X$ is covered by $n$ sumfree sets when it lies in the union of $n$ sumfree sets.

Schur degree. The Schur degree $\operatorname{sdeg}(X)$ is the least $n \ge 1$ such that $n$ sumfree sets cover $X$. If there is no such $n$, it is $\infty$.

For example, $\operatorname{sdeg}(\{1, \dots, N\}) \le n$ holds for $N \le S(n)$ and fails for $N > S(n)$.

Block sums. Let $A = (a_1, \dots, a_L)$ be a finite sequence of length $|A| = L$. Its block sums are the sums of runs of consecutive entries:

$$a_i + a_{i+1} + \dots + a_j \qquad (1 \le i \le j \le L).$$

The set of these sums is $\hat A$. The average of $A$ is the rational number $\mu(A) = (a_1 + \dots + a_L)/L$.

The number $L(n)$. A length $L$ has the ER property for $n$ when every sequence $A$ of $L$ positive integers with $\mu(A) \le n$ has $\operatorname{sdeg}(\hat A) \ge n$.

For $n \ge 2$, the inequality $\operatorname{sdeg}(\hat A) \ge n$ holds when no $n - 1$ sumfree sets cover $\hat A$. It fails when some $n - 1$ sumfree sets cover $\hat A$.

The number $L(n)$ is the least $L \ge 1$ with the ER property for $n$.

The pigeonhole bound. Let $\rho(0) = 2$ and $\rho(k+1) = (k+1)(\rho(k) - 1) + 2$. The first values are $\rho(1) = 3$, $\rho(2) = 6$, $\rho(3) = 17$ and $\rho(4) = 66$.

For $k \ge 1$, $\rho(k)$ is an upper bound for the Ramsey number: $R_k(3) \le \rho(k)$, with equality for $k \le 3$.

The group $G$. Let $G = \mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$. A set $C \subseteq G$ is sumfree in $G$ when the sum in $G$ of two of its elements, equal or distinct, is never in $C$.

The lifted sequence. Take $m_1 \ge 1$ and $M \ge m_1$. Write the $m_1 m_2$ numbers $u + Mj$, with $0 \le u < m_1$ and $0 \le j < m_2$, in increasing order:

$$x_0 < x_1 < \dots < x_{m_1 m_2 - 1}.$$

The lifted sequence is the sequence of the $m_1 m_2 - 1$ gaps between consecutive terms, $x_1 - x_0, \dots, x_{m_1 m_2 - 1} - x_{m_1 m_2 - 2}$. Lemma 4.1 below uses it to turn a cover of $G \setminus \{0\}$ into a sequence in ℕ.

Lean names.

• SumFree S: $S$ is sumfree.
• CoveredBySumFree X n: $X$ is covered by $n$ sumfree sets.
• sdeg X : ℕ∞: the Schur degree, with ⊤ for $\infty$.
• blockSums A and average A, for A : List ℕ: $\hat A$ and $\mu(A)$.
• ERProperty n L: the length $L$ has the ER property for $n$.
• erL n: $L(n)$.
• ramseyBound k: $\rho(k)$.
• GroupSumFree C: $C$ is sumfree in $G$. The Lean definition takes any type with an addition; the targets use it for ZMod m₁ × ZMod m₂.
• liftPrefix m₁ M L: $x_L$, defined for all $m_1$ and $M$ by $x_L = (L \bmod m_1) + M \lfloor L/m_1 \rfloor$.
• liftSeq m₁ m₂ M: the lifted sequence, defined for all $m_1$, $m_2$ and $M$ as the list of the $m_1 m_2 - 1$ differences $x_{k+1} - x_k$.

Formalization targets

Goal

$$\mathrm{erL}\ 4 = 16$$

An exact value, so no later result changes the statement; it is the case Eliahou and Revuelta left open.

Theorem 4.1 of Eliahou–Revuelta, in ℕ, with $\rho(k)$ for $R_k(3)$

$$\rho(k) \le |A| + 1 \implies k + 1 \le \operatorname{sdeg}(\hat A) \qquad (k \in \mathbb{N},\ A \text{ a finite sequence in } \mathbb{N}).$$

Upper bound of Proposition 5.3, with $\rho(k)$ for $R_k(3)$

$$\mathrm{erL}(k+1) \le \rho(k) - 1 \qquad (k \in \mathbb{N}).$$

No length below 16 has the property at $n = 4$

$$\neg\,\mathrm{ERProperty}\ 4\ L \qquad (1 \le L \le 15).$$

Lemma 4.1 (McKenna 2026): lift from a group

For $m_1, m_2, q \ge 1$, $M \ge 3m_1 - 2$ and sets $C_1, \dots, C_q$, sumfree in $G$, that cover $G \setminus \{0\}$, the sequence $A =$ liftSeq m₁ m₂ M satisfies

$$|A| = m_1 m_2 - 1, \quad a_i > 0, \quad \operatorname{sdeg}(\hat A) \le q, \quad a_1 + \dots + a_L = x_L \ \ (L \le m_1 m_2 - 1).$$

Corollary 4.2 (McKenna 2026): group coverings bound $L(n)$ from below

For $n \ge 3$, $m_1, m_2 \ge 1$ and $n - 1$ sets, sumfree in $G$, that cover $G \setminus \{0\}$:

$$m_1 m_2 \le \mathrm{erL}\ n.$$

Theorem 1.2 (McKenna 2026), with the Lean upper bound: bounds for $L(5)$

$$49 \le \mathrm{erL}\ 5 \le 65.$$

Significance

$L(4) = 16$. At $n = 4$, Conjecture 5.6 predicts $L(4) = S(3) + 1 = 14$. So $L(4) = 16$ refutes the conjecture at $n = 4$. Here $L(n)$ equals the upper bound $R_{n-1}(3) - 1$ of Proposition 5.3.

The two bounds of Proposition 5.3 coincide at $n = 2, 3$, where the paper gives $L(2) = 2$ and $L(3) = 5$. So $n = 4$ is the first case in which the conjecture says more than Proposition 5.3.

$L(5) \ge 49$. At $n = 5$, Conjecture 5.6 predicts $L(5) = S(4) + 1 = 45$. So $L(5) \ge 49$ refutes the conjecture at $n = 5$.

What remains open. Conjectures 5.7 and 5.8 remain open.

The paper derives Conjecture 5.7 at each $n$ from Conjecture 5.6 at the same $n$, with Theorem 5.4. At $n = 4, 5$ that derivation is not available. But Conjecture 5.7 holds there by the known values: $44 \le 4 \cdot 14$ and $160 \le 5 \cdot 45$.

Conjecture 5.8 follows from Conjecture 5.6 at $n = 6$ (that is, $L(6) = 161$) with Theorem 5.4. Nothing here decides that case.

With $L(4) = 16$, Theorem 5.4 gives only $S(4) \le 64$. This is weaker than $S(4) \le R_4(3) - 2 \le 60$.

Status. Every target is proved and formalized.

• Theorem 4.1 and Proposition 5.3 are proved in the refereed paper.
• $L(4) = 16$ (Theorem 1.1), Lemma 4.1, Corollary 4.2 and $L(5) \ge 49$ (Theorem 1.2) are proved in McKenna 2026 (doi:10.5281/zenodo.22987189). Before publication, separate agents, with their own code, checked the proofs in two rounds of adversarial audit.

At launch, all 12 theorems of the tree, the goal included, are Proved in Lean over 4 definition bundles. Their only axioms are propext, Classical.choice and Quot.sound.

An independent verifier checked the definitions and the six headline statements against Eliahou–Revuelta and McKenna 2026. The six statements are the goal, Theorem 4.1, Proposition 5.3, Lemma 4.1, Corollary 4.2 and Theorem 1.2.

Literature. The literature search for McKenna 2026 found no result on $L(4)$, $L(5)$ or Conjectures 5.6–5.8. One citing text, in Jungić 2023, was not read. This records the search; it is not a claim of priority.

Open work, not targets.

• The exact $L(5)$: $49 \le L(5) \le 61$ on paper (with $R_4(3) \le 62$), and $49 \le L(5) \le 65$ in Lean.
• The case $n = 6$: $161 \le L(6) \le R_5(3) - 1 \le 306$ (DS1: $R_5(3) \le 307$). Here Conjecture 5.6 is the open step toward $S(6) \le 966$.

Difficulty

Two kinds of bound. The two sides of an exact value of $L(n)$ are statements of different kinds.

An upper bound $L(n) \le m$ needs one length. It follows from $\operatorname{sdeg}(\hat A) \ge n$ for every sequence $A$ of positive integers of one length $L$, with $1 \le L \le m$ and average at most $n$.

A lower bound $L(n) \ge m$ needs every shorter length. For every $L$ with $1 \le L < m$, it needs a sequence of $L$ positive integers, with average at most $n$, whose block sums are covered by $n - 1$ sumfree sets.

One counterexample at length $m - 1$ is not enough. A sequence of length $L + 1$ and average at most $n$ need not contain $L$ consecutive entries of average at most $n$. So monotonicity in $L$ does not follow directly from the definition.

The average bound. The lower bound $S(n-1) + 1$ of Proposition 5.3 comes from the constant sequence $(1, \dots, 1)$, with $\hat A = \{1, \dots, L\}$. Conjecture 5.6 states that at length $S(n-1) + 1$, no sequence of average at most $n$ has $\operatorname{sdeg}(\hat A) \le n - 1$.

Without the bound on the average, this fails. The paper gives a sequence of length 14 with $\operatorname{sdeg}(\hat A) = 3$, found by semi-random search. Its average is 114, and the authors remark that such examples "are hard to come by".

The gap for $L(5)$. The gap from 49 to 61 is open. By McKenna 2026 (§5), the construction of Corollary 4.2 gives nothing above 49 at $n = 5$:

• $S(4) = 44$ excludes the cyclic groups of order at least 46.
• Solver runs exclude the non-cyclic groups of order 50 to 60. Their unsatisfiability proofs (in the DRAT format) were checked.
• $L(5) \le 61$ excludes the orders of 62 or more.

McKenna 2026 knows no sequence of length 49 with average at most 5 and $\operatorname{sdeg}(\hat A) \le 4$; such a sequence would give $L(5) \ge 50$.

Formalization scope

• Ambient ℕ. The paper works in an abelian group; here sets are Set ℕ and sequences List ℕ. For $X \subseteq \mathbb{N}$ the Schur degree is the same in ℕ and in ℤ. Theorem 4.1 is formalized for sequences in ℕ only.
• sdeg is sInf in ℕ∞, so it is ⊤ when no cover exists, and $\operatorname{sdeg}(\emptyset) = 1$. Covers are Fin n → Set ℕ; the sets need not be disjoint or inside $X$. Each lower bound on sdeg must exclude every cover.
• blockSums A uses B <:+: A with B ≠ []; average [] = 0 is never used, since erL requires $L > 0$.
• erL n is sInf {L | 0 < L ∧ ERProperty n L} in ℕ, defined for every $n$ (the paper: $n \ge 2$). As sInf ∅ = 0, an upper bound on erL alone would hold if no length had the property; the Theorem 4.1 target excludes this, giving ERProperty (k+1) at length $\rho(k) - 1 \ge 1$, and 0 satisfies neither the goal nor the lower bounds.
• Ramsey bound. $\rho(k)$ replaces $R_k(3)$. TriangleRamsey k N says every colouring of the pairs $x < y$ of at least $N$ naturals with at most $k$ colours has a monochromatic triangle; the tree proves it for $N = \rho(k)$. As $\rho(4) = 66 > 62 \ge R_4(3)$, the Lean upper bound for $L(5)$ is 65, not 61.
• Lemma 4.1, Corollary 4.2. As in McKenna 2026, the sets need only cover $G \setminus \{0\}$, and Lemma 4.1 requires $q \ge 1$: for $q = 0$, $m_1 = m_2 = 1$ the sequence is empty and $\operatorname{sdeg}(\emptyset) = 1$. The prefix sums are exact: $x_L$.
• Subtraction is truncated; with $m_1, m_2 \ge 1$ and $\rho(k) \ge 2$, none of 3 * m₁ - 2, m₁ * m₂ - 1, ramseyBound k - 1 and n - 1 in Fin (n - 1) ($n \ge 3$) truncates, and the differences in liftSeq do not truncate when $M \ge m_1 \ge 1$.
• Finite checks use kernel decide; no native_decide, no external certificate.

Bundles: ClassicalSchurBasic (the objects of the Setting), ClassicalSchurRamsey (TriangleRamsey, ramseyBound), ClassicalSchurLift (GroupSumFree, liftPrefix, liftSeq), ClassicalSchurValues (the finite data of the two value theorems). As a check, the definitions give the paper's values erL 2 = 2 and erL 3 = 5 (checked in Lean by an independent verifier in a scratch file; not in the tree). Reusable: the definitions of ClassicalSchurBasic (the interface lemmas are inlined in the proofs, not separate nodes), TriangleRamsey k (ramseyBound k), and the lift from group coverings. Welcome beyond the targets: a formal TriangleRamsey 4 62, which with not_coveredBySumFree_blockSums gives $L(5) \le 61$ in Lean; the exact $L(5)$; the case $n = 6$.

Selected references

• S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, Discrete Math. 344 (2021) 112332. https://doi.org/10.1016/j.disc.2021.112332
• S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, preprint, arXiv:2006.01502v1, 2020. https://arxiv.org/abs/2006.01502v1
• R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
• H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
• M. J. H. Heule, Schur number five, Proc. AAAI-18, 2018; preprint arXiv:1711.08076, 2017. https://arxiv.org/abs/1711.08076
• S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
• A. McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49, Zenodo, 2026. https://doi.org/10.5281/zenodo.22987189 (version 1.0.1: https://doi.org/10.5281/zenodo.22987688). The Lean library ClassicalSchur and the comparator check: https://github.com/mysticflounder/schur-degree-block-sums (tag v1.0.1).