OpenAI claim summary for Math-164

Order of Magnitude of the Largest Three-Term-Progression-Free Sets

OpenAI's claim

Progression-free density and reciprocal sums: For each fixed length $k\ge3$, the claimed progression-free density decays as $\exp(-c_k(\log N)^{\varepsilon_k})$ up to a fixed factor. This quantitative estimate is used to deduce arbitrarily long progressions from a divergent reciprocal sum.

Mathematical statement of the claimed result

Mathematical claim 1.

For each fixed integer $k\ge3$, let $r_k(N)$ denote maximal cardinality among subsets of $\{1,\ldots,N\}$ containing no arithmetic progression $a,a+d,\ldots,a+(k-1)d$ with $d\ne0$. The claim gives constants $C_k,c_k,\epsilon_k>0$ with \[r_k(N)\le C_kN\exp\{-c_k(\log N)^{\epsilon_k}\}\quad(N\ge2).\] Its divergent-reciprocal-sums corollary asserts \[A\subset\mathbb N,\ \sum_{a\in A}a^{-1}=\infty\quad\Longrightarrow\quad A\text{ contains a nonconstant progression of every finite length}.\] This concerns sets of distinct positive integers. It does not settle a separate finite-field progression clause.

Outline of the argument

Progression-free density and reciprocal sums: Density increments take place inside triangular polynomial cells rather than repeatedly discarding inherited structure. Integer coordinate blocks and exact substitution retain old constraints when new ones are added. A hierarchy of precision costs bounds the total logarithmic length loss by a polynomial in the logarithmic density parameter, enabling the quasipolynomial estimate and the reciprocal-sum consequence.

Formal verification

Family 159 describes Lean coverage for the divergent-reciprocal-sum progression consequence; the quantitative progression-free density bound is not selected.

Progression-free density and reciprocal sums: The manuscript links ErdosReciprocal.lean.

The documented selection does not cover the entire manuscript assertion relevant here.

This site has not run the Lean development. These links describe OpenAI’s selected formal statements and should be read with their stated scope.

Status caveat

OpenAI reports that an internal model produced the manuscripts. Their arguments have not been independently verified as proofs by this site. Any portion outside the documented formal scope may contain mistakes, and the catalogue label reports the announced mathematical claim.

Sources

• OpenAI, Quasipolynomial Bounds for Arithmetic Progressions, 2026-09-23; citation key OAI:Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026. PDF (GitHub); PDF (direct); Manuscript page and citation; Latest version; Statement source: ap:main; Statement source: ap:reciprocal.
• Family 159: Lean scope.
• Comparator ErdosReciprocal.json.
• Comparator ErdosReciprocal.lean.
• Family 159: Reasoning summary.
• OpenAI catalogue entry.