Ramsey numbers: log power settled?

The claim, in plain words

Among six people there are always three who all know each other or three who are all strangers; with five there may not be. The Ramsey number r(s,t) is the fewest people that guarantees s mutual acquaintances or t mutual strangers. These papers study “the off-diagonal regime in which s is fixed and t tends to infinity”. Erdős and Szekeres (1935) showed that r(s,t) is at most about t^s−1, and Ajtai, Komlós and Szemerédi (1980) saved a power of log t: r(s,t) is at most a constant times t^s−1/(log t)^s−2. For s = 3, “Kim proved that r(3,t) has order t²/log t, matching the classical upper bound in order.” Lower bounds need graphs with no s-clique and no large independent set. For r(5,t), as the papers recount, Spencer’s local lemma gave order (t/log t)³ and the Bohman–Keevash random process gave t³/(log t)^8/3: “Thus even the power of t in the upper bound remained out of reach by these methods.” In 2026 Bradač (an arXiv preprint) proved r(s,t) ≥ c_s t^s−1/(log t)^2s−4, “determining the polynomial exponent for every fixed s”; for s = 5 that is t⁴/(log t)⁶ against the upper bound’s t⁴/(log t)³.

Result 170 is two OpenAI preprints, both dated September 24, 2026. The sharp logarithmic exponent of r(5,t) (41 pages), Theorem 1.1: “There is an absolute constant C>0 such that, for every ε>0, all sufficiently large integers t satisfy t⁴/(log t)^3+ε ≤ r(5,t) ≤ C·t⁴/(log t)³.” Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers (53 pages), Theorem 1.1: “For every fixed integer s≥6 there is a constant C_s>0 such that, for every ε>0 and every sufficiently large integer t, t^s−1/(log t)^s−2+ε ≤ r(s,t) ≤ C_s t^s−1/(log t)^s−2.” In both, the limit of ((s−1) log t − log r(s,t))/log log t is s − 2. The new part is the lower bound; each paper re-proves the classical upper bound so as to be self-contained. The second paper cites the first’s framework but “supplies all the required arguments locally”.

What they don’t claim

“Sharp” here means the exponent of log t, not the constant: the first paper “leaves open a constant-factor asymptotic for t⁴/(log t)³”, and the second “does not assert that r(s,t) is bounded below by a positive constant times t^s−1/(log t)^s−2”. The lower bound loses a factor (log t)^ε, and how large t must be is never quantified. s = 4 is not covered; s = 3 was settled before. The graphs are shown to exist by contradiction, with no explicit construction and no algorithm: “No bound on the time needed to search or decode is asserted.” And the exponent is a limit that settles very slowly. In our own calculation, if r(5,t) were exactly t⁴/(100 (log t)³), the quantity in the theorem would be 4.75 at t = 10⁶, 4.39 at 10¹² and 3.85 at 10¹⁰⁰, on its way down to 3.

Where it stands

Posted as preprints

OpenAI, 41 and 53 pages, both dated September 24, 2026

Peer reviewed

Not yet

Checked in Lean

Both main theorems, formalized by OpenAI; not run by us

Last checked October 19, 2026. Neither preprint has been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization whose comparator statements, one for s = 5 and one for every s ≥ 6, state both bounds and the limits as in the papers; the upper bound is formalized from scratch. By our count the proofs take 482 files and 73,678 lines (s = 5, the development) and 408 files and 63,795 lines (s ≥ 6), excluding Mathlib; the s = 5 proof reuses 32 files from the s ≥ 6 library, with no unproved steps by our search; we have not rebuilt them. One construction lemma in the s ≥ 6 development is stated for every dimension from 3 up; read at face value, it would also bear on r(4,t), which no one claims, so we have flagged it for expert review rather than draw any conclusion. The key earlier construction comes from Bradač’s June 2026 arXiv preprint, and the papers re-prove what they use from it. The papers are not among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

1. The graph. Following Bradač, work in projective space of dimension d = s − 1 over a large prime field. A flag is a point together with a hyperplane through it. Take a random stream of about q^d log q flags, and join an earlier flag i to a later flag j when the point a_i lies on the hyperplane b_j “but a_j does not lie on b_i”.
2. No s-clique. In a clique listed in order, each new point is off the earlier hyperplanes but on all later ones, so the points are linearly independent yet all lie in the last hyperplane: “A five-clique would give five linearly independent points in one hyperplane.” Independent sets are the consistent sequences.
3. An entropy count. Suppose every stream had a consistent sequence of length about q(log q)^1+η. Then picking one out of a random stream would carry a lot of information, by a union bound.
4. Cheap descriptions. Marking scans, adapted from Bradač, put most flags into small known regions. “The principal additional ingredient is a description theorem for sparse point–hyperplane pairs”: a short message, drawn from shared random tables, that pins down part of them, using projections to lower dimensions, a Poisson score, and polynomial-method bounds for rich lines. A balanced tree of tests uses it to shrink the decoder’s domains, and a bounded number of rounds shortens the description.
5. The contradiction. The final description is shorter than the entropy bound allows, so some stream has no long independent set: a graph on about q^d log q vertices with no (d+1)-clique and no independent set of about q(log q)^1+η. Choosing the prime to fit t gives the lower bound.

The numbers in the video

• Our check of r(3,3) = 6: the pentagon colouring of five people has no one-coloured triangle, and all 32,768 colourings for six people have at least 2.
• The bounds for r(5,t), as the papers cite them: Spencer (t/log t)³, Bohman–Keevash t³/(log t)^8/3, Bradač t⁴/(log t)⁶, new t⁴/(log t)^3+ε, against the upper bound t⁴/(log t)³.
• Our Fano-plane example: 7 points, 7 lines and 21 flags, with a sample stream of 5 flags.
• Our exhaustive check of every ordered sequence of flags: cliques of size d occur (84 and 468 for d = 2 with q = 2 and 3; 10,080 for d = 3; 4,999,680 for d = 4, all with q = 2), but never of size d + 1.
• Our limit calculation, quoted above; and the Lean counts, our count of the import closures.

Read the source

• The sharp logarithmic exponent of r(5,t) (PDF), 41 pages.
• Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers (PDF), 53 pages.
• The Lean scope note.
• The collection’s catalog, where this is result 170.

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

• The sharp logarithmic exponent of r(5,t) main paper
• Sharp logarithmic exponents for fixed off-diagonal Ramsey numbers companion

Transcript

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.