Wiki
Wiki

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

Updated

Problem 147

../

claims/: The 2 claim pages of Problem 147, one per claimant's result; the problem's standing derives from them.


Statement. If HH is bipartite with minimum degree rr then there exists ϵ=ϵ(H)>0\epsilon=\epsilon(H)>0 such that

ex(n;H)≫n2−1r−1+ϵ.\mathrm{ex}(n;H) \gg n^{2-\frac{1}{r-1}+\epsilon}.

Status. DISPROVED (LEAN). The site's commentary (page last edited 18 January 2026) credits Janzer's rainbow Turán paper [Ja23] with the disproof for even r≥4r\ge4 and his later paper [Ja23b] with the case r=3r=3; both are refereed, and each is recorded as an accepted claim on the blow-up page and the 3-regular page. The site's label is DISPROVED (LEAN); the external Lean proof it refers to is linked, unverified, under Formalization below.

Source. erdosproblems.com/147, accessed 2026-09-04. Cite as: T. F. Bloom, Erdős Problem #147, https://www.erdosproblems.com/147.

References.

  • [ErSi84] Erdős, P. and Simonovits, M., Cube-supersaturated graphs and related problems. Progress in graph theory (Waterloo, Ont., 1982) (1984), 203-218.
  • [Ja23] Janzer, Oliver, Rainbow Turán number of even cycles, repeated patterns and blow-ups of cycles. Israel J. Math. 253 (2023), 813-840.
  • [Ja23b] Janzer, Oliver, 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), 8478-8494.

Formalization. Statement in formal-conjectures, which carries a formal_proof attribute naming Erdos147.lean in Boris Alexeev's lean-proofs, a refutation of the universal statement through the single witness C12[2]C_{12}[2], the bipartite 44-regular graph with upper exponent 139/84<5/3139/84<5/3 at minimum degree 44; its header names Janzer as informal author and the AI systems Codex and GPT-5.6 Sol as formal authors, and it is linked on the blow-up claim page. The corpus has not built or audited it, and no acceptance is claimed from it.

Current assessment

Janzer's published Theorem 1.4 supplies the disproof: choosing 0<η<1/60<\eta<1/6 gives r=3r=3 counterexamples with upper exponents incompatible with the proposed lower bound. The linked result records the exponent comparison and same-paper dependency chain, with external inputs separate. This page records neither a dated broader status search nor independent proof-review coverage. The site's label DISPROVED (LEAN) refers to an external, unverified Lean proof that refutes the statement through the minimum-degree-44 witness C12[2]C_{12}[2], linked above; [Ja23] is credited by the site with the even case r≥4r\ge4 and has its own claim page, but it remains outside the direct-proof compilation, which rests on [Ja23b] alone. The two claim pages carry the acceptance evidence (refereed publication and the site's credit) from which the frontmatter standing is derived.

Progress

Janzer's [[../library/extremal_graph_theory/janzer_2023_disproof_conjecture_erdos_simonovits_turan_number/theorem_1_4_e147|Theorem 1.4]] constructs, for every η>0\eta>0, a 3-regular bipartite graph HH with

ex⁡(n,H)=O(n4/3+η).\operatorname{ex}(n,H)=O(n^{4/3+\eta}).

For r=3r=3, the proposed lower bound has exponent 3/2+ϵ(H)3/2+\epsilon(H). Taking η<1/6\eta<1/6 gives an incompatible upper exponent, so this one family directly disproves the universal statement. The linked result page records the exact exponent comparison and the complete same-paper dependency chain, with external inputs stated separately. The published theorem statement independently supplies the status evidence.

Known Results

  • [[../library/extremal_graph_theory/janzer_2023_disproof_conjecture_erdos_simonovits_turan_number/theorem_1_4_e147|Janzer's direct r=3r=3 disproof]] derives the counterexample from the explicit Hk,ℓH_{k,\ell} construction and Theorem 1.6.
  • [[../library/extremal_graph_theory/janzer_2023_disproof_conjecture_erdos_simonovits_turan_number/_index|Source record]] cites arXiv v2 of 8 November 2021, which its locators follow, and the published DOI.

[Ja23]'s Turán bound for the blow-up C2k[r]C_{2k}[r] is a second, independent disproof, recorded on its claim page; the direct-proof compilation covers [Ja23b] only.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.