Wiki
Wiki

Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated


Claim. There exist a fixed connected bipartite 22-degenerate graph HH and constants c,ε>0c,\varepsilon>0 with ex(n,H)≥c n3/2+ε\mathrm{ex}(n,H)\ge c\,n^{3/2+\varepsilon} for all sufficiently large nn. This is Theorem 1.2 of Chapter 10 of OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, technical report announced 1 August 2026 (the claim's date), PDF revised 6 August 2026; the corpus states it on its result page under the report's card. The chapter remarks (p. 237) that Janzer's construction disproved only the reverse implication of the equivalence of Problem 113 and that this theorem refutes the forward one. The site labels Problem 146 disproved by the same theorem, which is recorded on that problem's claim page.

The forward implication of the equivalence, that every 22-degenerate bipartite graph HH has ex(n,H)=O(n3/2)\mathrm{ex}(n,H)=O(n^{3/2}), is false: the theorem's HH is 22-degenerate and bipartite, and c n3/2+εc\,n^{3/2+\varepsilon} exceeds every O(n3/2)O(n^{3/2}) bound for large nn. The theorem therefore disproves the equivalence the problem asserts on its own. The reverse implication is not addressed; its disproof is Janzer's accepted claim, which already settles the problem.

Depends on. OpenAI's claim page for Problem 146, which records the same theorem and its standing.

Acceptance. Reviewed: the site's curator, Thomas Bloom, accepts this theorem in labeling Problem 146 DISPROVED (LEAN) and crediting the connected bipartite 22-degenerate graph to OpenAI (erdosproblems.com/146, page last edited 31 August 2026), as recorded on the Problem 146 claim page; the forward implication of this problem follows from it in one line. The site's thread for Problem 113 carries a comment of 1 August 2026 pointing to the chapter's remark, but the site's page (last edited 19 October 2025) credits the disproof to Janzer only. The release's own README says that its manuscripts were produced by an internal OpenAI model and are at different stages of verification. No refereed publication, arXiv version or written independent expert review is recorded. The result page records its reading depth, the statement and construction checked clause by clause and the proof for structure only. The accompanying Lean file CompactnessAndDegeneracy.lean of openai/ten-proofs at the pinned commit states Theorem 1.2, strengthened by a degree condition, as twoDegenerateExtremalCounterexample and derives not_erdos_146 from it against its own degeneracy definition. formal-conjectures states the theorem as erdos_146.variants.two_degenerate_counterexample in its 146.lean, added 2026-08-07, and registers this file as its formal proof; its erdos_113, which states the equivalence, registers only the formalization of Janzer's direction. This corpus has neither built nor audited the file. The problem's standing is also fixed by Janzer's accepted claim and does not depend on this page.