{"id":"palomar/PALOMAR-2026-09-01-000001","url":"https://github.com/mysticflounder/modular-schur/tree/7c91cf3c5ca9b50354a74344dce71a28c9fefa01/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-01-000001-v2.json","repo":"https://github.com/mysticflounder/modular-schur","tags":["math.CO","math.NT","msc:05D10","msc:11B13","msc:11B75","msc:68V20","combinatorics","number-theory","lean-formalization","schur-numbers"],"score":0,"title":"Modular Schur numbers: S_m(k,ℓ) = n − 1 for k ≥ n − 1, where n = m/gcd(m,ℓ−1)","trust":"high","domain":"math.CO","source":"palomar","authors":["Adam McKenna"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 formalization, with Mathlib, of the main results of the paper \"Prime-power structure of the stable regime for modular Schur numbers\" (docs/paper/modular-schur.pdf in this repository). The modular Schur number S_m(k,ℓ), introduced by Chappelon, Revuelta Marchena and Sanz Domínguez (2013), is the largest N such that 1, …, N can be coloured with k colours so that no colour class contains a solution of x_1 + ⋯ + x_ℓ ≡ y (mod m). For m ≥ 2 and ℓ ≥ 2, put n = m/gcd(m,ℓ−1). The main theorem is the closed form S_m(k,ℓ) = n − 1 for every k ≥ n − 1. D'orville, Sim, Wong and Ho (Integers 25…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"Prime-power structure of the stable regime for modular Schur numbers","identifier":"https://github.com/mysticflounder/modular-schur/blob/main/docs/paper/modular-schur.pdf","relationship":"formalizes"},{"title":"Modular Schur numbers","identifier":"Electron. J. Combin. 20(2) (2013) #P61; arXiv:1306.5635","relationship":"formalizes"},{"title":"Modular generalizations of Schur numbers","identifier":"Integers 25 (2025) #A62","relationship":"adapts"}]}