Prove2Me

Borwein–Loring block identity for qm=2m+1−m−2q_m=2^{m+1}-m-2

Proved
Erdos261.bl_block

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

erdos-problemsnumber-theory

Theorem. For every m≥0m\ge0, with qm=2m+1−m−2q_m=2^{m+1}-m-2,

qm2qm=∑qm<k≤qm+mk2k.\frac{q_m}{2^{q_m}}=\sum_{q_m<k\le q_m+m}\frac{k}{2^k}.

For m≥2m\ge2 this exhibits a representation of qm/2qmq_m/2^{q_m} by mm distinct terms (Borwein–Loring), and it is the block used in the rewrite rule for representations in Erdős Problem 261.

Formalization Note. Natural-number subtraction is harmless since m+2≤2m+1m+2\le2^{m+1}; the cases m=0,1m=0,1 are included.

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

theorem bl_block (m : ℕ) :
    ((2 ^ (m + 1) - m - 2 : ℕ) : ℚ) / 2 ^ (2 ^ (m + 1) - m - 2) =
      ∑ k ∈ Ioc (2 ^ (m + 1) - m - 2) (2 ^ (m + 1) - m - 2 + m), (k : ℚ) / 2 ^ k := by sorry

end Erdos261
Source
Erdős Problem 261 (https://www.erdosproblems.com/261); definitions from Formal Conjectures 261.lean; Borwein–Loring, Math. Comp. 54 (1990) 377–394; Lemma A4 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