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?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

178.lean

Retained formal statement1 of 1

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?

Erdős remarks 'it seems certain that the answer is affirmative'. This was solved by Beck [Be81]. Recently Beck [Be17] proved that one can replace d1\ll_d 1 with d4+ϵ\ll d^{4+\epsilon} for any ϵ>0\epsilon>0.

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.

Search problems.science

Find a Problem, Result, source, or page