The Ajtai–Erdős–Komlós–Szemerédi independence conjecture

The Ajtai–Erdős–Komlós–Szemerédi (AEKS) independence conjecture (1981; Erdős Problem 802) asserts the following for every fixed r. Every K_r-free graph on n vertices with average degree d has an independent set of size at least a constant (depending on r) times n log d/d. That is the same order as for triangle-free graphs. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math) make claims on this problem and on the related Alon–Krivelevich–Sudakov coloring conjecture. This page summarizes the published claims and lists publicly available follow-up work.

Background

• As recounted in the introduction of A logarithmic independence bound for clique-free graphs:
  • For general graphs the bound α(G) ≥ n/(d + 1) is best possible, as disjoint unions of cliques show.
  • Ajtai, Komlós and Szemerédi (1980) proved the logarithmic improvement for triangle-free graphs, and Shearer (1983) obtained the asymptotic coefficient 1.
  • In 1981, Ajtai, Erdős, Komlós and Szemerédi conjectured the same order of growth for each fixed forbidden clique. They proved the lower bound Ω_r(n log log d/d).
  • Shearer (1995) improved this to Ω_r(n log d/(d log log d)). Later refinements describe more of the local structure and, for a fixed forbidden clique, retain a log log loss: Dutta–Mubayi–Subramanian; Davies–Kang–Pirot–Sereni; Dhawan.
  • Logarithmic bounds hold under stronger local assumptions, for example Alon (1996), when every vertex neighbourhood is (r − 2)-colourable.
• The Erdős Problems page for problem 802 records the conjecture and the bounds of Ajtai–Erdős–Komlós–Szemerédi, Shearer, Ajtai–Komlós–Szemerédi and Alon.

The original results

• Independence (25 September 2026). The manuscript A logarithmic independence bound for clique-free graphs, Theorem 1.1: for every integer r ≥ 4 there is c_r > 0 such that every finite simple K_r-free graph with n vertices and average degree d ≥ 2 satisfies α(G) ≥ c_r n log d/d.
  • The manuscript states that this gives a positive answer to the AEKS conjecture, recorded as Erdős Problem 802. The order is best possible up to a constant even for triangle-free graphs, and the constant c_r is not optimized.
• Coloring (5 October 2026). The manuscript Correspondence coloring graphs with a forbidden clique claims a bound for every fixed r ≥ 4: every K_r-free graph of sufficiently large maximum degree Δ has correspondence chromatic number O_r(Δ/log Δ).
  • It presents this as resolving the Alon–Krivelevich–Sudakov coloring conjecture in the stronger correspondence-coloring form.
  • The same bound, with a constant depending on F, is claimed when any fixed graph F is excluded as a subgraph. Ordinary and list coloring satisfy the same bounds.
• Sources. Commit 1581d4c of the openai/math repository:
  • A logarithmic independence bound for clique-free graphs;
  • Correspondence coloring graphs with a forbidden clique.
• Formalization, as described by the repository.
  • The scope note lean/docs/184.md links only the independence manuscript. It states the formalized result: for every fixed integer r ≥ 4 there is c_r > 0 such that every finite K_r-free simple graph on n vertices with average degree d ≥ 2 has an independent set of size at least c_r n log d/d.
  • The Comparator challenge CliqueFreeLog.lean states logarithmic_independence_bound, with the average degree defined as 2|E|/|V| and Mathlib's independence number.
  • The coloring result is not among the selected statements.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 17 October 2026)
2026-10-08	MathVet (GitHub; review of openai/math, tables at repository commit c76f1e4, 14 October 2026)	Review (fidelity of the formal statements)	Rates the family "partial". Only the independence half is stated; the coloring conjecture in correspondence-coloring form has no Lean statement. Records a sandboxed Comparator pass for CliqueFreeLog.	MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
2026-10-10 to 2026-10-14	con-leche development journal (task #348)	Verification (second kernel)	In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list CliqueFreeLog. The challenge was therefore accepted by con-leche and by Lean's official kernel.	Development journal.
2026-10-10	cert-machine, openai/math lane K, run 38017370880	Verification (two kernels)	Records that Lean's default kernel and the nanoda kernel accept the CliqueFreeLog solution (251 s). The project reports two-kernel certification of 398 of 416 challenges of the collection.	Repository.
2026-10-11	Formal Conjectures pull request #7165	Catalogue (formal statements)	Adds Erdős Problem 802 with the research status "open", following the Erdős Problems page, together with the known bounds of Ajtai–Erdős–Komlós–Szemerédi, Shearer, Ajtai–Komlós–Szemerédi and Alon tagged as solved.	Open.
2026-10-11	K. Chen, arXiv:2610.15293v1, A note on the logarithmic exponent of Ramsey number r(4,t)	Uses	Combines recent lower bounds for the off-diagonal Ramsey numbers r(s, t) with fixed s ≥ 5 (citing preprints of the collection) with the recent proof of the AEKS independence conjecture. It deduces r(4, t) = t3/(log t)2+o(1). The note is "solely for informal circulation and will not be submitted for publication".	arXiv preprint (v1).

Notes

• The kernel checks listed above concern the formal statement logarithmic_independence_bound as written; the coloring result has no formal statement in the collection.
• As of the date above, the Erdős Problems page for problem 802 (last edited 26 October 2025) lists no proof claims.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.