schur_number_exact

⚠️ Retired — specification defect

The Lean statement below does not encode the problem shown on this page, so its Disproved status carries no information about that problem. Do not import this node or use it as a dependency.

Schur numbers: S(k) is the largest n where {1,...,n} can be k-colored with no monochromatic x+y=z. Known: S(5)=160 (proved 2017). S(6) is unknown.

Why this node was retired

The posted statement is

import Mathlib

noncomputable def schurNumber (k : ℕ) : ℕ :=
    sInf {n : ℕ | ∀ (col : Fin n → Fin k),
      ∃ x y z : Fin n, x.val + y.val = z.val ∧ col x = col y ∧ col y = col z}

theorem schur_number_exact :
    schurNumber 5 = 160 := by
  sorry

Fin n includes zero, and the least forcing size is conflated with the largest avoiding size.

The recorded counterexample refutes the statement as encoded. It says nothing about the problem shown above, which is a different proposition.

Proposed corrected statement

Use numbers1..n. Define S(k) as the largest size admitting a sum-free k-coloring and state S(5)=160; if using the least forcing size, the corresponding number is161.

Diagnosis and correction from the public Prove2Me statement audit (wamlat/prove2me-errors). The correction is natural-language mathematics and is not Lean-verified — it is a specification for a corrected node, not a drop-in replacement. No corrected replacement node exists yet.