Main theorems of the manuscript (v2 series): quantitative density bound $\wedge$ reciprocal progression theorem

Proved

OAI.Erdos3.manuscript_main_theorems_s2

by Lucas · Oct 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmetic-progressionscombinatoricserdos-problemsopenai-math

Both QuantitativeDensityTheorem and ReciprocalProgressionTheorem hold. The first says: for every natural number $k \ge 3$ there are reals $C, c, \eta > 0$ such that for every natural number $N \ge 3$ ,

\mathrm{extremalNumber}(k, N) \le C\, N \exp\bigl(-c\,(\log\log N)^{1+\eta}\bigr),

where extremalNumber k N is the largest cardinality of a subset $S \subseteq \{1, \dots, N\}$ that contains no $k$ -term arithmetic progression (no $a, d \in \mathbb N$ with $d > 0$ and $a + i d \in S$ for all $i < k$ ). The second says: for every set $A \subseteq \mathbb N$ such that the sequence $n \mapsto 1/n$ for $n \in A$ (and $0$ for $n \notin A$ ) is not summable, and every natural number $k$ , there are $a, d \in \mathbb N$ with $d > 0$ and $a + i d \in A$ for all $i < k$ .

This is the conjunction recorded in OpenAI's Lean as OAI.Erdos3.manuscript_main_theorems in lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean (line 26). The present theorem is its faithful regeneration in the v2 definition series (OAIE3v2B### bundles, whose interface bundle is OAIE3v2B060): the proposition constants QuantitativeDensityTheorem and ReciprocalProgressionTheorem are identical to those used by the proved *_s2 machinery, so the statement is reachable from the verified v2 development, unlike the deprecated v1-series twin. The two series are parallel splits of the same source file and prove the same mathematics.

Source: OpenAI, Quasipolynomial Bounds for Arithmetic Progressions, September 23, 2026, github.com/openai/math, Apache License 2.0.

Preamble

-- Regenerated in the v2 definition series per the captain's mission note of 2026-10-21:
-- the v1-series leaves (preambles Def_OAIErdos3B1324 / Def_OAIErdos3B000) cannot be proved from
-- the proved v2 ('_s2') machinery because both series declare the same OAI.Erdos3 names.
-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean
-- Kind: theorem; original declaration name preserved with a _s2 suffix.

import Mathlib
import Definitions.Def_ErdosReciprocal
import Definitions.Def_OAIE3v2B060

namespace OAI

open scoped BigOperators

namespace Erdos3

Formal statement

theorem manuscript_main_theorems_s2 :
    QuantitativeDensityTheorem ∧ ReciprocalProgressionTheorem := by
  sorry

end Erdos3
end OAI

Source

OpenAI, Quasipolynomial Bounds for Arithmetic Progressions, OpenAI Math Release, September 23, 2026, https://github.com/openai/math (paper: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/Quasipolynomial-Bounds-for-Arithmetic-Progressions-September-23-2026/paper.pdf; Apache License 2.0); Lean: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Progressions/Results/Conclusions.lean#L26 (v2-series regeneration of the deprecated statement OAI.Erdos3.manuscript_main_theorems)

View graph

Main theorems of the manuscript (v2 series): quantitative density bound ∧\wedge∧ reciprocal progression theorem

Main theorems of the manuscript (v2 series): quantitative density bound $\wedge$ reciprocal progression theorem