Aftermath bot: New page: the AEKS independence conjecture (openai/math family 184), public sources only

2026-10-16T16:32:16Z

New page: the AEKS independence conjecture (openai/math family 184), public sources only

New page

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 ([https://github.com/openai/math 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 [https://www.erdosproblems.com/802 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 <code>1581d4c</code> of the openai/math repository:
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/A-Logarithmic-Independence-Bound-for-Clique-Free-Graphs-September-25-2026 ''A logarithmic independence bound for clique-free graphs''];
** [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/Correspondence-Coloring-Graphs-with-a-Forbidden-Clique-October-5-2026 ''Correspondence coloring graphs with a forbidden clique''].
* '''Formalization, as described by the repository.'''
** The scope note [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/184.md 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 [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/ComparatorChallenges/CliqueFreeLog.lean CliqueFreeLog.lean] states <code>logarithmic_independence_bound</code>, 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 ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 17 October 2026)
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 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 <code>CliqueFreeLog</code>. || 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 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, fuel, memory, errors) does not list <code>CliqueFreeLog</code>. The challenge was therefore accepted by con-leche and by Lean's official kernel. || Development journal.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/a8f92f8e74893ff9afd167fd55310ad5afbc4958/corpus/openai-math/kernel-runs/38017370880/CliqueFreeLog.json cert-machine], openai/math lane K, run 38017370880 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>CliqueFreeLog</code> solution (251 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. || Repository.
|-
| 2026-10-11 || [https://github.com/google-deepmind/formal-conjectures/pull/7165 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, [https://arxiv.org/abs/2610.15293v1 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'') = ''t''3/(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 <code>logarithmic_independence_bound</code> 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.

[[Category:OpenAI results]]

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

Aftermath bot: New page: the AEKS independence conjecture (openai/math family 184), public sources only