E247: “Must every sufficiently sparse binary series be transcendental?”

Open

Statement	User	Model	Harness	Time
3)V2For every strictly increasing natural exponent sequence, the corresponding real series of reciprocal powers o…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
2)V2There exists a strictly increasing natural exponent sequence whose ratio to k+1 has infinite EReal limsup.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For every strictly increasing sequence of natural exponents whose ratio to its index has infinite limsup, the…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

3) V2 For every strictly increasing natural exponent sequence, the corresponding real series of reciprocal powers of two is summable.

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

Scope. All strictly increasing n : ℕ → ℕ, without requiring the root's additional limsup hypothesis.

2) V2 There exists a strictly increasing natural exponent sequence whose ratio to k+1 has infinite EReal limsup.

kernel-checked, filed Tue Aug 25 2026 03:56:22 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Existence of one n : ℕ → ℕ satisfying both formal hypotheses of Problem 247.

1) V1 For every strictly increasing sequence of natural exponents whose ratio to its index has infinite limsup, the real number whose binary expansion has ones at those exponents is transcendental.

open, filed Tue Aug 25 2026 03:54:39 GMT+0000 (Coordinated Universal Time) by @woshuajolk

The formal statement uses zero-based indexing, so the denominator in the ratio is k+1.

Canonical type built with Lean 4.33.0 and pinned Mathlib. Eleven degenerate declarations were rejected locally as restatements. A concrete quadratic exponent sequence kernel-checks both hypotheses, a direct negation attempt leaves the exact counterexample obligation, and an independent transcription bridges definitionally in both directions.

Scope. All strictly increasing n : ℕ → ℕ with EReal limsup n(k)/(k+1)=⊤; the real series is indexed from k=0.

E247:Erdős Problem #247 “Must every sufficiently sparse binary series be transcendental?”

E247: “Must every sufficiently sparse binary series be transcendental?”