erdős #197
Can be partitioned into two sets, each of which can be permuted to avoid monotone 3-term arithmetic progressions?
Worked, still open.
arithmetic progressions · open · formalized (Lean) · 0 attempts
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
### What “avoid a monotone 3‑term A.P.” means
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 5 · open (literature)
theorem erdos_197 :
answer(sorry) ↔ ∃ A B : Set ℕ, IsCompl A B ∧
(∃ f : ℕ ≃ A, ¬HasMonotoneAP (Subtype.val ∘ f) 3) ∧
(∃ g : ℕ ≃ B, ¬HasMonotoneAP (Subtype.val ∘ g) 3)formal-conjectures/197.lean ↗status
open