The Ajtai-Erdos-Komlos-Szemeredi conjecture on independent sets in K_r-free graphs
Erdős problem #802 · erdosproblems.com/802
Every graph with vertices and average degree has an independent set of size at least , and disjoint cliques show this is sharp. Ajtai, Komlos and Szemeredi (1980) proved that triangle-free graphs have , and Shearer sharpened the constant to . In 1981 Ajtai, Erdos, Komlos and Szemeredi conjectured the same order for every fixed forbidden clique; they proved , and Shearer (1995) improved this to . For fixed , does every -free graph on vertices with average degree have an independent set of size ?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Extremal graph theory: independence number
- Posed by
- M. Ajtai, P. Erdos, J. Komlos and E. Szemeredi, On Turan's theorem for sparse graphs, Combinatorica 1 (1981), p. 314; Erdos Problem #802
- Year posed
- 1981
- Years open
- 45y
- Solved
- 2026-09-25
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 46 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: for every there is such that every finite -free graph with vertices and average degree has , removing the loss in Shearer's 1995 bound. The proof maximizes an entropy functional over vertex weights and shows that the weighted triangle mass is at most times the edge mass, via random multipliers, vertex splitting and a recursion on the clique size. The constant is not optimized and no leading coefficient (as in Shearer's triangle-free result) is claimed.
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. A companion manuscript in the same family (5 October 2026) extends the method to correspondence coloring.
Verification
No independent mathematician has checked this yet. Checked here: the abstract, introduction and Theorem 1.1 of the TeX source, read against the conjecture as stated in AEKS (1981) and Erdos Problem #802; the proof was not refereed. Lean: formalization.yaml lists OAI.CliqueFreeLog.logarithmic_independence_bound (Comparator challenge CliqueFreeLog, file OAI/Combinatorics/CliqueFree/Main.lean). Its statement was read here: for every r >= 4 there is c > 0 such that every finite simple graph that is r-clique-free with average degree 2|E|/|V| at least 2 has independence number at least c |V| log d / d. This is the headline claim. Permitted axioms: propext, Quot.sound, Classical.choice. Not rebuilt here.