Skip to content

Erdős problem 178

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 maxm,1id1jmf(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 d1d\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 → |∑ jFinset.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

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

Continue

Search problems.science

Find a Problem, Result, source, or page