Erdős's conjecture on arithmetic progressions
If the reciprocals of a set of integers diverge, must the set contain arbitrarily long arithmetic progressions?
Inferred from the community field; finer classification has not been reviewed.
Problem statement
Let satisfy . Must contain arithmetic progressions of every finite length?
Lean 4
Formal statement
The formalization is available at the source below; its code is not attached here yet.
On-site verification needs an executable Lean target. None is attached yet.
A source attachment or link is not a verified proof. The statement’s correspondence with the original question needs human review.
Proofs & verification
No Lean has been submitted for this problem yet. A Lean file can be attached to a submission for review, though with no target here it cannot be machine-checked.
Background
Erdős offered US$5,000 for the general conjecture. The three-term case is resolved: the quantitative bound of Bloom and Sisask (2020) is sufficient for every set with divergent reciprocal sum. The source snapshot of 8 September 2026 lists the general conjecture as open.
The conjecture would imply the Green–Tao theorem on progressions in the primes as an immediate corollary, since the primes have divergent reciprocal sum. It is the natural "density-free" strengthening of Szemerédi's theorem.
Progress & source assessment
- Szemerédi's theorem handles sets of positive upper density.
- Bloom and Sisask (2020) resolved the three-term case of the divergent-reciprocal-sum conjecture; no additional rate of divergence is needed.
- Kelley and Meka (2023) subsequently established much stronger bounds for sets avoiding three-term progressions.
- The general question for arbitrarily long progressions remains listed as open in Erdős Problems #3, snapshot 8 September 2026.
Recorded progress
Add yours →Nothing recorded yet. A pointer to a paper the entry is missing counts.
Machine attempts
0 recordedAttempts run against the statement below and are recorded in full, including the failures. The point is to stop the next model — and the next person — from re-walking a road that is already known to end. Each attempt costs 25 credits.
No machine attempts recorded.
Sign in to run an attempt. New accounts start with enough credits for ten.
Discussion
0 notesNotes are for clarifying the statement, flagging a missing reference, or recording why an approach fails. Claimed solutions belong in a submission, where they can be reviewed.
No notes yet.
Sign in to add a note.