The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-06-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-06-000007/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-06-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'