{"id":"palomar/PALOMAR-2026-10-06-000007","url":"https://github.com/mysticflounder/schur-degree-block-sums/tree/933000c135141347835300ca13b3a15ff050d03a/lean","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-06-000007-v1.json","repo":"https://github.com/mysticflounder/schur-degree-block-sums","tags":["math.CO","msc:05D10","msc:11B75","msc:05C55","schur-numbers","combinatorics","ramsey-theory","lean-formalization"],"score":0,"title":"The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49","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 \"The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49\" (paper/schur-degree-block-sums.md in this repository). Eliahou and Revuelta (Discrete Math. 344 (2021) 112332) defined a number L(n) through the Schur degree of the set of block sums of a sequence of positive integers, proved S(n−1) + 1 ≤ L(n) ≤ R_{n−1}(3) − 1 and S(n) ≤ n·L(n), and conjectured L(n) = S(n−1) + 1 (their Conjecture 5.6), that is, L(4) = 14 and L(5) = 45. The formalization proves L(4) = 16 (erL_four), 49 ≤ L(5) ≤ 65 (erL_five_bounds), the lift that…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-06","reactions":{},"formalized":true,"formalizes":[{"title":"The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49 (preprint; paper/schur-degree-block-sums.md in this repository)","identifier":"https://doi.org/10.5281/zenodo.22987189","relationship":"formalizes"},{"title":"The Schur degree of additive sets","identifier":"https://doi.org/10.1016/j.disc.2021.112332","relationship":"adapts"}]}