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?

Sources

The source's own material, retained exactly.

10 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

12.lean

Retained formal statement2 of 9

Let AA be an infinite set such that there are no distinct a,b,c∈Aa,b,c \in A such that a∣(b+c)a \mid (b+c) and b,c>ab,c > a. Does there exist some absolute constant c>0c > 0 such that there are always infinitely many NN with ∣A∩{1,…,N}∣<N1−c|A \cap \{1, \dotsc, N\}| < N^{1−c}?

The DeepMind prover agent has found a formal disproof of this statement.

FormalConjectures/ErdosProblems/12.leanErdos12.erdos_12.parts.ii1 lineExact file
False ↔ ∃ c > 0, ∀ (A : Set ℕ), Erdos12.IsGood A → {N | ↑(A ∩ Set.Icc 1 N).ncard < ↑N ^ (1 - c)}.Infinite
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.