Prove2Me

Integer form of the representation equation n/2n=∑k∈Sk/2kn/2^n=\sum_{k\in S}k/2^k

Proved
Erdos261.rep_iff_int

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 1≤n≤N1\le n\le N and let S⊆{1,…,N}S\subseteq\{1,\dots,N\}. Put cj=j [j∈S]−n [j=n]c_j=j\,[j\in S]-n\,[j=n]. Then

n2n=∑k∈Sk2k  ⟺  ∑j=1Ncj 2N−j=0.\frac{n}{2^n}=\sum_{k\in S}\frac{k}{2^k}\iff\sum_{j=1}^{N}c_j\,2^{N-j}=0.

Multiplying by 2N2^N turns the rational identity into an integer column identity, the input of the signed binary-carry formulation.

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

theorem rep_iff_int (n N : ℕ) (S : Finset ℕ) (hn : 1 ≤ n) (hnN : n ≤ N) (hS : S ⊆ Icc 1 N) :
    (n : ℚ) / 2 ^ n = ∑ k ∈ S, (k : ℚ) / 2 ^ k ↔
      ∑ j ∈ Icc 1 N, ((if j ∈ S then (j : ℤ) else 0) - (if j = n then (n : ℤ) else 0)) *
        2 ^ (N - j) = 0 := by sorry

end Erdos261
Source
Erdős Problem 261 (https://www.erdosproblems.com/261); definitions from Formal Conjectures 261.lean; Lemma A2 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