{"id":"palomar/PALOMAR-2026-10-06-000003","url":"https://github.com/mysticflounder/schur-centred-bound/tree/6b1c69732d73428042efce8d563f67604320cad4","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-06-000003-v1.json","repo":"https://github.com/mysticflounder/schur-centred-bound","tags":["math.CO","msc:05D10","msc:11B75","msc:05C55","ramsey-theory","schur-numbers","combinatorics","lean-formalization"],"score":0,"title":"S(6) ≤ 1801 if R₄(3) ≤ 61: a centred Schur bound and the structure at the frontier","trust":"high","domain":"math.CO","source":"palomar","authors":["Adam McKenna"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization, with Mathlib, of an upper bound for the Schur numbers in terms of the triangle Ramsey numbers, and of the structure of a colouring at the limit of that bound. If every colouring with k colours of the pairs of r points has a monochromatic triangle (R_k(3) ≤ r), then the interval [1, 2((k + 1)⌊(r − 1)/2⌋ + 1)] is not covered by k + 1 sumfree sets, so S(k + 1) ≤ 2(k + 1)⌊(r − 1)/2⌋ + 1. With R_2(3) ≤ 6 this gives S(3) ≤ 13, which is exact. Under the hypothesis R_4(3) ≤ 61, a computer-assisted claim of M. Tatarevic that this project does not prove, the pigeonhole step…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-06","reactions":{},"formalized":true}