Erdős problem 197

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

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