---

Claim. The statement of Problem 579 is false. For every $c>0$ and every threshold $N$ there is a $K_{2,2,2}$-free graph on some $n\ge N$ vertices with at least $(3/2048)n^2$ edges and independence number below $cn$. So no constant $c(\delta)$ exists for any $\delta\le3/2048$, and in the sources' language $\mathrm{RT}(n;K_{2,2,2};o(n))$ is not $o(n^2)$: the question of Balogh and Lenz whether $\theta(K_{2,2,2})=0$, and Problem C of Liu, Reiher, Sharifzadeh and Staden, are answered in the negative. Together with Theorem 1 of Erdős, Hajnal, Sós and Szemerédi (1983), which gives the statement for $\delta>1/8$, the Ramsey--Turán density $\theta(K_{2,2,2})$ lies in $[3/2048,1/8]$.

The result. The claim is a Lean 4 file submitted to the bounty site Conjectures.io against its task for this problem (task type disprove). The formal target is the formal-conjectures statement Erdos579.erdos_579, quoted under Formalization on the problem page, with its open answer fixed to true; the problem page's Formulation paragraph reads that statement as the problem's Statement clause for clause. The file proves the exact negation of the target from a lemma whose statement restates the universal assertion, by an explicit finite construction: Boolean-cube stages, masked compatibility graphs and random perfect-matching realizations assemble, for every $c>0$ and every $N$, an octahedron-free graph on $n\ge N$ vertices at the fixed unordered edge density $3/2048$ with independence number below $cn$. The record credits the proof to the solver Jordan; the file's copyright headers credit one author writing with OpenAI Codex, and its preamble says that selected portions are modified from the TCSlib and FABL Lean libraries. The file (810,011 bytes, 18,336 lines, its dependencies bundled as source) has a target, a pinned-statement definition and final theorems consistent with the site's statement, and contains no sorry, axiom, native_decide, unsafe or set_option, as the problem page records.

Acceptance. The accepting body is Conjectures.io, and its record is the evidence listed as reviewed: the site's Lean kernel verified the proof (the submission was accepted into verification at 18:12:32 UTC and production verification completed at 18:19:42 UTC), its review approved the record under its policy v3, and it certified the record on 6 October 2026 with the reward paid. The record's review decision states that the submission refutes the problem by the construction described above, that the committed formal statement matches the intended conjecture, that the Lean kernel, the statement comparator and the permitted-axiom check (propext, Quot.sound, Classical.choice) passed in the production run and in a separate isolated replay, that the review covered the critical interfaces and bounded prior-work searches rather than every auxiliary lemma, that two AI assessments from separate contexts supported approval, and that a human reviewer authorized the decision; the site's second, independent kernel was not run for this task. This is documented acceptance by one site, not a referee's report and not a journal publication. The evidence is not listed as formalized: this corpus has not built the file, so the kernel check is the site's alone, the construction is not recomputed, and the clause-for-clause reading of the formal statement on the problem page is not a fidelity audit. No refereed publication, no erdosproblems.com acceptance and no formal-conjectures catalog agreement was found: on 2026-10-06 the site's page labeled the problem OPEN with no proof claim, and the catalog's default branch carried the statement with answer(sorry) under research open.