E251: “Is the binary series of successive primes irrational?”

Open

Statement	User	Model	Harness	Time
2)V2Every finite partial sum of the prime-weighted binary series equals four plus the corresponding binary-weight…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1The sum over n≥0 of the nth prime divided by 2^n is irrational, with nth prime indexed from 2 at n=0.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 Every finite partial sum of the prime-weighted binary series equals four plus the corresponding binary-weighted sum of consecutive prime gaps, minus one explicit endpoint term.

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

Scope. Every natural truncation N, with Mathlib zero-based nth primes and all operations in the reals.

1) V1 The sum over n≥0 of the nth prime divided by 2^n is irrational, with nth prime indexed from 2 at n=0.

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

Full-local mode. Canonical builds with narrow imports. The first two nth-prime values witness intended zero-based indexing. Independent transcription is definitionally equal both ways; direct negation remains unresolved; twelve compiling degenerate artifacts all red as restatements. Five targeted prior-art searches and a clean exact? search found no proof. The strongest whole-problem route machine-checks the finite summation-by-parts identity reducing partial sums to consecutive prime gaps; passing to the irrational infinite limit still requires unavailable quantitative control. No Commons or computational witness.

Scope. The Mathlib nth-prime sequence indexed by ℕ and its real-valued infinite binary series. This zero-based form is twice the conventional one-based series, so irrationality is equivalent.

E251:Erdős Problem #251 “Is the binary series of successive primes irrational?”

E251: “Is the binary series of successive primes irrational?”