Schur numbers

DefinitionSchur forcing property#✓fully proved

For natural numbers \(k\) and \(N\), we say that \(N\) forces a monochromatic Schur triple in \(k\) colours when every colouring \(c\) of the natural numbers with \(k\) colours has \(x, y, z \in \{1, \dots, N\}\) with \(x + y = z\) and \(c(x) = c(y) = c(z)\).

Solutions with \(x = y\) count, so this property gives the Schur numbers, not the weak Schur numbers.

def schurForces (k N : ℕ) : Prop :=
  ∀ c : ℕ → Fin k, ∃ x ∈ Icc 1 N, ∃ y ∈ Icc 1 N, ∃ z ∈ Icc 1 N,
    x + y = z ∧ c x = c y ∧ c y = c z
Used by 1
Used bySchur number

DefinitionSchur number#✓fully proved

For \(k \ge 1\), the Schur number \(S(k)\) is \(N_0 - 1\), where \(N_0\) is the least natural number \(N\) that forces a monochromatic Schur triple in \(k\) colours: every colouring \(c\) of the natural numbers with \(k\) colours has \(x, y, z \in \{1, \dots, N\}\) with \(x + y = z\) and \(c(x) = c(y) = c(z)\). For \(k = 0\), \(S(0) = 0\).

Such an \(N_0\) exists by Schur's theorem, and \(S(k)\) is the largest \(N\) such that \(\{1, \dots, N\}\) splits into \(k\) sum-free parts, some possibly empty (OEIS A045652); the numbers \(N_0 = S(k) + 1\) form OEIS A030126.

noncomputable def schurNumber (k : ℕ) : ℕ :=
  if k < 1 then 0 else sInf {N | schurForces k N} - 1
Uses 1 · Used by 6
Statement usesSchur forcing property
Used byLower bound for the sixth Schur number · The fifth Schur number · The fourth Schur number · Upper bound for the sixth Schur number · The third Schur number · The second Schur number

TheoremThe second Schur number#●ready to prove

The Schur number \(S(2)\) equals \(4\).

public theorem_wanted schurNumber_two : schurNumber 2 = 4
Sources
  • exhaustive check; OEIS A045652; listed in leansolving/SqueezeBench SqueezeBench/Problems/Schur/README.md.
Uses 1
Statement usesSchur number

TheoremThe third Schur number#●ready to prove

The Schur number \(S(3)\) equals \(13\).

public theorem_wanted schurNumber_three : schurNumber 3 = 13
Sources
  • exhaustive check; OEIS A045652; listed in SqueezeBench SqueezeBench/Problems/Schur/README.md.
Uses 1
Statement usesSchur number

TheoremThe fourth Schur number#●ready to prove

The Schur number \(S(4)\) equals \(44\).

public theorem_wanted schurNumber_four : schurNumber 4 = 44
Sources
  • S. W. Golomb and L. D. Baumert, Backtrack programming, J. ACM 12 (1965), 516–524; OEIS A045652; listed in SqueezeBench SqueezeBench/Problems/Schur/README.md.
Uses 1
Statement usesSchur number

TheoremThe fifth Schur number#●ready to prove

The Schur number \(S(5)\) equals \(160\).

public theorem_wanted schurNumber_five : schurNumber 5 = 160
Sources
  • M. J. H. Heule, Schur Number Five, Proc. AAAI 2018, 6598–6606 (arXiv:1711.08076), a DRAT-verified SAT proof; OEIS A045652; listed in SqueezeBench SqueezeBench/Problems/Schur/README.md.
Uses 1
Statement usesSchur number

TheoremLower bound for the sixth Schur number#●ready to prove

The Schur number \(S(6)\) is at least \(536\).

public theorem_wanted le_schurNumber_six : 536 ≤ schurNumber 6
Sources
  • H. Fredricksen and M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000), R32; listed in SqueezeBench SqueezeBench/Problems/Schur/README.md.
Uses 1
Statement usesSchur number

TheoremUpper bound for the sixth Schur number#●ready to prove

The Schur number \(S(6)\) is at most \(1836\).

public theorem_wanted schurNumber_six_le : schurNumber 6 ≤ 1836
Sources
  • the multicolour Ramsey bound R₆(3) ≤ 1838 (S. P. Radziszowski, Small Ramsey Numbers, Electron. J. Combin. Dynamic Survey DS1) together with S(k) ≤ R_k(3) - 2; the range 536 ≤ S(6) ≤ 1836 is stated in S. Eliahou and D. F. Revuelta, The Schur degree of additive sets, arXiv:2006.01502; listed in SqueezeBench SqueezeBench/Problems/Schur/README.md.
Uses 1
Statement usesSchur number
2 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.