oai-math-revised beta

Browse › Combinatorics › 170 Sharp logarithmic exponents for off-diagonal Ramsey numbers

Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers

OpenAI · September 24, 2026

Lean

Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion

Edit NOTES.md · Existing issues · Source on GitHub

Abstract

For every fixed integer s ≥ 6, we determine the sharp logarithmic exponent of the off-diagonal Ramsey number: $\displaystyle r(s,t)=\frac{t^{s-1}}{(\log t)^{s-2+o(1)}} \qquad (t\longrightarrow\infty).$

If the PDF does not display here, open it directly: Open PDF.

Notes

No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.

Automatically collected notes (unreviewed)

work in progress

Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.

Follow-up works

  • Kaizhe Chen, A note on the logarithmic exponent of Ramsey number r(4,t) (arXiv:2610.15293, 11 Oct 2026). Informal note that cites this paper (s≥6) and its companion (s=5), and derives $r(4,t)=t^3/(\log t)^{2+o(1)}$ from them via a transfer principle from $r(s,t)$ to $r(s-1,t)$; it also remarks that removing the $o(1)$ for some $s\ge5$ would remove it for $s-1$. [family-level]

Formalization

  • OpenAI math release, Lean scope notes for family 170 (lean/docs/170.md, 2026-10-06). The release's scope note says the Lean development proves, for every fixed $s\ge6$, the eventual bounds $t^{s-1}/(\log t)^{s-2+\varepsilon}\le r(s,t)\le C_st^{s-1}/(\log t)^{s-2}$ and the exponent limit along natural $t$, with comparator statement SharpLogRamsey.lean (and RamseyFive.lean for the companion paper). [family-level]
  • OpenAI, SharpRamsey/Main.lean (openai/math, commit adc7f12). The top-level Lean file for this paper, stating OAI.SharpLogRamsey.main (s : ℕ) (hs : 6 ≤ s) : MainBounds s ∧ MainLimit s.
  • Erdős Problem a Day, #986: OpenAI's two Lean proofs kernel-replayed here (2026-10-20). Reports rebuilding and kernel-checking both Lean developments, matching their comparator statements, and developing an $s=4$ extension and a bridge to Formal Conjectures' Ramsey definition; the accompanying manuscript review is explicitly attributed to AI agents. [AI-generated per source] [family-level]
  • Domagoj Bradač, Off-diagonal Ramsey numbers (arXiv:2605.28793v3, 2026-06-16). Chen and Lin–Zhang identify its lower bound $r(s,t)\ge c_s t^{s-1}/(\log t)^{2s-4}$ as the preceding polynomial-exponent result whose logarithmic loss the OpenAI family improves. [family-level]

Possibly relevant literature (found by the agent, not checked)

Digests and expositions

Elsewhere

Independent sites; their content is not reviewed here.

Cite

@misc{OAI:Sharp-Logarithmic-Exponents-for-Fixed-Off-Diagonal-Ramsey-Numbers-September-24-2026,
  author = {{OpenAI}},
  title = {{Sharp Logarithmic Exponents for Fixed Off-Diagonal Ramsey Numbers}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Sharp-Logarithmic-Exponents-for-Fixed-Off-Diagonal-Ramsey-Numbers-September-24-2026/paper.pdf}{OAI:Sharp-Logarithmic-Exponents-for-Fixed-Off-Diagonal-Ramsey-Numbers-September-24-2026}},
  year = {2026}
}

Lean formalization

OpenAI provides Lean files for this family: lean/docs/170.md. The Lean statements have not been checked by people against the paper's claims.

Family 170: Sharp logarithmic exponents for off-diagonal Ramsey numbers

For every fixed integer s ≥ 5, proves $r(s,t)=t^{s-1}/(\log t)^{s-2+o(1)}$ as $t\to\infty$, determining the logarithmic exponent and matching the classical upper bound at that scale. Here $r(s,t)$ is the least number of vertices forcing an s-clique or a t-vertex independent set.

Other papers in this family: