Skip to content

Erdős problem 951

Start work

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

Sources

The source's own material, retained exactly.

3 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

951.lean

Retained formal statement1 of 3

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

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