VibeMathedMath problems solved with AI

The logarithmic exponent of the off-diagonal Ramsey numbers r(s,t) for fixed s at least 5

For fixed ss, the Ramsey number r(s,t)r(s,t) is the least NN such that every graph on NN vertices contains KsK_s or an independent set of size tt. Ajtai, Komlos and Szemeredi (1980) proved r(s,t)=Os(ts−1/(log⁡t)s−2)r(s,t)=O_s(t^{s-1}/(\log t)^{s-2}), and Erdos asked for the true order of growth: for s=3s=3 it is t2/log⁡tt^2/\log t (Kim 1995), Erdos Problem #166 asked for r(4,t)≫t3/(log⁡t)O(1)r(4,t)\gg t^3/(\log t)^{O(1)} (Mattheus-Verstraete), and Erdos Problem #986 asked for r(s,t)≫ts−1/(log⁡t)c(s)r(s,t)\gg t^{s-1}/(\log t)^{c(s)}, which Bradac proved in 2026 with c=2s−4c=2s-4. That left the power of log⁡t\log t between s−2s-2 and 2s−42s-4. For fixed s≥5s\ge5, what is the exponent θs\theta_s with r(s,t)=ts−1/(log⁡t)θs+o(1)r(s,t)=t^{s-1}/(\log t)^{\theta_s+o(1)}; in particular, is the Ajtai-Komlos-Szemeredi upper bound sharp up to (log⁡t)o(1)(\log t)^{o(1)}?

Result
Proved(see note)
Status
Partial result
AI contribution
AI-discovered
Method
Construction
Field
Extremal and probabilistic combinatorics: Ramsey numbers
Posed by
Classical problem of P. Erdos on the order of r(s,t) for fixed s (Erdos Problems #165, #166, #986; general case per Chung and Graham, 1998); upper bound by Ajtai, Komlos and Szemeredi (1980)
Year posed
—
Years open
—
Solved
2026-09-24
Model
Unreleased internal OpenAI model
Vendor
OpenAI
Collaborators
—
Verification
Lean-checked, statement unaudited
Publication
Announced
Collection
OpenAI math release (October 2026), version adc7f12
Significance
44 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

For every fixed s≥5s\ge5: there is CsC_s such that for every ε>0\varepsilon>0 and all large tt, ts−1/(log⁡t)s−2+ε≤r(s,t)≤Csts−1/(log⁡t)s−2t^{s-1}/(\log t)^{s-2+\varepsilon}\le r(s,t)\le C_s t^{s-1}/(\log t)^{s-2}, so r(s,t)=ts−1/(log⁡t)s−2+o(1)r(s,t)=t^{s-1}/(\log t)^{s-2+o(1)} and the classical upper bound is sharp up to (log⁡t)o(1)(\log t)^{o(1)}. The lower bound comes from a random ordered point-hyperplane flag graph in PG(s−1,q)\mathrm{PG}(s-1,q) (Bradac's construction) with a new entropy and compression analysis of its independent sets. It does NOT give r(s,t)=Θ(ts−1/(log⁡t)s−2)r(s,t)=\Theta(t^{s-1}/(\log t)^{s-2}), and it does not cover s=4s=4, where the gap between t3/(log⁡t)4t^3/(\log t)^4 and t3/(log⁡t)2t^3/(\log t)^2 remains.

What the AI did

The OpenAI math release (github.com/openai/math, commit adc7f12) states that its results were produced by an unreleased internal OpenAI model under one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result. This result is not among the README's stated exceptions (the Re(s) > 11/12 zero-free region write-up and the Hodge conjecture for CM abelian varieties). The manuscript is credited to OpenAI alone and names no human author. The family has two manuscripts dated 24 September 2026: one for s = 5 and one for every fixed s >= 6, each self-contained.

Verification

No independent mathematician has checked this yet. Checked here: the abstracts, introductions and main theorems of both TeX sources, read against the Erdos problems and the state of the art they cite (Bradac 2026, Ajtai-Komlos-Szemeredi 1980); the proofs were not refereed. Lean: the Comparator challenges RamseyFive (OAI.SharpRamseyFive.main, solution module OAI/Combinatorics/RamseyFive/Main.lean) and SharpLogRamsey (OAI.SharpLogRamsey.main, solution module OAI/Combinatorics/SharpRamsey/Main.lean) are not in the release's formalization catalogue, but their JSON and solution files exist at the pinned commit. Their statements were read here: with r(s,t) defined as the least N such that every graph on Fin N has an s-clique or a t-independent set, they assert an absolute C with ts−1/(log⁡t)s−2+ε≤r(s,t)≤Cts−1/(log⁡t)s−2t^{s-1}/(\log t)^{s-2+\varepsilon}\le r(s,t)\le C t^{s-1}/(\log t)^{s-2} eventually for every ε>0\varepsilon>0, and convergence of the logarithmic exponent to s−2s-2, for s = 5 and for every s >= 6 respectively. Together they state the headline claim. Permitted axioms: propext, Quot.sound, Classical.choice. Not rebuilt here.

Sources

Changelog1 change

Discussion