---

Submission note. Posted to the site's forum by KJ_C on 28 April 2026:

Following the folklore counterexample noted by Zach Hunter, I used AI assistance (GPT-5.5 xhigh, with the proof checked by Claude Opus 4.7) to attempt the remaining case of Problem #180. The argument produces the following dichotomy, which I believe is correct but may already be known in the literature. I am posting here to ask whether this result is folklore, and if not, whether it constitutes progress.

Claim. Let $\mathcal{F}$ be a nonempty finite family of finite graphs with $\mathrm{ex}(n;H)=\Theta(n)$ for every $H\in\mathcal{F}$. Then exactly one of the following holds:

$\mathcal{F}$ contains, after deleting isolated vertices, both $K_{1,a}$ and $bK_2$ for some $a,b\geq 2$, and then $\mathrm{ex}(n;\mathcal{F})=\Theta(1)$;

$\mathcal{F}$ does not contain such a star/matching pair, and then $\mathrm{ex}(n;\mathcal{F})=\Theta(n)$.

The proof uses three ingredients: (1) the standard characterisation that $\mathrm{ex}(n;H)=\Theta(n)$ if and only if $H^\circ$ is a forest with at least two edges, proved via a random graph argument and a minimum-degree greedy embedding; (2) explicit constructions — $K_{1,n-1}$ or a perfect matching — for the lower bound in the second case; and (3) a maximum-matching/maximum-degree counting argument showing $e(G)\leq 2(a-1)(b-1)$ in the first case.

My questions: Is this dichotomy already in the literature? If so, could you point me to a reference? If not, does this constitute progress on Problem #180?

The full proof is shown below. This was generated with AI assistance and reviewed for logical consistency, but I am not a professional mathematician and welcome expert verification.

All graphs are finite and simple. Subgraph means not necessarily induced. For a graph $H$, let $H^\circ$ denote $H$ with isolated vertices deleted.

Lemma. $\mathrm{ex}(n;H)=\Theta(n)$ if and only if $H^\circ$ is a forest with at least two edges.

Proof. If $H^\circ$ has at most one edge, then every sufficiently large graph with at least one edge contains $H$, so $\mathrm{ex}(n;H)$ is eventually $0$.

If $H^\circ$ contains a cycle, let $h=|V(H^\circ)|$. Take $G\sim G(n,p)$ with $p=n^{-1+1/(2h)}$. Then $\mathbb{E}, e(G)=\Omega(n^{1+1/(2h)})$. The expected number of cycles of length at most $h$ is at most $\sum_{\ell=3}^h n^\ell p^\ell = \sum_{\ell=3}^h n^{\ell/(2h)} = O(n^{1/2})$. So some $G$ has $e(G)-X=\Omega(n^{1+1/(2h)})$ where $X$ counts short cycles. Deleting one edge from each short cycle gives an $H$-free graph with superlinear edges, so $\mathrm{ex}(n;H)$ is not $O(n)$.

Now suppose $H^\circ$ is a forest with $h=|V(H^\circ)|$ vertices and at least two edges. If $G$ has more than $(h-2)n$ edges, repeatedly delete vertices of degree at most $h-2$; if all were deleted, at most $(h-2)n$ edges were removed, contradiction. So some nonempty $G'\subseteq G$ has minimum degree at least $h-1$. Order $V(H^\circ)=x_1,\dots,x_h$ so each vertex has at most one earlier neighbor, and embed greedily into $G'$: at step $i$, the image of any earlier neighbor has at least $h-1$ neighbors of which fewer than $h-1$ are used, so an unused neighbor is always available. Hence $G$ contains $H^\circ$, giving $\mathrm{ex}(n;H)=O(n)$.

For the lower bound: if $H^\circ\cong K_{1,a}$ with $a\ge 2$, a perfect matching is $H$-free and has $\lfloor n/2\rfloor$ edges. If $H^\circ$ is not a star, then $K_{1,n-1}$ is $H$-free, since every nonempty subgraph of a star is again a star after deleting isolated vertices. In both cases $\mathrm{ex}(n;H)=\Omega(n)$. $\square$

Theorem. Let $\mathcal{F}$ be a nonempty finite family with $\mathrm{ex}(n;H)=\Theta(n)$ for every $H\in\mathcal{F}$. Then exactly one of the following holds:

(i) $\mathcal{F}$ contains, after deleting isolated vertices, both $K_{1,a}$ and $bK_2$ for some $a,b\ge 2$, and then $\mathrm{ex}(n;\mathcal{F})=\Theta(1)$;

(ii) $\mathcal{F}$ contains no such star/matching pair, and then $\mathrm{ex}(n;\mathcal{F})=\Theta(n)$.

Proof. By the Lemma, every $H^\circ$ with $H\in\mathcal{F}$ is a forest with at least two edges.

Case (ii). The upper bound is immediate: $\mathrm{ex}(n;\mathcal{F})\le\mathrm{ex}(n;H_0)=O(n)$ for any fixed $H_0\in\mathcal{F}$. For the lower bound: if no member of $\mathcal{F}$ is a star, then $K_{1,n-1}$ is $\mathcal{F}$-free, giving $\mathrm{ex}(n;\mathcal{F})\ge n-1$. If some member is a star but no member is a matching with at least two edges, then a maximum matching is $\mathcal{F}$-free, giving $\mathrm{ex}(n;\mathcal{F})\ge\lfloor n/2\rfloor$. Hence $\mathrm{ex}(n;\mathcal{F})=\Theta(n)$.

Case (i). Suppose $\mathcal{F}$ contains $K_{1,a}$ and $bK_2$ with $a,b\ge 2$. Let $G$ be $\mathcal{F}$-free. Then $\Delta(G)\le a-1$ and $\nu(G)\le b-1$. Let $M$ be a maximum matching; since $M$ is maximal, every edge of $G$ has an endpoint in $V(M)$. Therefore

$$> e(G)\le\sum_{v\in V(M)}d_G(v)\le|V(M)|\cdot\Delta(G)\le 2(b-1)(a-1). >$$

So $\mathrm{ex}(n;\mathcal{F})=O(1)$. Since every member of $\mathcal{F}$ has at least two edges, a single edge is $\mathcal{F}$-free, giving $\mathrm{ex}(n;\mathcal{F})\ge 1$. Hence $\mathrm{ex}(n;\mathcal{F})=\Theta(1)$. $\square$

Posted to the site's forum by KJ_C on 2 May 2026:

Quick formalization update. I've now formalized this dichotomy in Lean 4 (familiesTheorem): the file builds against Mathlib4, contains no sorry/admit, and#print axioms Erdos180.familiesTheorem reports only Lean's foundational axioms (propext, Classical.choice, Quot.sound).

Repo: https://github.com/arexychen/Erdos180

Two caveats I want to flag explicitly: (1) The single-forbidden-graph characterization (ex(n;H) = Θ(n) ↔ H° is a forest with ≥ 2 edges) is invoked only in the direction actually consumed by the dispatch:IsThetaLinear → ≥ 2 reduced edges. The forward direction (forest ⇒Θ(n)) and the forest conclusion are not consumed. A Phase 1 mathlib survey (phase1-report.md in the repo) records why the full classical biconditional could not be formalized within the time-box: the cycle case appears to require either a high-girth/high-chromatic-number existence theorem or random-graph short-cycle expectation plus a probabilistic deletion argument, none of which the survey found in mathlib4. The weakened axiom statement is provable from elementary case analysis on graphs with at most one non-isolated edge, which is what the formalization actually does. (2) The Case (i) bound in Lean is O(|V(F_star)| · |V(F_matching)|) rather than the tighter 2(a-1)(b-1) from the LaTeX. Both giveΘ(1), but explicit constants differ. This is a faithful formalization of the asymptotic statement, not of the specific constants. The Lean code was generated by GPT-5.5 (xhigh) under prompts I designed with Claude Opus 4.7 assistance. I am not a mathematician; the verification I did is structural (axiom audits, statement comparison against the LaTeX). Mathematical review by anyone with extremal graph theory background is welcome — the README lists specific things I would find most useful to hear about.

The claim. Let $\mathcal F$ be a nonempty finite family of finite graphs with $\mathrm{ex}(n;H)=\Theta(n)$ for every $H\in\mathcal F$; equivalently, every member is, after deleting isolated vertices, a forest with at least two edges. Then exactly one of two cases holds. (i) $\mathcal F$ contains, after deleting isolated vertices, both a star $K_{1,a}$ and a matching $bK_2$ with $a,b\ge2$; then $\mathrm{ex}(n;\mathcal F)=\Theta(1)$, with every $\mathcal F$-free graph having at most $2(a-1)(b-1)$ edges. (ii) $\mathcal F$ contains no such pair; then $\mathrm{ex}(n;\mathcal F)=\Theta(n)$. In case (i) no member satisfies $\mathrm{ex}(n;H)\ll_{\mathcal F}\mathrm{ex}(n;\mathcal F)$, and in case (ii) every member does, so the dichotomy decides Problem 180 for every such family: no for the families of case (i), which extend Hunter's folklore counterexample, and yes for those of case (ii).

Covers. Every finite family all of whose members have linear extremal number, other than the two-member star-and-matching families that the corrected Statement excludes. Families with a member containing a cycle, the subject of the no-forest variant and of the accepted disproof, are outside it.

Claimant and postings. Posted on the problem's thread by the account KJ_C on 28 April 2026 (post 5979), with the full proof in the post. The post says the argument was produced with GPT-5.5 (xhigh) and the proof checked with Claude Opus 4.7, and asks whether the dichotomy is folklore. The repository's dichotomy.tex, linked above and first committed on 2 May 2026, states the dichotomy with its proof; its README says Claude Opus 4.7 drafted it, and the note itself calls the result likely folklore. A reply of the same day (post 6000) says that a standard check found the dichotomy correct but modest and did not find it exactly in the literature; that is not a review of the proof. On 29 August 2026 post 8638 (the account Adenwalla) remarks that the argument shows more generally that a family containing a forest, but not both a star and a forest on more than two vertices, satisfies the conjecture.

Formalization. Post 6169 (2 May 2026) links the Lean 4 repository arexychen/Erdos180, linked above at a later pinned revision, whose README declares it a formalization of this dichotomy (Erdos180.familiesTheorem, with the structural variant familiesTheoremStructural) and says its Lean code was generated by GPT-5.5 (xhigh). The README and the post record two caveats: only one direction of the single-graph characterization ($\mathrm{ex}(n;H)=\Theta(n)$ exactly for forests with at least two edges) is formalized, and the general theorem's case (i) constant is weaker than the $2(a-1)(b-1)$ of the written argument, which is formalized only for the canonical star-matching pair. The README disclaims mathematical novelty for the dichotomy and priority for the problem's resolution. The development was not built or audited in this repository, so it gives no formalized evidence.

Depends on. Nothing in this wiki: the argument is self-contained apart from the standard greedy forest embedding and the random-graph lower bound it cites.

Standing. Claimed: no outside review, journal publication or Lean proof built here is known, and the site's curator does not mention the dichotomy.