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 statement2 of 3

Beurling conjectured that if the number of Beurling integer in [1, x] is x + o(log x), then a must be the sequence of primes.

FormalConjectures/ErdosProblems/951.leanErdos951.erdos_951.variants.beurling3 linesExact file
∀ (a : ℕ → ℝ),  IsBeurlingPrimes a →    (fun x => ↑(BeurlingIntegers a ∩ Set.Iic x).ncard - x) =o[Filter.atTop] Real.log → a = Nat.cast ∘ Nat.nth Nat.Prime
SolvedStatement only, no proof