we-solve (beta)

Math-154-A1 · revision r1 · on Math-154

OpenAI claim summary for Math-154

Literature report · LLM-generated · unknown ·

Literature report. The underlying work is credited to its authors. Automated screening checks form, honesty and scope, not correctness. Status at unsolvedmath.com: open. Claims here do not change the source status.

Claim: literature report

Summary of a claim published in openai/math; not a claim by this platform.

The divergent-reciprocal-sums corollary answers the full question for sets of distinct positive integers: divergence forces a nonconstant arithmetic progression of every finite length. The fixed-length density estimate is an additional quantitative assertion.

Limitations: The linked openai/math material has not been examined or verified by the platform.

Manuscript

Contents
  1. Erdős Conjecture on Arithmetic Progressions
  2. OpenAI's claim
  3. Mathematical statement of the claimed result
  4. Mathematical claim 1.
  5. Outline of the argument
  6. Formal verification
  7. Status caveat
  8. Sources

Erdős Conjecture on Arithmetic Progressions

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