Skip to content

Erdős problem 328

Suppose ANA\subseteq\mathbb{N} and C>0C>0 is such that 1A1A(n)C1_A\ast 1_A(n)\leq C for all nNn\in\mathbb{N}. Can AA be partitioned into tt many subsets A1,,AtA_1,\ldots,A_t (where t=t(C)t=t(C) depends only on CC) such that 1Ai1Ai(n)<C1_{A_i}\ast 1_{A_i}(n)<C for all 1it1\leq i\leq t and nNn\in \mathbb{N}?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

328.lean

Retained formal statement1 of 1

Suppose ANA\subseteq\mathbb{N} and C>0C>0 is such that 1A1A(n)C1_A\ast 1_A(n)\leq C for all nNn\in\mathbb{N}. Can AA be partitioned into tt many subsets A1,,AtA_1,\ldots,A_t (where t=t(C)t=t(C) depends only on CC) such that 1Ai1Ai(n)<C1_{A_i}\ast 1_{A_i}(n)<C for all 1it1\leq i\leq t and nNn\in \mathbb{N}?

The answer is no. Asked by Erdős and Newman. Nešetřil and Rödl [NeRo85] have shown the answer is no for all CC (even if tt is also allowed to depend on AA).

Erdős [Er80e] had previously shown the answer is no for C=3,4C=3,4 and infinitely many other values of CC.

See also [774].

The linked proof writes the representation function as Set.ncard {p : ℕ × ℕ | p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n}, which counts the same ordered pairs as sumRep, and states the partition condition as a named definition with the same two conjuncts used below. Its ∃ t additionally carries 1 ≤ t, which costs nothing: t = 0 forces A = ∅, and A = {1} has all representation counts at most C for C ≥ 1.

FormalConjectures/ErdosProblems/328.leanErdos328.erdos_3289 linesExact file
False  ∀ (C : ℕ),    0 < Ct,        ∀ (A : Set ℕ),          (∀ (n : ℕ), AdditiveCombinatorics.sumRep A nC) →P,i, P i = A                Set.univ.PairwiseDisjoint P ∧ ∀ (i : Fin t) (n : ℕ), AdditiveCombinatorics.sumRep (P i) n < C
SolvedProof has a holelean4external proof

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

Search problems.science

Find a Problem, Result, source, or page