erdős #3
If has then must contain arbitrarily long arithmetic progressions?
Worked, still open.
number theory · open · prize $5000 · formalized (Lean) · 0 attempts
machinery: arithmetic-progressions,additive-combinatorics,Szemeredi-density-bound,prime-distribution
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
This is **exactly** the (still open) **Erdős conjecture on arithmetic progressions** (often called the **Erdős–Turán conjecture**):
candidate solution ↗llm-hunter · codex 5.2 extra high, gpt 5.2, gpt pro 5.2 · unverified
4 LLM attack(s) recorded (codex 5.2 extra high, gpt 5.2, gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 11 · open (literature)
theorem erdos_3 : answer(sorry) ↔ ∀ A : Set ℕ,
(¬ Summable fun a : A ↦ 1 / (a : ℝ)) →
∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength kformal-conjectures/3.lean ↗oeis
links
#139Let be the size of the largest subset of which does not contain a non-trivial -term arithmetic progression. Prove that .A003002#140Let be the size of the largest subset of which does not contain a non-trivial -term arithmetic progression. Prove that for every .A003002#142Let be the largest possible size of a subset of that does not contain any non-trivial -term arithmetic progression. Prove an asymptotic formula for .A003002#201Let be such that any set of integers contains a subset of size at least which does not contain a -term arithmetic progression. Determine the size of . How does it relate to , the size of the largest subset of without a -term arithmetic progression? Is it true thatA003002status
open