{"id":"palomar/PALOMAR-2026-10-11-000016","url":"https://github.com/linrock/math-proofs/tree/b53791ff6294b4b90e3653970367f127a52fd16e/erdos-261","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-11-000016-v1.json","repo":"https://github.com/linrock/math-proofs","tags":["math.NT","msc:11D61","msc:11B75","number-theory","egyptian-fractions","lean-formalization"],"score":0,"title":"Erdős 261: dyadic weighted representations n / 2^n = ∑ a_k / 2^(a_k)","trust":"high","domain":"math.NT","source":"palomar","authors":["Linmiao Xu"],"reviews":0,"subject":"math.NT","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-11","reactions":{},"formalized":true,"formalizes":[{"title":"Some questions of Erdős and Graham on numbers of the form ∑ g_n / 2^{g_n}","identifier":"https://doi.org/10.1090/S0025-5718-1990-0993927-5","relationship":"formalizes"},{"title":"On a Diophantine equation of Erdős and Graham","identifier":"https://arxiv.org/abs/2008.01501","relationship":"formalizes"}]}