Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
OpenAI, Ten Advances in Mathematics and Theoretical Computer Science, technical report announced 1 August 2026 with its original PDF (the claim's date; linked above), PDF revised 6 August 2026, the version cited; Chapter 10, Counterexamples to the Compactness and Degeneracy Conjectures for Extremal Numbers, Theorem 1.2, printed pp. 237--238. 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, and the chapter names no individual author. Library pages: the card and the result page.
The result. A graph is -degenerate when every nonempty subgraph has a vertex of degree at most , the form equivalent to the problem's induced-subgraph wording. Theorem 1.2: there exist a fixed connected bipartite -degenerate graph and constants with
for all sufficiently large . The problem asserts for every and every bipartite -degenerate ; at the asserted bound is , which exceeds for large , so the universal statement fails at the pair and the problem is disproved. The graph is built in layers: of size , , each vertex joined to its two parents; the lower bound comes from a random induced subgraph of a bipartite Hamming-ball graph, which Proposition 8.1 shows is -free by an entropy-potential argument, with a second-moment edge count and padding giving (pp. 247--248). The problem page's Current assessment records the reading depth: statements and the construction were checked clause by clause, the proof was read for structure only, and no step was checked.
Depends on. Nothing in this wiki; the argument is self-contained within the chapter, and the problem page's account rests on this claim.
Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem DISPROVED (LEAN) and wrote the commentary crediting the disproof to an internal model at OpenAI, with the connected bipartite -degenerate and the exponent (erdosproblems.com/146, accessed 2026-09-18; the page was last edited 31 August 2026, and the community database lists the status disproved (Lean) as of its last update, dated 2 August 2026, without recording when the state changed, so the day of the relabel itself is not established); Bloom took no part in the report. That documented acceptance by the site is the only acceptance evidence: no refereed publication, no arXiv version and no written independent expert review of the argument were found on 2026-09-18 (the problem page's search scope), so the standing rests on the site's acceptance of an AI-generated argument, and nothing is independently reviewed in this repository. A refereed version, an independent whole-argument review or a build of the formal proof checked against the problem's statement would add evidence.
Formalization, not evidence. The file CompactnessAndDegeneracy.lean of
openai/ten-proofs at the pinned commit (linked above) proves
not_erdos_146 against its own DegeneracyConjectureStatement, and the
formal-conjectures statement file recorded on the problem page points to it
through a formal_proof attribute. The file contains no sorry, axiom
or native_decide, the corpus has not built or audited it, and the two
files' degeneracy definitions were not bridged, so it is listed as a link
and not as formalized evidence.