Skip to content

Erdős problem 12

Let A⊂NA \subset \mathbb{N} be infinite with no distinct a,b,c∈Aa, b, c \in A such that a∣(b+c)a \mid (b + c) with b,c>ab, c > a. Can ∣A∩[1,N]∣/N|A \cap [1, N]|/\sqrt{N} have positive lower limit? Must every such AA fall below N1−cN^{1-c} infinitely often?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/12.lean

Formal Conjectures

FormalConjectures/ErdosProblems/12.leanErdos12.erdos_12.parts.i1 lineExact file
True ↔ ∃ A, Erdos12.IsGood A ∧ 0 < Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / √↑N) Filter.atTop
SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Reported activity

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

  • AI building on literature

    Erdős AI contributions wiki · 7 Apr, 2026

    Machine
    DeepMind prover agent
    Open the source record

  • AI collaborating with humans

    Erdős AI contributions wiki · 7 Apr, 2026

    Machine
    GPT-5.4 Thinking
    People
    Nat Sothanaphan, Terence Tao
    Open the source record

  • argument

    VibeMathed

    Machine
    AlphaProof Nexus
    Reported outcome
    partial
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page