If $π (x)$ counts the number of primes in $[1, x]$ then is it true that (for large $x$ and $y$ ) $π (x + y) \leq π (x) + π (y)?$

unreviewedOpen. Worked here; no verified result yet.

number theory · open · formalized (Lean) · 0 attempts

use this data

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

Evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This inequality is *exactly* what’s usually called the **second Hardy–Littlewood conjecture**:

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

Formal proof

AMS 11 · open (literature)

theorem erdos_855 : answer(sorry) ↔
    ∀ᶠ x in atTop, ∀ᶠ y in atTop, π (x + y) ≤ π x + π y

OEIS1

Connections2

0 \leq a_{1} < \dots < a_{k}

p

A (k) = min a_{k}

A (k)

A (k) \sim k lo g k ?

B (k) = min \frac{a _{1} + \dots + a _{k}}{k} .

Check it yourself

One command re-derives this record's receipts on your machine.

vela reproduce examples/erdos-problems

Search Vela