Prove2Me

Block rewrite of a representation of n/2nn/2^n

Proved
Erdos261.block_rewrite

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

erdos-problemsnumber-theory

Write Rep⁡\operatorname{Rep} for a representation n2n=∑kak2ak\frac{n}{2^n}=\sum_k \frac{a_k}{2^{a_k}} by pairwise distinct positive integers aka_k (Erdős Problem 261). Theorem. Let q=2m+1−m−2q=2^{m+1}-m-2. If n2n=∑k∈Sk2k\frac{n}{2^n}=\sum_{k\in S}\frac{k}{2^k} for a finite set SS with q∈Sq\in S and S∩{q+1,…,q+m}=∅S\cap\{q+1,\dots,q+m\}=\varnothing, then S′=(S∖{q})∪{q+1,…,q+m}S'=(S\setminus\{q\})\cup\{q+1,\dots,q+m\} also satisfies n2n=∑k∈S′k2k\frac{n}{2^n}=\sum_{k\in S'}\frac{k}{2^k}, and ∣S′∣+1=∣S∣+m|S'|+1=|S|+m.

The rewrite replaces one term by a Borwein–Loring block. The reverse rewrite lowers the number of terms by m−1m-1, so it terminates.

Preamble
import Mathlib
import Definitions.Def_Erdos261_defs
open Finset
Formal statement
namespace Erdos261

theorem block_rewrite (n m : ℕ) (S : Finset ℕ)
    (hS : (n : ℚ) / 2 ^ n = ∑ k ∈ S, (k : ℚ) / 2 ^ k)
    (hq : 2 ^ (m + 1) - m - 2 ∈ S)
    (hdisj : Disjoint S (Ioc (2 ^ (m + 1) - m - 2) (2 ^ (m + 1) - m - 2 + m))) :
    (n : ℚ) / 2 ^ n = ∑ k ∈ S.erase (2 ^ (m + 1) - m - 2) ∪
        Ioc (2 ^ (m + 1) - m - 2) (2 ^ (m + 1) - m - 2 + m), (k : ℚ) / 2 ^ k ∧
      #(S.erase (2 ^ (m + 1) - m - 2) ∪ Ioc (2 ^ (m + 1) - m - 2) (2 ^ (m + 1) - m - 2 + m))
        + 1 = #S + m := by sorry

end Erdos261
Source
Erdős Problem 261 (https://www.erdosproblems.com/261); definitions from Formal Conjectures 261.lean; Corollary A5 of GPT 6.1 Sol; lemma proposed by GPT 6.1 Sol (Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph