# Sharp logarithmic exponents for off-diagonal Ramsey numbers

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

- [The sharp logarithmic exponent of $r(5,t)$](../../preprints/The-Sharp-Logarithmic-Exponent-of-r-5-t-September-24-2026/paper.pdf)
- [Sharp Logarithmic Exponents for Fixed Off-Diagonal Ramsey Numbers](../../preprints/Sharp-Logarithmic-Exponents-for-Fixed-Off-Diagonal-Ramsey-Numbers-September-24-2026/paper.pdf)

## 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](../ComparatorChallenges/RamseyFive.lean) |
| Sharp logarithmic exponent for fixed off-diagonal Ramsey numbers | [SharpLogRamsey.lean](../ComparatorChallenges/SharpLogRamsey.lean) |