{"id":"palomar/PALOMAR-2026-11-04-000007","url":"https://github.com/mysticflounder/schur-538/tree/c3306693e01496162241bb7630ff2f19bd1482b7/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-04-000007-v1.json","repo":"https://github.com/mysticflounder/schur-538","tags":["math.CO","msc:05D10","msc:11B75"],"score":0,"title":"A Schur 6-colouring of [1, 538]","trust":"high","domain":"math.CO","source":"palomar","authors":["Adam McKenna"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 check, with Lean core only, of the existence of a colouring of the integers 1 to 538 with 6 colours and no monochromatic x + y = z, with x = y allowed. So the integers 1 to 538 are the union of six sum-free sets, which gives S(6) ≥ 538 for the Schur number S(6). The largest lower bound in the sources that the author read on 3 November 2026 is S(6) ≥ 537, by Chen, Zhu and Long. The paper paper/schur-six-538.md in this repository states the result.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-04","reactions":{},"formalized":true}