Skip to content

Erdős problem 951

If 1 < a 0 < ... has property Erdos951Prop, is it true that #{a i ≤ x} ≤ π x?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/951.lean

Formal Conjectures

FormalConjectures/ErdosProblems/951.leanErdos951.erdos_9514 linesExact file
sorry  ∀ (a : ℕ → ℝ),    1 < a 0 →      StrictMono aErdos951.Erdos951Prop a → ∀ᶠ (x : ℝ) in Filter.atTop, {i | a ix}.ncard ≤ ⌊x⌋₊.primeCounting
OpenStatement only, no proof

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • AI standalone

    Erdős AI contributions wiki · 27 Jan, 2026

    Machine
    GPT-5.2 Pro
    Open the source record
  • AI building on literature

    Erdős AI contributions wiki · 28 Jan, 2026

    Machine
    AlphaEvolve
    Open the source record
  • AI collaborating with humans

    Erdős AI contributions wiki · 28 Jan, 2026

    Machine
    GPT-5.2 Thinking
    People
    Nat Sothanaphan
    Open the source record

Continue

Search problems.science

Find a Problem, Result, source, or page