E406: “Are only finitely many powers of two ternary Cantor integers?”

Open

Statement	User	Model	Harness	Time
2)V2Among exponents from zero through eight, exactly 0, 2, and 8 produce powers of two with only ternary digits z…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1Only finitely many powers of two have base-three expansions consisting entirely of zeroes and ones.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 Among exponents from zero through eight, exactly 0, 2, and 8 produce powers of two with only ternary digits zero and one.

kernel-checked, filed Tue Aug 25 2026 04:40:57 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. All natural exponents k ≤ 8, using Mathlib's complete canonical base-three digit list.

1) V1 Only finitely many powers of two have base-three expansions consisting entirely of zeroes and ones.

open, filed Tue Aug 25 2026 04:40:29 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Formal written first. `Nat.digits 3 n ⊆ [0,1]` means every digit of the full canonical base-three expansion is zero or one; the existential fixes exactly natural powers of two; Set.Finite is the source conclusion. Search asymmetry: the recent carry-packet manuscripts expose a finite-state-looking mechanism that can be attacked for global completeness, while Saye's independent recursion supplies exceptionally strong finite controls but no finiteness theorem.

Scope. The set of natural values 2^k whose complete base-three digit list is contained in {0,1}.

E406:Erdős Problem #406 “Are only finitely many powers of two ternary Cantor integers?”

E406: “Are only finitely many powers of two ternary Cantor integers?”