Sharp logarithmic exponents for off-diagonal Ramsey numbers

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation

▶The presented solutionin preparation

Papers 2

The sharp logarithmic exponent of r(5,t)

OpenAI · September 24, 2026

We determine the sharp logarithmic exponent of the off-diagonal Ramsey number \(r(5,t)\): \(\displaystyle r(5,t)=\frac{t^4}{(\log t)^{3+o(1)}} \qquad (t\longrightarrow\infty).\)

Read PDF Download Source

Cite

@misc{OAI:The-Sharp-Logarithmic-Exponent-of-r-5-t-September-24-2026,
  author = {{OpenAI}},
  title = {{The sharp logarithmic exponent of $r(5,t)$}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Sharp-Logarithmic-Exponent-of-r-5-t-September-24-2026/paper.pdf}{OAI:The-Sharp-Logarithmic-Exponent-of-r-5-t-September-24-2026}},
  year = {2026}
}

Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers

OpenAI · September 24, 2026

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).\)

Read PDF Download Source

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}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization determines the sharp logarithmic exponent of the off-diagonal Ramsey number \(r(5,t)\). It proves \(r(5,t)=t^4/(\log t)^{3+o(1)}\) as \(t\to\infty\). For every \(\varepsilon>0\), the lower bound \(t^4/(\log t)^{3+\varepsilon}\) holds eventually, while the upper bound is \(Ct^4/(\log t)^3\) for an absolute \(C>0\). The corresponding logarithmic exponent converges to three along all natural values of \(t\).

The formalization determines the sharp logarithmic exponent of the off-diagonal Ramsey number for every fixed integer \(s\ge6\). It proves \(r(s,t)=t^{s-1}/(\log t)^{s-2+o(1)}\) as \(t\to\infty\). More explicitly, for each \(\varepsilon>0\) the lower bound \(t^{s-1}/(\log t)^{s-2+\varepsilon}\) holds eventually, while the upper bound is \(C_s t^{s-1}/(\log t)^{s-2}\). The logarithmic exponent limit is taken along all natural values of \(t\).

Comparator links

Result	Comparator statement
Sharp logarithmic exponent of \(r(5,t)\)	RamseyFive.lean
Sharp logarithmic exponent for fixed off-diagonal Ramsey numbers	SharpLogRamsey.lean

Scope note on GitHub →