The claim. For every integer $r\ge4$ there is a constant $c_r>0$ such that every finite simple $K_r$-free graph $G$ on $n$ vertices with average degree $d=2|E(G)|/n\ge2$ satisfies

with the natural logarithm (Theorem 1.1 of OpenAI, A logarithmic independence bound for clique-free graphs, OpenAI Math Release preprint, 25 September 2026, at the pinned revision of the release repository linked above, paged at the result page of its card). The constant depends on $r$ alone, uniformly in $n$ and $d$; the proof gives $c_r=1/(16D_r)$ for an existence constant $D_r$ it does not optimize. The manuscript names Problem 802 as the question it answers. In the site's letters ($t=d$) this is the displayed bound $\gg_r\frac{\log t}tn$ of Problem 802 for every fixed $r\ge4$. The case $r=3$ is the 1980 theorem of Ajtai, Komlós and Szemerédi and also follows from the $r=4$ instance with the same constant, because a triangle-free graph is $K_4$-free (Mathlib's SimpleGraph.CliqueFree.mono); that one-line step is not a declaration in the release, so a reader citing the theorem for $r=3$ should name it. The origin's convention $\log x=\max\{1,\ln x\}$ follows with the constant $c_r\ln2$, since $\ln t\ge(\ln2)\max\{1,\ln t\}$ for $t\ge2$. The proof (Sections 2--6 of the manuscript) maximizes an entropy-minus-edges functional over vertex weights, bounds the weighted triangle count of a maximizer by its weighted edge count through an entropy and vertex-splitting argument, deduces the maximum-degree bound of Proposition 6.1 by deleting closed neighborhoods, and passes to average degree by discarding the vertices of degree above $2d$; the manuscript says its companion release manuscripts on Ramsey numbers are not inputs.

The formalization. The release's Lean tree (folder lean/ at the pinned revision, Lean v4.34.1 with the release's pinned Mathlib) proves

theorem logarithmic_independence_bound (r : ℕ) (hr : 4 ≤ r) :
    ∃ c : ℝ, 0 < c ∧
      ∀ {V : Type} [Fintype V] (G : SimpleGraph V),
        G.CliqueFree r → 2 ≤ averageDegree G →
        c * (Fintype.card V : ℝ) * Real.log (averageDegree G) / averageDegree G ≤
          (G.indepNum : ℝ)

as OAI.CliqueFreeLog.logarithmic_independence_bound in OAI/Combinatorics/CliqueFree/Main.lean, with OAI.CliqueFreeLog.averageDegree (OAI/Combinatorics/CliqueFree/Model.lean) the real number $2|E|/|V|$, which is $0$ on an empty vertex type, a case the hypothesis $2\le$ average degree excludes. The comparator challenge ComparatorChallenges/CliqueFreeLog.lean, with its configuration CliqueFreeLog.json, pins the declaration OAI.CliqueFreeLog.logarithmic_independence_bound (its definition_names list is empty) and carries a byte-identical copy of averageDegree, and it permits only the axioms propext, Quot.sound and Classical.choice; the release's catalog lean/formalization.yaml lists the declaration under this manuscript.

Depends on. Nothing in this wiki: the proof is self-contained in the manuscript and its Lean tree, and the Lean statement rests on Mathlib's CliqueFree, indepNum and Real.log alone.

Acceptance. Formalized: this corpus's verification built the solution module and the comparator challenge from the release at the pinned revision, printed the axioms of the declaration, which were exactly propext, Classical.choice and Quot.sound, and found the comparator fingerprint of the pinned challenge statement identical to the solution's; the result was recorded on 2026-10-07. The statement audit that formalized requires is this corpus's own: a statement-fidelity audit compared the declaration clause by clause with the problem page's Statement and Formulation (the range of $r$, the dependence of the constant, the graph class, the degree range, the conclusion and the absence of hidden hypotheses) and judged it an exact formal statement of the question for $r\ge4$, with the $r=3$ case supplied by CliqueFree.mono as above and the logarithm convention changing only the constant. Not reviewed: no outside reviewer or independent acceptance is recorded. Not refereed: the manuscript is an unrefereed release preprint with no arXiv version; the release's README says that its manuscripts and proof artifacts were produced by an internal OpenAI model and that the collection includes results at different stages of verification, so the claimant is the organization; the site's label is OPEN with an empty proof-claims tab and no file for the problem exists in formal-conjectures. Only the pinned revision is described.