Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Openai 2026 quasipolynomial bounds arithmetic progressions
corollary_11_2: The claimed uniform bound H_k on the reciprocal sum of every set of positive integers with no k-term progression, with H_k the dyadic sum of r_k(2^m)/2^m; the finiteness of f(k) in Problem 169, without a numerical estimate.
corollary_1_2: The claimed resolution of Erdős's reciprocal-sum conjecture (Problem 3): every set of positive integers with divergent reciprocal sum contains nonconstant arithmetic progressions of every finite length, deduced from Theorem 1.1 by summing the density bound over dyadic blocks.
theorem_1_1: The claimed stretched-exponential density bound for k-term-progression-free subsets of the first N integers, for every fixed k, which the manuscript proves by iterating a density increment on triangular polynomial cells; the quantitative source of its claimed resolution of Problem 3.
OpenAI, Quasipolynomial Bounds for Arithmetic Progressions, OpenAI Math
Release preprint, September 23, 2026. Released under the Apache License 2.0 at
https://github.com/openai/math (revision adc7f1241), folder
preprints/Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026;
the held PDF, paper.pdf in the release, is retained as
openai_2026_quasipolynomial_bounds_arithmetic_progressions.pdf,
and the release's TeX bundle in the same folder is the TeX source cited below.
@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}
}Attestation as the release states it. The release README says its manuscripts were "produced by an internal OpenAI model", that the collection "includes results at different stages of verification", that not all of them have Lean formalizations, and that "Some of the unformalized results could have issues". The manuscript's own README carries only the title, author, date and citation block and adds no statement about human assistance. The manuscript is a 198-page PDF with no author names beyond "OpenAI", no arXiv identifier and no journal. The release includes a reasoning summary for this manuscript's family; that file is not held here. These are the source's own provenance attestations, recorded as history, not as this corpus's review. No refereed publication, arXiv version or independent review of the manuscript is recorded here and nothing on this card is independently reviewed.
Formalization, as the release lists it. The release's catalog
lean/formalization.yaml does not name this manuscript. Its family page
nevertheless states that the reciprocal-sum consequence is formalized ("for
every requested length, such a set contains a progression with positive common
difference") and that the quantitative bound on the largest progression-free
subset of "is outside this statement"; it names the comparator
statement file lean/ComparatorChallenges/ErdosReciprocal.lean, which states
the reciprocal-sum theorem with its proof left open as a challenge, and whose
companion JSON points at the solution module
OAI.Combinatorics.Progressions.Main. The release tree holds that library under
lean/OAI/Combinatorics/Progressions/, about 4,770 files, whose
Results/Conclusions.lean declares a theorem for the reciprocal-sum statement
and one for a quantitative density statement; the density statement, as the
library's Model.lean defines it, is the saving
for each fixed , a weaker form than
Theorem 1.1's
, though still one that gives dyadic
summability. The corpus's verification built
OAI.Erdos3.manuscriptReciprocalProgressionTheorem at the pinned revision and
checked its axioms (propext, Classical.choice and Quot.sound only); the
record is kept on the claim page of
Problem 3. The
release's other declarations were read statically and not built here. A Lean
file is a formal statement about the release's own definitions, not a proof of
the Erdős problem.
Companions. The release lists no other manuscript in the same family. The manuscript itself cites the release's Quantitative Superexponential Bounds for van der Waerden Numbers (card) as the companion supplying the lower bound for , , complementary to its own coloring threshold in Section 1.4.
Read status: claims checked for Theorem 1.1, Corollary 1.2, Theorem 2.1,
Lemma 2.2, Proposition 10.4, Proposition 11.1 and Corollaries 11.2--11.5,
read clause by clause in the TeX source (sections/00-introduction.tex lines
13--36, sections/01-setup.tex lines 97--124 and 192--203,
sections/08-iteration.tex lines 360--367, sections/09-consequences.tex
in full) on 2026-10-07; the statements of the remaining section-level results
(Theorem 3.4, Propositions 4.1, 6.2, 7.4, 7.8 and 9.1, Corollary 7.9,
Theorem 8.2, and the appendix results the interface table names)
were read as statements only; the proofs were read for their structure only
and no step was checked; nothing here is independently reviewed.
Contents
- Section 1, Introduction (pp. 4--8). Defines as the maximum cardinality of a set free of -term progressions, only nonconstant ones (common difference ) counting, with natural logarithms, and cites Erdős's question as Problem 4.33.6 of his 1974 Math. Balkanica problem list. Theorem 1.1 (p. 4): for each fixed there are with for every , equivalently a threshold forcing a progression in every -dense subset. The constants depend on and "the exponent is not optimized". Corollary 1.2 (p. 4): every with divergent reciprocal sum contains nonconstant progressions of every finite length; its half-page proof sums the density bound over dyadic blocks. Section 1.1 notes that alone does not settle the question and that the proof uses . Section 1.2 surveys prior bounds (Roth, Heath-Brown, Szemerédi, Bourgain, Sanders, Bloom, Bloom--Sisask, Kelley--Meka, Raghavan for three terms; Gowers, Green--Tao, Leng--Sah--Sawhney for longer ones) and states that the contribution is the all-length summable bound, with "no improvement of the three-term exponent" (p. 6) claimed. Section 1.3 explains the method: density increments on triangular polynomial cells whose integer blocks are determined successively by polynomial constraints of weighted degree at most and width , with the key requirement that one increment's extra precision loss at weight be polynomially bounded in terms of the dimensions, the log-density parameter and the precisions of the weights above alone, never itself or the precisions below it. Section 1.4 derives the coloring threshold , display (1.3), and pairs it with the companion paper's lower bound. Section 1.5 is a reading guide.
- Section 2, Polynomial cells and the increment theorem (pp. 8--13). Fixes , defines precision budgets and , triangular cells, the two-box density certificate (display (2.2)) and width logs . Theorem 2.1 (Triangular increment, p. 10): for and a certificate at threshold for a progression-free input on a box with sufficiently long root sides, either the hypotheses cannot all hold or some root slice supports a new certificate at threshold , with at most fresh absolute slots plus downward preparation copies, and dimension and width recurrences (2.3), (2.4) whose right sides omit and lower widths. Defines polynomial patches and their rank, and states Lemma 2.2 (Dimension-independent fresh rank, p. 11): for , a progression-free -valued function of mean at least on a box of any dimension with sufficiently large sides admits, unless the hypotheses are impossible, a degree- patch on a slice with positive score at target and at most slots, independent of ; its proof is a paragraph assembling the appendix results. Definition 2.3 fixes the warm, cold-preliminary and late budget vocabulary; Section 2.8 and Figure 3 (p. 14) give the route: preparation, forward sampling, absolute increment, return, extraction, iteration.
- Section 3, Constrained paths and their detection estimates (pp. 14--23). Constructs, at one layer, a probability law on integer-affine maps that pull the current polynomial back to an exact integer-polynomial lift plus a small polynomial residual, and states Theorem 3.4 (Pathwise detection and approximation) with a cold clause and a warm clause (the latter not charging or the height of the value space). Defines the stopped tree of a cell.
- Section 4, Preparing a cell by rank cuts (pp. 24--35). Proposition 4.1 (Prepared system with triangular costs): after polynomially many rank-cut transactions, every rank-stop probability is below its bound, the old integer tuple is retained, and the width loss at a block depends on its own width only additively. Recovery estimates, the sharpened major statement, transfer of a failed relation through earlier layers, termination.
- Section 5, Detection independent of the current width (pp. 36--39). Proves the warm clause of the detection theorem with a pseudorandom chart weight and a cube form of the densification of Conlon, Fox and Zhao (their Sections 6.2--6.3), so that the inverse theorem is applied to bounded conditional averages rather than to sparse factors.
- Section 6, Forward sampling of a prepared cell (pp. 40--43). Proposition 6.2 (Forward mass): a prepared certificate at threshold yields terminal paths whose expected input mean is at least , with at least a fraction of paths at mean at least , without charging the inverse of the certificate's excess.
- Sections 7 and 8, Returning the increment (pp. 44--68). Section 7 sets up paired cutoffs, the comparison measure and Proposition 7.4 (Scalar comparison), then the group representation with exact marked projection , degree reduction, and the passive layers (Proposition 7.8, Passive micro replacement; Corollary 7.9, Passive scalar return). Section 8 treats the active layers through Theorem 8.2 (Active replacement), by induction on degree with injective top projection, exact factors over one site and degree reduction, keeping the old determining identity exact.
- Section 9, Parameter extraction and exact restoration (pp. 69--75). Proposition 9.1 (One-layer extraction): the returned surplus becomes a pair of cutoff boxes adding the current raw block to the determining system, with inherited polynomials restored exactly and bounded by warm data; flags removed, inactive equations solved over the integers, real pivots, elimination of the active modulus, freezing, localization.
- Section 10, Triangular iteration (pp. 76--82). Lemma 10.1 (Root compression), Proposition 10.2 (Triangular dimension bounds, with , ), the four-step numerical schedule, Proposition 10.3 (Triangular width bounds, recurrence (10.2)), the completion of the proof of Theorem 2.1, Proposition 10.4 (Finite-horizon closure): a progression-free subset of of density cannot have , proved by rounds with until the target reaches one. The proof of Theorem 1.1 (pp. 81--82) inverts this, checks the threshold form at its endpoints and derives the coloring bound.
- Section 11, Weighted consequences (pp. 82--84). Proposition 11.1 (Dyadic weighted summation): $\sum_{a\in A}w(a)\le S_k(w)=\sum_m r_k(2^m)\max_{2^m\le n<2^{m+1}}w(n)$ for progression-free . Corollary 11.2 (Uniform harmonic bound): . Corollary 11.3: bounded sums for the weights , , and . Corollary 11.4: divergence of over forces progressions of every length, for every fixed ; a remark records for every fixed . An unnumbered paragraph recovers the Green--Tao dense-primes theorem (their Theorem 1.2) from the case and the prime number theorem. Corollary 11.5 (Harmonic tails): $\sum_{a\in A,a>x}1/a\le C'_k(\log x)^{1-\varepsilon_k} e^{-c_k(\log x)^{\varepsilon_k}}$ for large .
- Appendices A--I (pp. 85--195), opened by a preface and Table 1 of analytic inputs (p. 85), Appendix A beginning on p. 86. A: quantitative conventions, filtered nilmanifolds, symbols, Gowers norms, and the Quasipolynomial inverse theorem (Theorem A.7) on intervals, boxes and products of cyclic groups with dimension up to . B: the step-drop lemma for a biased symbol. C: the shift comparison theorem (Theorem C.1): a degree- positive comparison between and on transfers, outside a set of at most shifts, to degree- tests after multiplication by a shifted nonnegative ; its degree-one case adapts Kelley--Meka (their Sections 4--5) and Bloom--Sisask (their Sections 2.1--2.2) on Bohr sets. D: positive counting, the absolute increment on a fixed-dimensional prime box (score against for a degree- niltest), conversion of patches, and Proposition D.7 (Relative lifting, rank at most , with an impossibility alternative). E: unconstrained sampling and scalar transfer. F: constrained affine sampling (the coefficient tilt and the sampler's parameter order). G: cube comparison and pathwise detection. H: positive score recovery from constrained samples. I: relative lifting with additive rank, whose Theorem I.15 proves Proposition D.7 from the sampling assertions.
- External inputs the proofs rest on, at statement level: the interval
inverse theorem of Leng, Sah and Sawhney (arXiv:2402.17994v3, Theorem 1.2;
the box and product-cyclic forms are proved in Appendix A); Schoen--Sisask's
Theorem 5.4 (Forum Math. Sigma 4, 2016) as the radius-sensitive
almost-periodicity input; Green--Tao's quantitative orbit theory (Ann. of
Math. 175, 2012; Proposition 7.2, Lemma 7.4 and Appendix A) and Leng's
efficient equidistribution theorem (arXiv:2312.10772v5, Theorem 4) with
Leng--Sah--Sawhney's Theorem 5.4 and Corollary 5.5 as antecedents of the
step-drop lemma, which the manuscript proves itself; Conlon--Fox--Zhao's
densification method and Gowers's Hahn--Banach decompositions (Section 3.2)
as methods; Bergelson--Leibman's Theorem A* and Keller--Lifshitz--Marcus's
Theorem 5.4 cited as background or as a stronger bound for which a direct
moment proof is given instead. The manuscript says the inputs' "precise
hypotheses are stated at the points of application" (p. 8). It flags
nothing as numerical, computer-assisted or conditional; the only flagged
limitation is that constants depend on and the exponent is not
optimized. The release folder holds no
verification/directory for this manuscript. - References (pp. 196--198): 48 entries, from Behrend 1946 and Erdős--Turán 1936 through Raghavan (arXiv:2603.27045v3, 2026) and the release's own van der Waerden companion.
Bears on
- Problem 3: Corollary 1.2 is the problem's statement, progressions of every finite length in every set with divergent reciprocal sum, so the manuscript claims a resolution of the whole problem through the dyadic sum of Theorem 1.1; the claim is unverified here, no step of the proof (Sections 2--10 and Appendices A--I) was checked, and the page's status rests on acceptance evidence.
- Problem 142: Theorem 1.1 is a claimed upper bound on , for stronger than the recorded (Green--Tao, ) and (Leng--Sah--Sawhney, ); it is not an asymptotic formula, which is what the problem asks for, and the gap to Behrend's lower bound remains; unverified here, no status change implied.
- Problem 169: Corollary 11.2 claims , the finiteness of for each ; the constants are not explicit, so no numerical estimate of follows, and nothing is said about ; unverified here; the page's status rests on acceptance evidence.
- Problem 201: the manuscript does not name ; because the set is one of the -element sets in the definition, , so Theorem 1.1 would bound above by ; this corpus's inference, a comparison only, saying nothing about the ratio ; unverified here.
- Problem 139: Theorem 1.1 implies , the problem's statement, already proved (Szemerédi); the manuscript claims a stronger quantitative form by a new route; unverified here, and the page's status, resting on the accepted proof, is not affected.
- Problem 140: Theorem 1.1 with implies for every (the remark after Corollary 11.4), the problem's statement, already proved (Kelley--Meka); the manuscript claims "no improvement of the three-term exponent" (p. 6), so this is a new route to the problem's statement with an unspecified exponent, not a claimed improvement of the known one; unverified here, no status change.
- Problem 219: Corollary 1.2 applied to the primes, whose reciprocal sum diverges, gives the problem's statement, already proved (Green--Tao); Section 11.3 also re-derives the Green--Tao dense-primes theorem from ; a new route, unverified here, with the page's status resting on the accepted proof.