Combinatorics

Erdős 196

Must every permutation of

\mathbb{N}

, contain a monotone 4-term arithmetic progression?

References

erdosproblems.com/196

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ (f : ℕ ≃ ℕ), HasMonotoneAP (⇑f) 4

What you must prove

import FormalConjectures.ErdosProblems.«196»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos196.erdos_196" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/196.lean

Source type SHA-256: sha256:1969cd67b2bc2d369d8a90a88c2aec507b2944165032da740c678331c519e620
Task id: fc-379fc029-erdos196-erdos-196-abf59cd01e-formalized-v1
Task commitment: sha256:715b41ddfb19f6acc1ec21a9ce61b683f2da1753c6dfe3f2c626b4b791348ce5

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.