Erdős problem 197 · problems.science

Can $\mathbb{N}$ be partitioned into two sets, each of which can be permuted to avoid monotone 3-term arithmetic progressions?

Sources

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

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

197.lean

Retained formal statement1 of 1

Can $\mathbb{N}$ be partitioned into two sets, each of which can be permuted to avoid monotone 3-term arithmetic progressions?

FormalConjectures/ErdosProblems/197.leanErdos197.erdos_1971 lineExact file

1True ↔ ∃ A B, IsCompl A B ∧ (∃ f, ¬HasMonotoneAP (Subtype.val ∘ ⇑f) 3) ∧ ∃ g, ¬HasMonotoneAP (Subtype.val ∘ ⇑g) 3

OpenStatement only, no proof