Skip to content

Erdős problem 488

Let AA be a finite set and B={n≥1:a∣n for some a∈A}.B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}. Is it true that, for every m>n≥max⁡(A)m>n\geq \max(A), ∣B∩[1,m]∣m<2∣B∩[1,n]∣n?\frac{\lvert B\cap [1,m]\rvert }{m}< 2\frac{\lvert B\cap [1,n]\rvert}{n}?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

488.lean

Retained formal statement1 of 1

Let AA be a finite set and B={n≥1:a∣n for some a∈A}.B=\{ n \geq 1 : a\mid n\textrm{ for some }a\in A\}. Is it true that, for every m>n≥max⁡(A)m>n\geq \max(A), ∣B∩[1,m]∣m<2∣B∩[1,n]∣n?\frac{\lvert B\cap [1,m]\rvert }{m}< 2\frac{\lvert B\cap [1,n]\rvert}{n}?

FormalConjectures/ErdosProblems/488.leanErdos488.erdos_48810 linesExact file
True ↔  ∀ (A : Finset ℕ),    A.Nonempty →      0 ∉ A →        1 ∉ A →          ∀ (n m : ℕ),            m > n →              A.max ≤ ↑n →                ↑{x ∈ Finset.Icc 1 m | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑m <                  2 * ↑{x ∈ Finset.Icc 1 n | x ∈ {n | n ≥ 1 ∧ ∃ a ∈ A, a ∣ n}}.card / ↑n
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page