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 -degenerate graph and constants with for all sufficiently large . 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 -degenerate bipartite graph has , is false: the theorem's is -degenerate and bipartite, and exceeds every bound for large . 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 -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.