Erdős Problem 1063: a lower bound for n_k and the structure of the exceptional index
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-23-000014
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-23-000014/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-23-000014/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'