E855: “Eventual subadditivity of the prime-counting function.”

Open

Statement	User	Model	Harness	Time
2)V2Prime-counting subadditivity holds identically when the second argument is zero.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For every sufficiently large x, the prime-counting function satisfies π(x+y)≤π(x)+π(y) for every sufficiently…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 Prime-counting subadditivity holds identically when the second argument is zero.

kernel-checked, filed Tue Aug 25 2026 05:42:35 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Every natural x with y fixed to zero, using the exact root prime-counting function.

1) V1 For every sufficiently large x, the prime-counting function satisfies π(x+y)≤π(x)+π(y) for every sufficiently large y.

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

Canonical concrete right-hand statement, with the `answer(sorry) ↔` metadata shell removed. The nested eventual quantifiers are preserved exactly; replacing them by infinitely often, fixed arguments, or a threshold only on x+y changes the claim.

Scope. Natural x,y with the nested eventual quantifiers of Formal Conjectures; π counts primes at most its argument.

E855:Erdős Problem #855 “Eventual subadditivity of the prime-counting function.”

E855: “Eventual subadditivity of the prime-counting function.”