---

Claim. Two preprints of the OpenAI mathematics release, both dated 24 September 2026 and authored by OpenAI, claim the sharp logarithmic exponent of the off-diagonal Ramsey number for every fixed $s\ge5$. The sharp logarithmic exponent of $r(5,t)$ (carded as openai_2026_sharp_logarithmic_exponent_r_5_t, the statement paged at Theorem 1.1) states in its introduction that there is an absolute constant $C>0$ such that for every $\varepsilon>0$ and all sufficiently large $t$

$$\frac{t^{4}}{(\log t)^{3+\varepsilon}} \ \le\ r(5,t)\ \le\ C\,\frac{t^{4}}{(\log t)^{3}},$$

the threshold depending on $\varepsilon$; Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers (carded as openai_2026_sharp_logarithmic_exponents_fixed_off_diagonal_ramsey_numbers, the statement paged at Theorem 1.1) states that for every fixed $s\ge6$ there is $C_s>0$ such that for every $\varepsilon>0$ and all sufficiently large $t$

$$\frac{t^{s-1}}{(\log t)^{s-2+\varepsilon}} \ \le\ r(s,t)\ \le\ C_s\,\frac{t^{s-1}}{(\log t)^{s-2}}.$$

Both conclude $r(s,t)=t^{s-1}/(\log t)^{s-2+o(1)}$ as $t\to\infty$, the logarithmic exponent converging to $s-2$ along all natural $t$. The upper bounds restate the Ajtai--Komlós--Szemerédi bound; both manuscripts include their own proof of it, the first for the case $s=5$ with an absolute constant, the second for every $s\ge6$. The release's README says that its manuscripts were produced by an internal OpenAI model and that its results are at different stages of verification, not all of them with Lean formalizations.

Covers. The statement of Problem 986 for every fixed $s\ge5$: the lower bounds give $r(s,k)\gg k^{s-1}/(\log k)^{c}$ for any $c>s-2$, for instance $c=s-1$, and determine the power of the logarithm, which Bradač's bound had left between $2s-4$ and $s-2$. The cases $s=3$ and $s=4$ are not treated; they rest on the refereed results of Spencer and of Mattheus and Verstraete.

Depends on. Bradač's lower bound supplies the construction, not the theorem: both manuscripts work with the ordered incident-flag graph of the higher-dimensional construction in Subsection 2.5 of Bradač's paper and adapt its marking argument (its Claim 2.13). Each proves its own projective incidence estimate, the bipartite form of Alon and Krivelevich's orthogonality calculation: the $r(5,t)$ manuscript's Lemma 3.1, whose calculation it notes also underlies Bradač's polarity-graph estimates (Bradač's Lemma 2.1), and the general-$s$ manuscript's Lemma 2.1. The general-$s$ manuscript says it supplies all the required arguments locally; its companion develops the selected-law entropy framework for $s=5$. That page is accepted on the site curator's review; this claim rests on its own evidence, the formalization recorded under Acceptance. below.

Method and read depth. By the introductions, the improvement over Bradač's exponent $2s-4$ lies in the analysis of long independent sequences: an entropy and compression argument for a sequence selected from a random stream, separating steps with few choices from steps that shrink the candidate set substantially, in the spirit of Alon and Rödl's independent-set counting; for general $s$ a repeated-projection reduction for sparse pairs and a two-row high-rank description that rests on Nie and Wang's finite-degree closure inequality. The page rests on the abstracts, introductions and main theorem statements in the release's TeX sources; no proof is checked here.

Formalization. The release's Lean tree at the pinned revision states the two theorems in ComparatorChallenges/RamseyFive.lean (OAI.SharpRamseyFive.main: the sharp bounds and the exponent limit for $r(5,t)$) and ComparatorChallenges/SharpLogRamsey.lean (OAI.SharpLogRamsey.main, for every s with 6 ≤ s), each with sorry as the challenge form, and holds solution modules OAI/Combinatorics/RamseyFive/ and OAI/Combinatorics/SharpRamsey/ whose Main.lean files prove those two declarations, both imported by the project's root module; the two Main.lean files are the formalization links above, and the challenge files, being statements, are not linked; the comparator records permit only propext, Quot.sound and Classical.choice. The release's own catalog of papers with a formalized main result, formalization.yaml, lists neither manuscript, while its family document describes the formalization's scope. Toolchain leanprover/lean4:v4.34.1. The build and the statement audit of the two declarations are recorded in the Acceptance paragraph below.

Acceptance. Formalized, as a partial claim. This corpus's verification built OAI.SharpRamseyFive.main and OAI.SharpLogRamsey.main at the pinned revision with the toolchain leanprover/lean4:v4.34.1 and checked their axioms, which are exactly propext, Classical.choice and Quot.sound, with no sorry; the comparator challenges ComparatorChallenges/RamseyFive.lean and ComparatorChallenges/SharpLogRamsey.lean pin the two declarations, and each fingerprint was found identical to its challenge. A statement audit compared each declaration clause by clause with the displays above. OAI.SharpRamseyFive.main states the case $s=5$ exactly: one absolute $C>0$, chosen before $\varepsilon$, with $t^4/(\log t)^{3+\varepsilon}\le r(5,t)\le Ct^4/(\log t)^3$ for every $\varepsilon>0$ and all $t$ past a threshold depending on $\varepsilon$, and $(4\log t-\log r(5,t))/\log\log t\to3$ along the natural numbers. OAI.SharpLogRamsey.main states the case of every $s\ge6$ exactly, with $C_s$ chosen for each $s$ and before $\varepsilon$, and with the exponent limit $s-2$; its natural-number subtractions $s-1$ and $s-2$ are exact since $s\ge6$. In both, $r(s,t)$ is the least $N$ such that every simple graph on $N$ vertices has a clique of size $s$ or an independent set of size $t$, the Ramsey number; the infimum is never a junk value, since the defining set is upward closed and the proved lower bound rules out an empty one. Taking $\varepsilon=1$ gives the statement of Problem 986 for every fixed $s\ge5$ with $c=s-1$ and constant $1$. Together the two declarations certify this page's whole result; the scope stays partial because $s=3$ and $s=4$ are outside both, and those cases rest on the refereed claims of Spencer and of Mattheus and Verstraete. Not reviewed: the manuscripts are release preprints with no journal record and no independent review, the release's README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification, and its catalog of formalized papers lists neither manuscript. The acceptance of Bradač's full claim is a separate question and is not affected.