Erdős problem 785 · problems.science

Let $A,B\subseteq \mathbb{N}$ be infinite sets such that $A+B$ contains all large integers. Let $A(x)=\lvert A\cap [1,x]\rvert$ and similarly for $B(x)$ . Is it true that if $A(x)B(x)\sim x$ then $A(x)B(x)-x\to \infty$ as $x\to \infty$ ?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/785.lean

Formal Conjectures

FormalConjectures/ErdosProblems/785.leanErdos785.erdos_7856 linesExact file

1True ↔2  ∀ (A B : Set ℕ),3    A.Infinite →4      B.Infinite →5        Erdos785.IsExactAdditiveComplement A B →6          Filter.Tendsto (fun x => ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) Filter.atTop Filter.atTop

SolvedStatement only, no proof

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:785
PLBY Lean proofsErdosProblems.Erdos785

Reported activity

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

Formalization
Erdős AI contributions wiki · 6 Mar, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science