---

The claim. OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, technical report announced 1 August 2026 and revised 6 August 2026 (the version carded at its library home); Chapter 10, Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers, printed pp. 236--249, carded at chapter_10/. The report's author is OpenAI; its announcement attributes the arguments to an internal model and the manuscript's preparation to humans working with it, and the release's own README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification, not all with Lean formalizations. Theorem 1.1 (p. 237, paged at theorem_1_1) gives a finite nonempty family $\mathcal F$ of connected bipartite graphs, every member containing a cycle, with

$$\mathrm{ex}(n,\mathcal F)=O\bigl(n^{4/3-1/48}\bigr) \qquad\text{and}\qquad \mathrm{ex}(n,F)=\Omega\bigl(n^{4/3}\bigr)\quad(F\in\mathcal F).$$

The family (Definition 2.5, p. 238) is $\{C_4,C_6\}$ together with the admissible quotients of two templates built from the one-subdivisions of $K_{3,2}$ and $K_{3,3}$; the upper bound is Proposition 3.4 (p. 240), by counting short paths after a girth-eight bipartite reduction, and the lower bounds are Proposition 4.3 (p. 242), from incidence graphs of symplectic generalized quadrangles in characteristic $2$ or $3$. Every member is bipartite and none is a forest, so the family meets the site's hypothesis and refutes the displayed comparison for every member $G$ and every constant: the statement is false in full, by a power of $n$ rather than an unbounded factor, and the no-forest form of the conjecture (Wigderson's p. 2 Conjecture, the report's display (1)) falls with it. The report's statement is asymptotic, for all sufficiently large $n$, which suffices against the site's comparison, which the problem page's Formulation reads as holding for all $n$, since a bound holding for all $n$ would hold eventually.

Acceptance. Reviewed: the site's curator, Thomas Bloom, relabeled the problem DISPROVED on 31 August 2026 and wrote the commentary crediting the disproof to an internal model at OpenAI, with the family's properties and the exponent $4/3-1/48$ (erdosproblems.com/575, accessed 2026-10-07; a forum comment of 1 August 2026 had reported the chapter); Bloom took no part in the report. That documented acceptance by the site is the only acceptance evidence: no refereed publication, arXiv version or written independent review of the argument was found on 2026-09-18 (Crossref and arXiv queries recorded on the problem page), and the standing therefore rests on the site's acceptance of an AI-generated argument. The statement, the definitions and the four-line proof of Theorem 1.1 were read clause by clause, and the proofs of Propositions 3.4 and 4.3 were read for structure only, with no step checked; no step is independently reviewed in this corpus.

Formalization, not evidence. The file CompactnessAndDegeneracy.lean of openai/ten-proofs at the pinned revision (linked above; the revision the thread pins is no longer served) proves not_erdos_180 : ¬ CompactnessConjectureStatement for the cyclic-family form, with the comparison holding for all sufficiently large $n$, under the name of Problem 180; it imports only Mathlib and contains no sorry, axiom or native_decide. The corpus has not built or audited the file, and no statement in it names this problem, so it is listed as a link and not as formalized evidence.

Depends on. Nothing in this wiki: the argument is the report's, read at claims-checked depth on its library pages.