Erdős’s reciprocal-sum conjecture and quasipolynomial Szemerédi bounds

1 paperLeanreasoning

Proves Erdős's conjecture that every set of positive integers with divergent reciprocal sum contains arithmetic progressions of every finite length. Quantitatively, for each fixed k ≥ 3, every subset of \(\{1,\ldots,N\}\) with no nonconstant k-term progression has size at most \(C_kN\exp[-c_k(\log N)^{\varepsilon_k}]\), with positive constants depending only on k.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 1

Quasipolynomial Bounds for Arithmetic Progressions

OpenAI · September 23, 2026

We prove Erdős's conjecture that every set of positive integers with divergent reciprocal sum contains arithmetic progressions of every finite length. More quantitatively, for every fixed k ≥ 3, we show \(\displaystyle r_k(N)\le C_kN\exp\bigl(-c_k(\log N)^{\varepsilon_k}\bigr)\) with \(C_k,c_k,\varepsilon_k\gt 0\), where \(r_k(N)\) is the largest size of a subset of \(\{1,\ldots,N\}\) with no nonconstant k-term arithmetic progression.

Read PDF Download Source

Cite

@misc{OAI:Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026,
  author = {{OpenAI}},
  title = {{Quasipolynomial Bounds for Arithmetic Progressions}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026/paper.pdf}{OAI:Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Quasipolynomial Bounds for Arithmetic Progressions

Scope

Erdős's reciprocal-sum conjecture asks whether every set of positive integers with divergent reciprocal sum contains arithmetic progressions of every finite length. The formalization proves this statement: for every requested length, such a set contains a progression with positive common difference.

The selected theorem is the reciprocal-sum consequence. The paper's quantitative upper bound for the largest progression-free subset of \(\{1,\ldots,N\}\) is outside this statement.

Comparator links

Result	Comparator statement
Erdős's reciprocal-sum arithmetic-progression conjecture	ErdosReciprocal.lean

Scope note on GitHub →

Reasoning summary

OpenAI released an abridged summary of the model's reasoning for this result: Quasipolynomial bounds for arithmetic progressions (PDF).