Back to Problems

erdos_197

Specification

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

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem erdos_197 :
    answer(sorry) ↔ ∃ A B : Set ℕ, IsCompl A B ∧
      (∃ f : ℕ ≃ A, ¬ HasMonotoneAP f 3) ∧
      (∃ g : ℕ ≃ B, ¬ HasMonotoneAP g 3)
ID: ErdosProblems__197__erdos_197
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.