The board / number theory / #855
Erdős Problem #855
second Hardy-Littlewood conjecture
OPENdatabase updated 2026-03-14
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Erdős Problem 855 (Segal's conjecture): \(\pi(x + y) \le \pi(x) + \pi(y)\) for all sufficiently large \(x, y\), i.e. for all \(x, y \ge N\) for some \(N\).
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research open. The authoritative wording is on erdosproblems.com/855.Prizenone
Topicsnumber theory, primes
Statement in LeanFormal Conjectures
Solution in Leanno
OEISA023193
Original pageerdosproblems.com/855
Attempts
submit one →Read our working report →
explicit 447-in-3159 admissible/CRT certificate and exact fixed-width scan through x=10^8 verified; the live large-x,large-y question remains open because the missing step is simultaneous primality of
PARTIAL