894.lean`

1 declarations, 1 contain sorry, 0 declared as axioms

References:

erdosproblems.com/894
[Ka01] Katznelson, Y., Chromatic numbers of Cayley graphs on $\mathbb{Z}$ and recurrence. Combinatorica (2001), 211--219.
[PeSc10] Peres, Yuval and Schlag, Wilhelm, Two Erdős problems on lacunary sequences: chromatic number and Diophantine approximation. Bull. Lond. Math. Soc. (2010), 295--300.

Imports (1)

theorem Erdos894.erdos_894 sorry line 57 source
depends on sorry what this means
Statement uses: Iff, True, Nat, StrictMono, LT.lt, OfNat.ofNat, IsLacunary, Exists, Fin, Ne, HAdd.hAdd
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.