Conjectures.io

Combinatorics

Green15.green_15

Does there exist a Lipschitz function f:N→Zf : \mathbb{N} \to \mathbb{Z} whose graph Γ={(n,f(n)):n∈N}⊆Z2\Gamma = \{(n, f(n)) : n \in \mathbb{N}\} \subseteq \mathbb{Z}^2 is free of 3-term progressions?

References

  • [BJP14] T. Brown, V. Jungić and A. Poelstra, "On double 3-term arithmetic progressions", Integers 14 (2014), Paper No. A43.
  • [CCS14] J. Cassaigne, J. D. Currie, L. Schaeffer and J. Shallit, "Avoidance of additive cubes and related results", Adv. in Appl. Math. 56 (2014), 25–66.

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∃ K f, LipschitzWith K f ∧ {x | ∃ n, (↑n, f n) = x}.IsAPOfLengthFree 3

What you must prove

import FormalConjectures.GreensOpenProblems.«15»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Green15.green_15" := by
  sorry

end Bounty

Pinned source: FormalConjectures/GreensOpenProblems/15.lean

Source type SHA-256
sha256:e8499f839608d37b026c975a89730544b39d77ba20964d5b93c766d914eaf019
Task id
fc-379fc029-green15-green-15-3c2ad99b82-formalized-v1
Task commitment
sha256:dc20224737542a57d1a483bbe43fa077bdcb026435529b13f0eaa854983e6fba

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.