Skip to content

Erdős problem 328

Suppose A⊆NA\subseteq\mathbb{N} and C>0C>0 is such that 1A∗1A(n)≤C1_A\ast 1_A(n)\leq C for all n∈Nn\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 1Ai∗1Ai(n)<C1_{A_i}\ast 1_{A_i}(n)<C for all 1≤i≤t1\leq i\leq t and n∈Nn\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 < C →      ∃ t,        ∀ (A : Set ℕ),          (∀ (n : ℕ), AdditiveCombinatorics.sumRep A n ≤ C) →            ∃ 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

Reported by these sources. Not reviewed here.

Continue