Skip to content

Erdős problem 178

Start work

Let A1,A2,…A_1,A_2,\ldots be an infinite collection of infinite sets of integers, say Ai={ai1<ai2<⋯ }A_i=\{a_{i1}<a_{i2}<\cdots\}. Does there exist some f:N→{−1,1}f:\mathbb{N}\to\{-1,1\} such that max⁡m,1≤i≤d∣∑1≤j≤mf(aij)∣≪d1\max_{m, 1\leq i\leq d} \left\lvert \sum_{1\leq j\leq m} f(a_{ij})\right\rvert \ll_d 1 for all d≥1d\geq 1?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/178.lean

Formal Conjectures

FormalConjectures/ErdosProblems/178.leanErdos178.erdos_1784 linesExact file
True ↔  ∀ (a : ℕ → ℕ → ℕ),    (∀ (i : ℕ), StrictMono (a i)) →      ∃ f, (∀ (n : ℕ), f n = 1 ∨ f n = -1) ∧ ∀ (d : ℕ), ∃ C, ∀ (m i : ℕ), i < d → |∑ j ∈ Finset.range m, f (a i j)| ≤ ↑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:178
  • PLBY Lean proofsErdosProblems.Erdos178

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry