Prove2Me

Erdős Problem 261: the representation property n/2n=∑ak/2akn/2^n=\sum a_k/2^{a_k} and the greedy carry

Definition
Erdos261_defs

by Ethan Cheung Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

erdos-problemsnumber-theory

Erdős261Prop. A natural number nn has property Erdos261Prop if there exist t≥2t\ge2 pairwise distinct positive integers a1,…,ata_1,\dots,a_t with

n2n=∑k=1tak2ak.\frac{n}{2^n}=\sum_{k=1}^{t}\frac{a_k}{2^{a_k}}.

This is copied verbatim from Google DeepMind's Formal Conjectures file for Erdős Problem 261 (the open part asks whether every n≥1n\ge1 has the property).

Greedy carry. g0=ng_0=n and gj+1=2gj−(n+j+1)g_{j+1}=2g_j-(n+j+1) if 2gj≥n+j+12g_j\ge n+j+1, otherwise gj+1=2gjg_{j+1}=2g_j. This is the greedy digit iteration of Borwein–Loring and Tengely–Ulas–Zygadło started at (n,n)(n,n); gj=0g_j=0 for some jj means the greedy algorithm finds a finite representation.

Definition code
import Mathlib

namespace Erdos261

/-- Verbatim from Formal Conjectures `FormalConjectures/ErdosProblems/261.lean`. -/
def Erdos261Prop (n : ℕ) : Prop := ∃ᵉ (t ≥ 2) (a : Fin t → ℕ), a.Injective ∧
  (1 ≤ a) ∧ n / (2 ^ n : ℚ) = ∑ k, (a k) / (2 ^ (a k) : ℚ)

/-- The greedy carry from `(n, n)`: `g₀ = n`, `g_{j+1} = 2 g_j - (n+j+1)` if `2 g_j ≥ n+j+1`,
otherwise `g_{j+1} = 2 g_j` (the Borwein–Loring / Tengely–Ulas–Zygadło greedy iteration). -/
def greedy (n : ℕ) : ℕ → ℤ
  | 0 => n
  | j + 1 => if ((n + j + 1 : ℕ) : ℤ) ≤ 2 * greedy n j
      then 2 * greedy n j - ((n + j + 1 : ℕ) : ℤ) else 2 * greedy n j

end Erdos261
Source
Erdős Problem 261, https://www.erdosproblems.com/261; Formal Conjectures FormalConjectures/ErdosProblems/261.lean (def Erdos261Prop); greedy: Tengely, Ulas, Zygadło, J. Number Theory 217 (2020), arXiv:2008.01501, §3

View graph