The equation $r(2^{t+1}-1)=2^{j+1}+t-1$ has no solutions with $t\ge1$

Proved

Erdos261.no_second_phase_dioph

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

erdos-problemsnumber-theory

Theorem. For all integers $j,r\ge0$ and $t\ge1$ ,

r\,(2^{t+1}-1)\ne 2^{j+1}+t-1.

With $M=2^{t+1}-1$ one has $2^{j+1}\equiv 2^e\pmod M$ for $e=(j+1)\bmod (t+1)\le t$ , and $1\le 2^e+t-1<M$ , so $M\nmid 2^{j+1}+t-1$ . In Erdős Problem 261 this equation describes greedy termination right after the first doubling phase (see no_two_phase_termination).

Preamble

import Mathlib
import Definitions.Def_Erdos261_defs
open Finset

Formal statement

namespace Erdos261

theorem no_second_phase_dioph (j r t : ℕ) (ht : 1 ≤ t) : r * (2 ^ (t + 1) - 1) ≠ 2 ^ (j + 1) + t - 1 := by sorry

end Erdos261

Source

Erdős Problem 261 (https://www.erdosproblems.com/261); greedy carry as in Borwein–Loring 1990 / Tengely–Ulas–Zygadło 2020 (platform def Def_Erdos261_defs); Claim A2 of claim from GPT 6.1 Sol (second answer, Oct 23 2026), Lean-verified by Grok Bot for Ethan Cheung (Oct 23 2026)

View graph

The equation r(2t+1−1)=2j+1+t−1r(2^{t+1}-1)=2^{j+1}+t-1r(2t+1−1)=2j+1+t−1 has no solutions with t≥1t\ge1t≥1

The equation $r(2^{t+1}-1)=2^{j+1}+t-1$ has no solutions with $t\ge1$