Erdős Problem #802
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
Attempts
submit one →Read our full write-up →
In 1981 Ajtai, Erdős, Komlós and Szemerédi asked whether every K_r-free graph with n vertices and average degree t has an independent set of size at least c_r·n·log t/t. Ajtai, Komlós and Szemerédi had just proved this for triangle-free graphs. This is Erdős problem #802. The 1981 paper's own bound had log log t in place of log t, and Shearer's 1995 bound n log t/(t log log t) had stood since. OpenAI's 6 October release claims the conjecture for every r ≥ 4. The proof chooses vertex weights that maximize an entropy-minus-edge-mass potential, deletes closed neighbourhoods one at a time, and needs only that the weighted triangle mass is at most a constant times the edge mass. Clique exclusion enters once, through random multipliers that keep each weight in expectation. Fed into the maximizer's variational inequality, they bound the weighted edge mass between any two vertex sets of bounded weight, and a separate theorem turns that bound into the triangle estimate by splitting vertices along random walks inside their neighbourhoods. We read all six sections line by line and found no gap. Hostile AI referee seats on §2 with §6, on §§3–5, on the Lean against the paper, and on the sources found none either; the two on the mathematics logged eight exposition notes between them. OpenAI's Lean proof of the comparator's theorem (31 modules) replays on our machine with the standard axioms and a matching statement. A kernel-checked bridge of ours carries it to a verbatim copy of Formal Conjectures' erdos_802, which is still marked open and asks for more: every r, and no lower bound on the average degree. Nothing in the theorem is ours.
CLOSED