Motivation

A set of integers is sum-free when no two of its members add up to a third. Schur's theorem (1916) says that for every $k$ there is a largest interval $[1,N]$ that can be split into $k$ sum-free classes, and the resulting Schur numbers $S(k)$ are notoriously hard to compute: $S(5) = 160$ was settled only in 2018, by a SAT computation with a machine-checked proof certificate.

Replacing "adds up to" by "adds up to, modulo $m$" gives a family that behaves very differently. Modular Schur numbers were introduced by Chappelon, Revuelta Marchena and Sanz Domínguez, who settled the moduli $m \in \{1,2,3\}$ and proved the universal bound $S_m(k,\ell) \le m-1$ (Electron. J. Combin. 20(2) (2013) #P61). D'orville, Sim, Wong and Ho then closed $m \in \{4,5,6,7\}$ by residue case analysis and posed the general modulus as an open problem (Integers 25 (2025) #A62, their Problem 1). Each additional modulus had cost a separate case analysis, and the case analysis grew with $m$.

The timeline matters for reading what follows. The 2013 paper supplies the universal cap. The 2025 paper supplies a singleton criterion (its Theorem 4) and a divisibility obstruction (its Corollary 3), and applies the latter only in the coprime case $\gcd(m,\ell-1)=1$ (its Corollary 5). What remained was to optimise that obstruction over every residue rather than only in the coprime case, which is what collapses the whole family to one formula.

Setting

Fix integers $m \ge 2$, $\ell \ge 2$ and $k \ge 1$. A set $S$ of integers is $\ell$-sum-free modulo $m$ when there are no $x_1, \dots, x_\ell \in S$ and $y \in S$, repetitions among the $x_i$ allowed, with

$$x_1 + \cdots + x_\ell \equiv y \pmod m .$$

The repetition clause is not a technicality: a single element can make its whole class unsafe. The modular Schur number $S_m(k,\ell)$ is the greatest $N \ge 0$ such that the interval $[1,N]$ can be partitioned into at most $k$ classes, each $\ell$-sum-free modulo $m$. A partition into such classes is called valid.

Two derived quantities carry the whole story. Write

$$d = \gcd(m, \ell - 1), \qquad n = \frac{m}{d} .$$

Then $dn = m$ exactly, and $d \mid (\ell - 1)$ by construction. All Lean statements in this mission use these same names.

Formalization targets

Goal: the closed form in the many-colours regime

$$S_m(k,\ell) = \frac{m}{\gcd(m,\ell-1)} - 1 = n - 1 \qquad \text{for all } m \ge 2,\ \ell \ge 2,\ k \ge n-1 .$$

Closed form here means something precise: the value is produced from $m$ and $\ell$ by one gcd, one division and one subtraction, with no search over colourings, no recursion, and no case split on $\ell \bmod m$. The statement fixes no constants and no modulus, so it is not invalidated by any later refinement of the threshold in $k$.

The single-colour value

$$S_m(1,\ell) = \min\!\left(\ell - 1, \left\lfloor \frac{m}{\ell} \right\rfloor\right) \qquad (2 \le \ell \le m),$$

together with the complementary regime $m < \ell$, where the value is $0$ if $\ell \equiv 1 \pmod m$ and $1$ otherwise. The two together give a value for every admissible pair $(m,\ell)$ at $k=1$, and the tree carries that combined formula at the residue level and at the integer level.

Significance

What the results give. One expression replaces an open-ended sequence of per-modulus case analyses. The moduli $m \in \{1,2,3\}$ of the 2013 paper and $m \in \{4,5,6,7\}$ of the 2025 paper are specialisations, and every remaining modulus is covered at once in the stated range of $k$.

The mechanism is a single self-defeating value. Take $\ell$ copies of $n$: they sum back to $n$ modulo $m$, so the lone class $\{n\}$ already breaks the rule, while every smaller value is safe. That one observation supplies a matching upper and lower bound.

• The upper bound is uniform in $k$. Adding colours never raises the value past $n-1$, which is what makes the formula stable.
• The lower bound costs $n-1$ colours, one per safe residue. Identifying the least sufficient number of colours is where the subject is still open.

Status of the tree, stated precisely. Everything listed under Formalization targets is both proved and machine-checked.

• 21 theorems and 3 definition bundles, each with a complete Lean proof verified by this platform.
• Axiom-clean: each closure is contained in {propext, Classical.choice, Quot.sound}.
• This mission therefore publishes a finished development rather than an open call on its stated goal.
• What is genuinely open is listed under Difficulty below, and is not part of the verified tree.

Relation to the accompanying paper. The paper states the single-colour value only under $2 \le \ell \le m$. Three results in the tree go beyond it: the complementary regime $m < \ell$, and the combined formula covering every $m \ge 2$ and $\ell \ge 2$, stated once at the residue level and again at the integer level. Two further results, the coset-cardinality bounds, are supporting work of the Lean development and are not numbered results of the paper. Each theorem's source field records which of these it is.

Difficulty

The threshold in $k$ is not $n-1$

The obvious attack on the general modulus is to guess that only singletons can be safe classes. The threshold in $k$ would then be exactly $n-1$, and the problem would close for all $k$ at once. That guess is false.

Take $m = 12$ and $\ell \equiv 11 \pmod{12}$, so $d = 2$ and $n = 6$. The two-element set $\{1,5\}$ is $\ell$-sum-free modulo $12$, and three colours then suffice where the singleton count would demand five.

So the least $k$ at which the closed form takes hold, written $k_0(m,\ell)$, is not $n-1$ in general. What is known about it:

• Prime moduli. $k_0(p,\ell) = p-1$ for every $\ell \ge p-1$ with $\ell \not\equiv 1 \pmod p$.
• Composite moduli. Bracketed above and below, but not determined.

A correction to the published prime-power formula

Theorem 8 of D'orville, Sim, Wong and Ho gives a three-branch formula at prime-power moduli. Its middle branch is false. The correction is stated here in full because it bears directly on the threshold.

• The counterexample. At $p = 2$, $i = 3$, $k = 3$ and $\ell = 8$ that branch gives $S_8(3,8) = 5$, while the correct value is $S_8(3,8) = 7$.
• Where the proof fails. In the supporting Lemma 2(2) of that paper. The pair $a = 2$, $b = 6$ satisfies every hypothesis of that lemma at $p = 2$, $i = 3$, $\ell = 8$, yet $\{2,6\}$ is $8$-sum-free modulo $8$.
• The replacement result.

$$S_{p^i}(k,\ell) = p^i - 1 \qquad \text{for } p \text{ prime},\ i \ge 1,\ \ell \ge 2,\ p \nmid (\ell - 1), \text{ and every } k \ge i(p-1) .$$

It is proved from a valuation-layer colouring that consumes $i(p-1)$ classes, together with the universal cap. The hypothesis $p \nmid (\ell-1)$ forces $d = 1$ and $n = p^i$, so the replacement reaches the goal theorem's value at $k \ge i(p-1)$ in place of $k \ge p^i - 1$, and it contradicts the printed middle branch for infinitely many triples $(p, i, \ell)$.

Status of that correction, stated precisely.

• It is a prose proof in a draft note, listed under Selected references below and readable in full there.
• It is not formalized, and it is not part of this mission's verified tree.
• Nothing in the verified tree depends on it.
• It is recorded here because a reader who compares this mission against the 2025 paper will otherwise meet the contradiction with no explanation. Formalizing it is the subject of a separate mission.

The intermediate regime

For $1 < k < n-1$ the classes must be simultaneously large and $\ell$-sum-free, and no formula is known. The value is empirically eventually periodic in $\ell \bmod m$ for fixed $k$, verified through $m \le 13$.

None of these open directions is weakened by the goal theorem, which deliberately assumes enough colours to avoid the question.

Formalization scope

Two levels of statement

Two levels appear in the tree, and the distinction between them is the first thing to fix.

• At the integer level the objects are the integers $1, \dots, N$ themselves.
• At the residue level they are their classes modulo $m$, which in Lean is the type ZMod m: Mathlib's type of residues modulo $m$, a commutative ring with exactly $m$ elements for $m \ge 1$, carrying the reduction map from $\mathbb{Z}$ and the arithmetic that map preserves.

Working in ZMod m turns "adds up to, modulo $m$" into a plain equation instead of a divisibility side condition, and it makes every colour class a subset of a finite type.

Conventions

The development works residue-by-residue in ZMod m and commits to the following conventions, all of which are silent in the prose and load-bearing in Lean.

• $\ell$-tuples are functions Fin ℓ → ZMod m valued in the class. This builds in "repetitions allowed" rather than leaving it to a side condition.
• Classes are Finsets, so finiteness is structural.
• A valid partition is a structure with four fields: covering, pairwise disjointness, containment in the target set, and $\ell$-sum-freeness of each class.
• Empty classes are permitted. This is what makes "at most $k$" and "exactly $k$" interchangeable once any colouring exists.

The two numbers, and the cap in their definition

Both a residue-level and an integer-level number are defined, and a reduction theorem proves them equal for every $m \ge 2$. Bounds are proved on the residue side and quoted on the integer side.

Both are defined with Nat.findGreatest against the bound $m-1$. That cap is neither an approximation nor a trivialising choice: a separate theorem shows any $N$ admitting a valid partition satisfies $N \le S_m(k,\ell)$ with no hypothesis on $N$, because $N \ge m$ admits no valid partition at all. A reader checking for a vacuous formalization should also note that the goal is an equality, not a bound, so it cannot be satisfied by weakening a hypothesis.

Reusable beyond this mission

• the residue-reduction bridge;
• the singleton criterion;
• the two coset-cardinality bounds, which are pure counting statements about subsets of a cyclic group whose differences lie in a proper subgroup.

Contributions welcome on the open directions named under Difficulty, in particular any lowering of the threshold in $k$ toward $k_0$, and a closed form for $k_0$ at composite moduli.

Selected references

• J. Chappelon, M. P. Revuelta Marchena, M. I. Sanz Domínguez, Modular Schur numbers, Electron. J. Combin. 20(2) (2013) #P61. https://doi.org/10.37236/2374 (also arXiv:1306.5635)
• J. D'orville, K. A. Sim, K. B. Wong, C. K. Ho, Modular generalizations of Schur numbers, Integers 25 (2025) #A62. https://math.colgate.edu/~integers/z62/z62.pdf
• M. J. H. Heule, Schur number five, AAAI 2018. arXiv:1711.08076
• A. McKenna, A correction to a prime-power formula for modular Schur numbers, 2026. Draft note, not submitted for publication. Released in the repository below on 2026-09-20: PDF · Markdown source
• A. McKenna, Prime-power structure of the stable regime for modular Schur numbers, 2026. Lean development and paper: https://github.com/mysticflounder/modular-schur