---

The claim. There is a finite nonempty family $\mathcal F$ of connected bipartite graphs, every member containing a cycle, with $\mathrm{ex}(n;\mathcal F)=O(n^{4/3-1/48})$ and $\mathrm{ex}(n;F)=\Omega(n^{4/3})$ for every $F\in\mathcal F$ (Theorem 1.1, Failure of compactness, of Chapter 10 of OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, technical report announced 1 August 2026, PDF of 6 August 2026, printed p. 237). No member of such a family satisfies $\mathrm{ex}(n;F)\ll_{\mathcal F}\mathrm{ex}(n;\mathcal F)$, so the family answers Problem 180 in the negative and, because every member contains a cycle, also disproves the no-forest form of the conjecture (Wigderson's p. 2 Conjecture), the variant the problem page keeps out of the statement and Problem 575 records. The statement, definitions and the four-line proof from Propositions 3.4 and 4.3 are paged at claims-checked depth on the result page; the eight sections of proof were read for structure only and no step was checked. The report's author is OpenAI; its announcement attributes the arguments to an internal model and the manuscript's preparation to humans working with that model.

The formalization. The repository openai/ten-proofs holds CompactnessAndDegeneracy.lean, whose CompactnessConjecture namespace ends in not_erdos_180 : ¬ CompactnessConjectureStatement at lines 8967--8970 of the commit the site's page links (18,588 lines, Mathlib only, no sorry, axiom or native_decide). At that commit CompactnessConjectureStatement says that every nonempty family with no acyclic member (IsCyclicFamily) is compact (IsCompactFamily: some member $F$ and some $C>0$ have $\mathrm{ex}(n;F)\le C\,\mathrm{ex}(n;\mathcal F)$ for all sufficiently large $n$), so not_erdos_180 refutes the no-forest form, with the comparison holding for all sufficiently large $n$. A family with no acyclic member that is not compact also refutes the corrected Statement, which excludes only star-and-matching pairs, so the Lean theorem implies the negative answer to Problem 180. The thread post of 1 August 2026 links the same file at an earlier commit, lines 8980--8983; only the later pin, the one the site links, is linked above. formal-conjectures names this file as the formal_proof of its variant erdos_180.variants.counterexample, as the problem page records. Nothing was built, axiom-audited or kernel-checked in this repository and no statement-fidelity review was commissioned, so the file is a link and not formalized evidence.

Acceptance. Reviewed: the site's curator, Thomas Bloom, labeled the problem DISPROVED (LEAN) and wrote in its commentary that an internal model at OpenAI disproved it, pointing to the remarks under Problem 575 (erdosproblems.com/180, last edited 31 August 2026); Bloom took no part in the report, so the credit is independent of the claimant. The same theorem is accepted on the same kind of credit on Problem 575's page. That documented acceptance is the only acceptance evidence: the report has no refereed publication, the problem's thread holds no curator post, and no written independent review of the argument is known. The printed wording is also answered by the two-forest counterexample, which the report records on p. 237 as the folklore refutation of the original formulation; that family is one the corrected Statement excludes, so its page is rejected.

Depends on. Theorem 1.1 of Chapter 10 of the report, the claimant's own argument, read at claims-checked depth.