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

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/328.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:328

Reported activity

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

Continue

Search problems.science

Find a Problem, Result, source, or page