{"id":"palomar/PALOMAR-2026-10-23-000014","url":"https://github.com/Paulee314/erdos1063-lean/tree/ba104cbcf0bb7c555a8b2f0d58018989a08c638e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-23-000014-v1.json","repo":"https://github.com/Paulee314/erdos1063-lean","tags":["math.NT","msc:11B65","msc:11A05","number-theory","binomial-coefficients","erdos-problems"],"score":0,"title":"Erdős Problem 1063: a lower bound for n_k and the structure of the exceptional index","trust":"high","domain":"math.NT","source":"palomar","authors":["Paul Lee"],"reviews":0,"subject":"math.NT","summary":"For k ≥ 2 let n_k be the least n ≥ 2k such that n − i divides the binomial coefficient C(n, k) for all but exactly one 0 ≤ i < k (Erdős Problem 1063; Erdős and Selfridge 1983; OEIS A389360; Guy's Unsolved Problems in Number Theory, B31). Using the definition of n_k from google-deepmind/formal-conjectures verbatim, this project proves two results in Lean 4 with Mathlib. (1) For every k ≥ 2, n_k ≥ W'_k = ∏_{p^a ∥ k} p^(a + ⌊log_p(k − 1)⌋); the bound is attained in the sense that n_k − i₀ = W'_k for k = 4, 6, 14. (2) If n ≥ 2k, e < k, and every n − i with 0 ≤ i < k, i ≠ e, divides C(n, k), then…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-23","reactions":{},"formalized":true,"formalizes":[{"title":"Proof of the sharper exponent v_p(n − e) ≥ v_p(k) + v_p(C(k − 1, e)) + ⌊log_p max(e, k − 1 − e)⌋ for p | k, in the erdosproblems.com discussion thread for Problem 1063 (10 July 2026)","identifier":"","relationship":"formalizes"},{"title":"The density of admissible n in Erdős–Selfridge problem 1063, with a growth conjecture for n_k (preprint)","identifier":"https://github.com/Paulee314/erdos1063/blob/6b4f9666c8834395ef1669634536350223fb270f/paper/erdos1063.pdf","relationship":"formalizes"}]}