Browse › Combinatorics › 184 Correspondence coloring with a fixed forbidden subgraph
A logarithmic independence bound for clique-free graphs
Open PDFCite Report a problem Add a reference or comment Interested in working on this Start a discussion
Edit NOTES.md · Existing issues · Source on GitHub
Abstract
For every fixed integer r ≥ 4, every Kr-free graph on n vertices with average degree d ≥ 2 has an independent set of size at least $c_r n\log d/d$, where $c_r\gt 0$ depends only on r. This proves the fixed-clique-size independence conjecture of Ajtai, Erdős, Komlós and Szemerédi.
If the PDF does not display here, open it directly: Open PDF.
Notes
No notes yet. Add a reference, a comment or your name with the buttons above, or edit NOTES.md on GitHub.
Automatically collected notes (unreviewed)
work in progress
Collected automatically by AI tools (Claude Opus 5.5 and GPT-6 Astra, 2026-10-21) and not checked by a person. May be wrong or incomplete. Report an error.
Follow-up works
- Kaizhe Chen, A note on the logarithmic exponent of Ramsey number r(4,t) (arXiv:2610.15293, 11 October 2026). Cites this paper for its Lemma 1.3, the bound α(G) ≥ c_s n log d/d for K_s-free graphs, and combines it with the release's r(s,t) preprints to derive r(4,t) = t³/(log t)^(2+o(1)); the note says it is for informal circulation only.
Formalization
- OpenAI math release (mirrored at mathcommunity/oai-math-revised), lean/docs/184.md (release Lean scope note, 2026-10-06). Gives the scope of the release's Lean formalization of Theorem 1.1, the c_r n log d/d bound for K_r-free graphs with r ≥ 4 and average degree d ≥ 2, with comparator statement CliqueFreeLog.lean.
- google-deepmind/formal-conjectures, ErdosProblems/802.lean (added by PR #7165, merged 20 October 2026). An independent Lean statement of Erdős Problem 802, the conjecture Theorem 1.1 addresses, with AEKS, Shearer, r=3 and Alon variants; at the time of access the main statement is still tagged open and the PR does not mention this paper.
- Erdős Problems (erdosproblems.ai), OpenAI's logarithmic independence bound for clique-free graphs (updated 2026-10-08). Reports building the release's Lean theorem and comparator, checking axioms and statement fingerprints, and auditing the formulation against Problem 802, while explicitly recording no outside review or independent acceptance.
Possibly relevant literature (found by the agent, not checked)
- N. Bansal, A. Gupta, G. Guruganesh, On the Lovász Theta function for Independent Sets in Sparse Graphs (arXiv:1504.04767, STOC 2015). Gives an improved Ramsey-type bound on the independence number of K_r-free graphs for large r, made algorithmic via an SDP, which may be relevant to the paper's remark that its proof makes no claim of an efficient algorithm.
Digests and expositions
- Latent Seminar, Forbidden subgraphs, independence, and correspondence coloring (2026-10-07). Explains both manuscripts' weighted triangle estimates and vertex splitting, including the additional participation bound needed for correspondence coloring, while explicitly disclaiming independent verification of the complete proofs. [family-level]
- AI Proved What?, Forbid a clique, gain a log? (Episode 184, October 2026). Provides an animated exposition and transcript covering both claimed bounds, examples distinguishing list and correspondence coloring, and the stated formalization scope. [AI-generated per source] [family-level]
News and blogs
- Thomas Bloom, Erdős problems in the OpenAI proofs (erdosproblems.com blog) (8 October 2026). Its section on Problem 802 states the release's claimed bound for K_r-free graphs, r ≥ 4, says it would prove the Ajtai–Erdős–Komlós–Szemerédi conjecture and improve Shearer's bound, and notes "This proof has been formalised."
Elsewhere
- VibeMathed: Problem record
- Emergent Mind: family 184
Independent sites; their content is not reviewed here.
Cite
@misc{OAI:A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026,
author = {{OpenAI}},
title = {{A logarithmic independence bound for clique-free graphs}},
howpublished = {OpenAI Math Release preprint
\href{https://github.com/openai/math/blob/main/preprints/A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026/paper.pdf}{OAI:A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026}},
year = {2026}
}Lean formalization
OpenAI provides Lean files for this family: lean/docs/184.md. The Lean statements have not been checked by people against the paper's claims.
Family 184: Correspondence coloring with a fixed forbidden subgraph
Proves the Alon–Krivelevich–Sudakov coloring conjecture in correspondence-coloring form: graphs avoiding any fixed subgraph F need $O_F(\Delta/\log\Delta)$ colors when their maximum degree Δ is sufficiently large. Also proves the Ajtai–Erdős–Komlós–Szemerédi independence conjecture: for fixed r ≥ 4, every n-vertex Kr-free graph of average degree d ≥ 2 has an independent set of size $\Omega_r(n\log d/d)$.
Other papers in this family:
- Correspondence coloring graphs with a forbidden clique · October 5, 2026