Claim. For every $\eta>0$ there is a finite 3-regular bipartite graph $H$ with $\operatorname{ex}(n,H)=O(n^{4/3+\eta})$. This is Theorem 1.4 of O. Janzer, Disproof of a conjecture of Erdős and Simonovits on the Turán number of graphs with minimum degree 3, Int. Math. Res. Not. IMRN 2023, no. 10, 8478--8494, first posted as arXiv:2109.06110 on 2021-09-13; the corpus states and proves it on its result page, from the explicit graph [[../library/extremal_graph_theory/janzer_2023_disproof_conjecture_erdos_simonovits_turan_number/construction_h_k_l|$H_{k,\ell}$]] and the bound of Theorem 1.6.

Take $0<\eta<1/6$. Then $\operatorname{ex}(n,H)=O(n^{4/3+\eta})=o(n^{3/2})$, so $H$ satisfies the upper bound in Problem 113, while $H$ is an induced subgraph of itself with minimum degree three, so $H$ is not 2-degenerate. The implication from the upper bound to 2-degeneracy therefore fails, and the equivalence the problem asserts is false. The other direction, that every 2-degenerate bipartite graph has Turán number $O(n^{3/2})$, is not decided by this construction; its refutation (OpenAI, Chapter 10, Theorem 1.2), accepted on the site's crediting of the same theorem for Problem 146, is recorded on its own claim page.

Depends on. Nothing in this wiki.

Acceptance. The paper is a refereed publication in International Mathematics Research Notices, published online 2022-04-26 (the refereed evidence), and the site's curator, Thomas Bloom, records the problem as disproved by it (the reviewed evidence; Bloom took no part in the paper). The corpus's source card reconstructs the complete same-paper chain from the arXiv v2 manuscript with two compilation-supplied qualifications (a larger smallness constant in Lemma 2.5 and a diagonal-free restriction of Lemma 2.19), each covered by a bounded independent review, and leaves Lemmas 2.1--2.4 and 2.6--2.8 as stated external inputs; that is not a whole-proof independent review. The acceptance recorded here rests on the publication and the site's acceptance.

Formalization. The file src/latest/ErdosProblems/Erdos113.lean of Boris Alexeev's plby/lean-proofs repository, at the commit linked above, declares itself a formalization of this result: it names Janzer as the informal author, names Codex and GPT-5.6 Sol as its formal authors, records the toolchain as Lean 4.33.0 with Mathlib v4.33.0, and carries a header stating that its original license is Apache 2.0 and that the file has been modified. In the namespace Erdos113 it declares

theorem not_erdos_113 :
    ¬ (∀ (V : Type) [Fintype V], ∀ H : SimpleGraph V,
      H.IsBipartite → (HasThreeHalvesExtremalBound H ↔ IsTwoDegenerate H))

proved through janzerGraph, a graph the file shows to be 3-regular, bipartite and not 2-degenerate, with an extremal bound of exponent $31/21<3/2$. Its first commit in the repository is dated 2026-08-17. This corpus has not built the development, printed its axioms, or audited the definitions HasThreeHalvesExtremalBound and IsTwoDegenerate against the problem statement; only the declared statement at the pinned commit is described. The development is therefore a link on this page and no formalized evidence.