What was already known
Ajtai, Komlós and Szemerédi proved the logarithmic order for triangle-free graphs. Ajtai, Erdős, Komlós and Szemerédi conjectured it for every fixed forbidden clique. Shearer's general K_r-free average-degree lower bound retained a log-log d denominator; later structural results had additional hypotheses.
AI involvement
OpenAI credits an internal model with the result and is the manuscript's author. The earlier conjecture and bounds are human work; no human proof check of the manuscript is reported.
OpenAI authors and releases the full claimed bound as internal-model work; autonomy beyond that is undocumented.
Importance
Claims the fixed-clique-size average-degree bound conjectured by Ajtai, Erdős, Komlós and Szemerédi.
Limitations
The bound holds for each fixed r≥4 and average degree d≥2, with a constant depending on r. It does not optimize that constant or provide an efficient algorithm. The documented independent check builds and audits the Lean statement, not the prose proof.
Technical verification
The release catalog and family scope note identify a Lean proof of precisely the r ≥ 4 average-degree statement. A dated independent Erdős Problems audit reports building the solution and challenge, checking only the standard Lean axioms, and matching statement fingerprints. This verifies the formal theorem, not a separate hand review of every manuscript step.
Formal checking
Built OAI.CliqueFreeLog.logarithmic_independence_bound and comparator challenge; checked axioms and statement fingerprint
- Checker
- Erdős Problems claim-audit corpus, independent of the release
- Scope
- For every fixed r ≥ 4, K_r-free graphs of average degree d ≥ 2 satisfy α(G) ≥ c_r n log d/d
- Basis
- Reported by the linked checker
Checking a formal statement does not establish that it matches the original problem.
Human understanding
The manuscript gives a proof outline and a later audit maps its structure, but no identified human author explains the central entropy and splitting mechanism from an independent understanding review; this is a missing-evidence default.
Correction and publication history
Claims the fixed-clique-size average-degree bound conjectured by Ajtai, Erdős, Komlós and Szemerédi.
Read this published revision