Let $1 < a_{1} < \dots$ be a sequence of real numbers such that $i \prod a_{i}^{k_{i}} - j \prod a_{j}^{ℓ_{j}} \geq 1$ for every distinct pair of non-negative finitely supported integer tuples $k_{i}, ℓ_{j} \geq 0$ . Is it true that $# {a_{i} \leq x} \leq π (x)?$

Worked, still open.

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

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

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

With the hypothesis as stated **for arbitrary real** (a_i>1), this is (as far as is currently recorded in the literature) **open**.

llm-hunter · gpt pro 5.2 · unverified

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

AMS 11 · api (literature)

theorem erdos_951.variants.isBeurlingPrimes {a : ℕ → ℝ} (ha : 1 < a 0)
    (hm : StrictMono a) (he : Erdos951Prop a) :
    IsBeurlingPrimes a

open