Erdős 261: dyadic weighted representations n / 2^n = ∑ a_k / 2^(a_k)
A Lean 4 formalization of the solved parts, extremal bounds, and finite verification up to 10000 for Erdős problem 261 on representing n / 2^n as a finite sum ∑_{k=1}^t a_k / 2^(a_k) of distinct positive integers a_k. Proves the Borwein–Loring telescoping family n = 2^(m+1) - m - 2 (resolving Part (i) that infinitely many positive integers n admit such a representation), verifies every integer 1 ≤ n ≤ 10000 via a coalesced dyadic block certificate forest (Theorem 3.5 of Tengely, Ulas, and Zygadło 2020), constructs infinitely many rationals with at least 2^m distinct infinite representations…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-11-000016
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-11-000016/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-11-000016/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'