---

Claim. For every fixed $s\ge3$ there is a constant $c_s>0$ such that

$$r(s,k)\ \ge\ c_s\,\frac{k^{s-1}}{(\log k)^{2s-4}} \qquad\text{for all }k\ge2.$$

This is Theorem 1.1 of D. Bradač, Off-diagonal Ramsey numbers, arXiv:2605.28793v3 (16 June 2026), p. 2, recorded on the library's result page. In the letters of Problem 986 it gives $R(s,k)\gg k^{s-1}/(\log k)^{c}$ with $c(s)=2s-4$ for every $s\ge3$, which is the whole statement; together with the upper bound $R(s,k)\le(1+o(1))k^{s-1}/(\log k)^{s-2}$ it fixes $R(s,k)$ for fixed $s$ up to a polylogarithmic factor. The paper states that the theorem proves the conjecture and that it improves the previously best lower bounds for all $s\ge5$, where the exponent of $k$ had been $(s+1)/2$.

Postings. The first arXiv version (27 May 2026, titled "Nearly tight exponents for off-diagonal Ramsey numbers") proved only $r(s,k)\ge\Omega(k^{s-2}/(\log k)^{2s-6})$, which does not settle the problem; the second is of 11 June 2026; the third (16 June 2026, titled "Off-diagonal Ramsey numbers") carries the statement above, so the claim is dated to it. The site's reference pairs the first title with the arXiv identifier.

Method and read depth. The introduction describes a product of polarity graphs of projective spaces, with independent sets counted by a container argument in the manner of Alon and Rödl and the vertices then sampled at random, in the framework Mubayi and Verstraete and Mattheus and Verstraete used for $r(4,k)$. The proof (Subsection 2.5, pp. 10--13) is not checked in this corpus; the page rests on the statement, the displays (1)--(2) and the declaration on p. 4.

Depends on. Nothing in this wiki; the result rests on the cited paper alone. The refereed cases $s=3$ and $s=4$ are not used by it.

Provenance. The paper states (p. 2 and the declaration on p. 4) that an internal model at OpenAI supplied the argument raising the exponent of $k$ from $s-2$ to $s-1$ and passed it to the author, that AI tools played no significant part in the rest of the ideas and proofs, that Claude produced the computation in the appendix, and that the author wrote the text personally. This is the source's own account and is recorded, not judged.

Formalization. The autoformalization system Trellis reports two autonomous Lean formalizations of the paper, linked above at pinned commits: the repository offdiagonal (its tag paper-v3), whose README states that it first formalized v1 and then, in a revision run, updated the main target to v3's Theorem 1.1 together with the paper's four other theorems, and the repository offdiagonal-luna, a second run by OpenAI gpt-5.6-luna through the Codex CLI (the model its README names) that the system's web page says closes the same five targets. Both are described by their authors as free of sorry and using only the standard axioms. The thread comment of 10 June 2026 links the system's web page, not the repositories. Nothing of them is built or audited in this corpus, so these links add no evidence kind. A third formalization, linked above, is the file src/latest/ErdosProblems/Erdos986.lean of Boris Alexeev's lean-proofs repository (GitHub plby/lean-proofs), first added on 17 August 2026: it declares itself a Lean formalization of a solution to the problem, names Bradač as its informal author and Codex and GPT-5.6 Sol as its formal authors, and for Lean and Mathlib v4.33.0 proves erdos_986, that for every $s\ge3$ there is a natural number $c>0$ with $k^{s-1}/(\log k)^c=O(R(s,k))$, from a bound with exponent $2s-4$ (bradac_ramsey_lower_bound_isBigO) that it imports from the repository's construction files for Problem 920. Since 19 September 2026 the formal-conjectures statement erdos_986, still with proof sorry, carries a formal_proof attribute pointing at this file. The corpus has not built or audited it, so it adds no formalized evidence.

Acceptance. Reviewed: the site's curator, Thomas Bloom, relabeled the problem PROVED (page last edited 21 June 2026) after the thread's report of 17 June 2026 that v3 resolves it, and the site's commentary credits the lower bound to this paper as the resolution. The curator is independent of the author. Not refereed: no journal record exists under either title (publisher bibliographic queries, 2026-09-17), and no referee's report or other expert review was found. Not formalized: no Lean checked in this corpus proves the statement; the third-party formalizations above are unbuilt here.

Relation to other claims. The two manuscripts of the OpenAI release of 24 September 2026 (claim page) build on this paper's construction and claim the sharp logarithmic exponent $s-2$ for every fixed $s\ge5$; they do not bear on the acceptance of this claim. The refereed cases $s=3$ (Spencer 1977, credited by Spencer to Erdős) and $s=4$ (Mattheus and Verstraete, Annals of Mathematics 2024) are accepted partial claims.