TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Mantel's theorem: $ex (n, K_{3}) = ⌊ n^{2} / 4 ⌋$ , uniquely attained by $T_{n, 2}$

Statement

For every $n \in N$ ,

$ex (n, K_{3}) = ⌊ \frac{n^{2}}{4} ⌋ = e (T_{n, 2}) .$

Every triangle-free graph on $n$ vertices has at most this many edges, and equality holds exactly for a graph isomorphic to the balanced complete bipartite graph $T_{n, 2}$ .

Facts & Assumptions

Given: The hypotheses and notation of the statement above.

[F1]

$ex (n, H)$ is the maximum edge count of an $n$ -vertex graph with no ordinary copy of $H$ (Ordinary-subgraph extremal number $ex (n, H)$ , Turán graph $T_{n, r}$ , and balanced blowup $H [s]$ ).

[F2]

The open neighbourhood is $N_{G} (v) = {u : {u, v} \in E}$ and $\deg_{G} (v) = ∣ N_{G} (v) ∣$ (Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree).

[F3]

Writing $n = q r + a$ with $0 \leq a < r$ , $e (T_{n, r}) = (\binom{n}{2}) - a (\binom{q + 1}{2}) - (r - a) (\binom{q}{2})$ ; among complete $r$ -partite graphs on $n$ vertices this is the maximum edge count, and equality holds exactly when all part sizes differ by at most $1$ (The exact edge count of $T_{n, r}$ and the unique balancing maximum among complete $r$ -partite graphs).

Proof

technique · induction after deleting the ends of an edge

1.1

The assertion is immediate for $n = 0, 1, 2$ . Assume it, including uniqueness, for $n - 2$ , and let $G$ be a triangle-free $n$ -vertex graph. If $G$ has no edge its bound is immediate. Otherwise choose an edge $u v$ . No vertex other than $u, v$ is adjacent to both ends, so $d (u) + d (v) \leq n$ .

givenF1F2

2.1

Delete $u, v$ to obtain a triangle-free graph $G^{'}$ . The removed edges number $d (u) + d (v) - 1$ , so $e (G) \leq ⌊ (n - 2)^{2} / 4 ⌋ + n - 1 = ⌊ n^{2} / 4 ⌋$ . The graph $T_{n, 2}$ is triangle-free and has the last edge count, proving the exact maximum.

step 1.1givenF1F3

3.1

Suppose equality holds. Then $G^{'} ≅ T_{n - 2, 2}$ , $d (u) + d (v) = n$ , and every other vertex is adjacent to exactly one of $u, v$ . In each part of $G^{'}$ , triangle-freeness forces all vertices to choose the same endpoint: two vertices in opposite parts choosing the same endpoint would form a triangle with their cross edge. Hence adjoining $u$ to one part and $v$ to the other makes $G$ complete bipartite.

step 1.1step 2.1

4.1

Its two part sizes sum to $n$ and its product is $⌊ n^{2} / 4 ⌋$ ; the balancing equality in the preceding lemma forces them to differ by at most $1$ . Thus $G ≅ T_{n, 2}$ . Conversely that graph has equality, completing the induction and the uniqueness proof.

step 3.1givenF3

5.1

Steps 1.1-4.1 prove Mantel's theorem independently of Turán's theorem, for all $n$ and with equality fully characterized.

step 1.1step 2.1step 3.1step 4.1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 23 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Yufei Zhao, Graph Theory and Additive Combinatorics (standard reference, not scraped)

Mantel's theorem: ex⁡(n,K3)=⌊n2/4⌋ex(n,K3​)=⌊n2/4⌋, uniquely attained by Tn,2Tn,2​