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}?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/488.lean

Formal Conjectures

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

Reported activity

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

  • AI building on literature

    Erdős AI contributions wiki · 27 Nov, 2025

    Machine
    Aristotle
    Open the source record

  • AI collaborating with humans

    Erdős AI contributions wiki · 20 Mar, 2026

    Machine
    Aristotle, GPT-5.4
    People
    Przemek Chojecki
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page