Graph Theory

Motivation

The generalized Turán number $\mathrm{ex}(n,H,\mathcal F)$ is the largest number of copies of a graph $H$ in an $n$-vertex graph containing no member of a family $\mathcal F$. With $H=K_2$ it is the classical Turán number; the systematic study of general $H$ began with Alon and Shikhelman (2016), and cycles are its most studied case: Bollobás and Győri bounded $\mathrm{ex}(n,C_3,C_5)$, and Gerbner and Palmer determined $\mathrm{ex}(n,C_l,K_{2,t})$.

Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (J. Combin. Theory Ser. B, 2020; arXiv:1712.07079), count copies of one cycle in graphs avoiding another. For even cycles they show $\mathrm{ex}(n,C_{2l},C_{2k})=\Theta(n^l)$. Most extremal constructions there are bipartite, so they also study the bipartite generalized Turán number. For the first non-trivial pair, six-cycles in a graph avoiding eight-cycles, they determine its leading term exactly. This mission formalizes that result, Theorem 12 of the paper.

Setting

All graphs are finite and simple. A $k$-cycle $C_k$ is a cycle with $k$ vertices. A copy of $C_k$ in $G$ is a subgraph of $G$ isomorphic to $C_k$; $\mathcal N(C_k,G)$ is the number of copies, so a cycle is counted once regardless of its starting point and direction. A graph is $C_8$-free if no subgraph of it is isomorphic to $C_8$ (induced or not). A graph is bipartite if its vertices can be split into two classes $A$ and $B$ with every edge joining $A$ to $B$.

$$\mathrm{ex}_{bip}(n,C_6,C_8)=\max\{\mathcal N(C_6,G) : G \text{ bipartite},\ C_8\text{-free},\ |V(G)|=n\}.$$

The proof works with a fixed bipartition $(A,B)$ of a $C_8$-free graph $G$ and uses the following notions.

• $N(u,v)$ is the set of common neighbours of $u$ and $v$.
• A pair $\{u,v\}$ is fat if $|N(u,v)|\ge 4$.
• A 6-cycle is fat if it contains a fat pair from each class.
• A pair is marked if it has exactly three common neighbours.
• A 4-set $F\subseteq A$ is nice if its four vertices have three common neighbours in $B$, i.e. they span a $K_{4,3}$.
• For $x,y,z\in A$, $h(x,y,z)$ is the number of 6-cycles through all three. The triple is good if $h\le 6$ and bad otherwise.
• A hypergraph is Berge-$C_4$-free if it has no distinct vertices $x,y,z,w$ and distinct hyperedges $h_1,\dots,h_4$ with $\{x,y\}\subseteq h_1$, $\{y,z\}\subseteq h_2$, $\{z,w\}\subseteq h_3$, $\{w,x\}\subseteq h_4$.

In Lean, $\mathrm{ex}_{bip}(n,C_6,C_8)$ is exBip n (cycleGraph 6) {8}, and $\mathcal N$ is Mathlib's copyCount.

Formalization targets

Goal: Theorem 12

$$\mathrm{ex}_{bip}(n,C_6,C_8)=n^3+O\bigl(n^{5/2}\bigr)\qquad(n\to\infty).$$

This is two-sided: $|\mathrm{ex}_{bip}(n,C_6,C_8)-n^3|\le Cn^{5/2}$ for some constant $C$ and all large $n$.

Milestones

1. Lower bound. $K_{3,n-3}$ is bipartite, $C_8$-free, and has exactly $6\binom{n-3}{3}=n^3-O(n^2)$ six-cycles. This is Theorem 10's construction with $k=4$, $l=3$, and Remark 2 notes that it is bipartite.
2. Shape of fat 6-cycles.
   • Claim 3: a fat pair $\{v_1,v_3\}$ on $v_1\cdots v_6$ excludes the fat pairs $\{v_2,v_4\}$ and $\{v_2,v_6\}$.
   • Claim 4: fat 6-cycles through one fat pair have pairwise intersecting fat pairs in the other class.
   • Claim 5: distinct fat pairs of fat 6-cycles in $A$ have $|N\cap N'|\le 1$.
   • Observation 1: a disjointness statement for fat pairs sharing a vertex.
3. Claim 6. For a fat pair $\{v_1,v_3\}\subseteq A$, the sum $g(v_1,v_3)$ of $|N(v_4,v_6)|$ over the fat pairs $\{v_4,v_6\}\subseteq B$ on a common fat 6-cycle with $v_1,v_3$ is at most $4n$.
4. Corollary 7 (from Győri–Lemons). A Berge-$C_4$-free hypergraph on $n$ vertices has $\sum_e|e|=O(n^{3/2})$.
5. Claim 7. The hypergraph on $B$ whose hyperedges are the sets $N(v_1,v_3)$, over the fat pairs of $A$ that lie on a fat 6-cycle, is Berge-$C_4$-free.
6. Claim 8. There are $O(n^{5/2})$ fat 6-cycles.
7. Non-fat cycles.
   • Claim 9: a marked pair inside a nice set gives good triples.
   • Claim 10: $O(|A|^{3/2})$ marked pairs lie in no nice set.
   • Claim 11: $O(|A|^2)$ bad triples contain neither a fat nor a marked pair.
8. One-sided count. At most $6\binom{|A|}{3}+O(|A|^{5/2})$ six-cycles contain no fat pair from $A$.

Significance

Theorem 12 is the only case of the paper where a bipartite generalized Turán number of two even cycles is determined up to a lower-order term. Theorem 10 gives the order $n^l$ in general, and Remark 2 gives bipartite upper and lower bounds whose ratio tends to 1 only as $k\to\infty$. Theorem 12 settles $(l,k)=(3,4)$ exactly. The authors conjecture that the non-bipartite number $\mathrm{ex}(n,C_6,C_8)$ has the same asymptotics, but this is open. The argument also links graph counting to Berge hypergraphs: Claim 7 reduces the fat 6-cycles to a Berge-$C_4$-free hypergraph, whose total edge size is controlled by Corollary 7.

Theorem 12 is proved in the paper. As far as a search of the Prove2Me catalogue shows, neither it nor any of its claims has a machine-checked proof. Formalizing it means:

• formalizing the case analysis of §4.2;
• formalizing Corollary 7, which depends on the Győri–Lemons theorems (Theorems 5 and 6), proved outside the paper;
• formalizing the elementary but tedious count of 6-cycles in $K_{3,n-3}$.

Difficulty

The obvious bound fails. Every 6-cycle in a bipartite graph has three vertices in each class, and each pair of them has some common neighbours. If no pair had more than three common neighbours, each triple in $A$ would lie on at most $27$ six-cycles, giving roughly $27\binom{n}{3}$ cycles, not $n^3$. The leading constant $1$ needs two refinements. First, triples on more than $6$ cycles must be shown to be rare. Second, cycles through pairs with many common neighbours (fat pairs) must be bounded separately, by $O(n^{5/2})$. That second bound is the main obstacle. A fat pair alone can lie on many cycles, so counting fat pairs is not enough. What makes the bound work is the near-disjointness of the common neighbourhoods (Claims 4–6) together with a hypergraph Turán estimate.

Formalization scope

• Vertices and copies. Graphs are SimpleGraph (Fin n), or a general finite type in milestones about a single graph. Copies are unlabelled (copyCount, the number of subgraphs isomorphic to $C_6$): $K_{3,3}$ has $6$ copies of $C_6$, not $72$.

• Bipartiteness. In $\mathrm{ex}_{bip}$ it is Colorable 2. In the milestones it is an explicit bipartition $(A,B)$ that excludes edges inside a class. $C_8$-freeness is (cycleGraph 8).Free G.

• The maximum. $\mathrm{ex}_{bip}$ is a supremum of natural numbers over a nonempty finite set, since the empty graph is admissible. It is therefore a true maximum; a sanity file proves this.

• Cycles inside the proof. Labelled 6-cycles are injective maps from $\mathbb Z/6$ with consecutive images adjacent. Claim 8 counts fat 6-cycles labelled, which changes only the constant.

• Landau terms. Every $O(\cdot)$ is an explicit constant, quantified before $n$ and the graph. The goal uses Mathlib's IsBigO of $\mathrm{ex}_{bip}(n,C_6,C_8)-n^3$ against $n^{5/2}$.

• Corrections to the printed text.

  • Observation 1's conclusion is stated with $N(v_4,v_6')$, as in its proof, rather than the printed $N(v_4',v_6')$.
  • Claim 6's $g$ is the displayed sum, not "the cardinality of the union".
  • Claim 4 drops the hypothesis "different cycles", which only excludes a trivial case. It also drops "these are the other fat pairs", which follows from Claim 3.

• Ruled-out encodings. Some encodings would make the statements trivial or wrong, and none of them is used:

  • a one-sided goal (only the upper bound, or only the lower bound);
  • a junk supremum;
  • labelled copies in place of unlabelled ones;
  • constants allowed to depend on $n$ or on the graph;
  • a bipartition that allows edges inside a class.

• Infrastructure. A complete development needs:

  • counting of cycle copies in complete bipartite graphs;
  • Hall's theorem (in Mathlib), used in Claims 7 and 10;
  • the Kővári–Sós–Turán bound $\mathrm{ex}(m,C_4)=O(m^{3/2})$ for Claim 10;
  • the Győri–Lemons theorems for Corollary 7.

  The Berge-cycle and $C_4$-free bounds can be reused beyond this mission. Contributions are welcome at any level: proofs of individual claims, of Corollary 7, or the final assembly.

Selected references

• D. Gerbner, E. Győri, A. Methuku, M. Vizer, Generalized Turán problems for even cycles, J. Combin. Theory Ser. B 145 (2020); arXiv:1712.07079v3. https://arxiv.org/abs/1712.07079, https://doi.org/10.1016/j.jctb.2020.05.005
• N. Alon, C. Shikhelman, Many $T$ copies in $H$-free graphs, J. Combin. Theory Ser. B 121 (2016). https://doi.org/10.1016/j.jctb.2016.03.004
• E. Győri, N. Lemons, Hypergraphs with no cycle of a given length, Combin. Probab. Comput. 21 (2012). https://doi.org/10.1017/S0963548311000691
• B. Bollobás, E. Győri, Pentagons vs. triangles, Discrete Math. 308 (2008). https://doi.org/10.1016/j.disc.2007.08.041
• D. Gerbner, C. Palmer, Counting copies of a fixed subgraph in $F$-free graphs, European J. Combin. 82 (2019). https://doi.org/10.1016/j.ejc.2019.07.004

Motivation

The Turán number $\mathrm{ex}(n,F)$ is the largest number of edges in an $n$-vertex graph with no copy of $F$. Its generalized version, introduced systematically by Alon and Shikhelman (JCTB 2016), replaces edges by copies of a second graph $H$: $\mathrm{ex}(n,H,\mathcal F)$ is the largest number of copies of $H$ in an $n$-vertex graph containing no member of the family $\mathcal F$. When both $H$ and the forbidden graphs are cycles, these numbers measure how many long cycles a graph can carry while some cycle lengths are excluded and they refine the Bondy–Simonovits even-cycle theorem (JCTB 1974), which bounds the number of edges of a $C_{2k}$-free graph by $O(n^{1+1/k})$.

Gerbner, Győri, Methuku and Vizer (arXiv:1712.07079, J. Combin. Theory Ser. B 2020, DOI 10.1016/j.jctb.2020.05.005) study $\mathrm{ex}(n,C_a,\mathcal C_A)$ for cycles. Their Theorem 10 gives $\mathrm{ex}(n,C_{2l},C_{2k})=\Theta(n^l)$; Theorem 14, the subject of this mission, adds a girth condition: when all cycles of length $3,\dots,2l-1$ are forbidden together with $C_{2k}$, the order of magnitude of the number of $C_{ml}$'s is $n^m$. The case $m=2$ answers the question of how many $C_{2l}$'s a $C_{2k}$-free graph of girth $2l$ can have.

Setting

All graphs are finite and simple. A copy of a graph $H$ in $G$ is a subgraph of $G$ isomorphic to $H$, and $\mathcal N(H,G)$ is the number of copies. $C_a$ is the cycle of length $a\ge3$; $P_l$ is the path on $l$ vertices (of length $l-1$).

For a set $A$ of integers, each at least $3$, let $\mathcal C_A=\{C_a:a\in A\}$; a graph is $\mathcal C_A$-free if it contains none of these cycles as a subgraph. Write $\mathcal C_{2l-1}=\{C_3,C_4,\dots,C_{2l-1}\}$. The generalized Turán number is

$$\mathrm{ex}(n,H,\mathcal C_A)=\max\{\mathcal N(H,G): G\text{ is a }\mathcal C_A\text{-free graph on }n\text{ vertices}\}.$$

For vertices $a\neq b$, $f_l(a,b)$ is the number of paths with $l$ edges between $a$ and $b$. A pair $\{u,v\}$ is fat if $f_l(u,v)\ge 4l^2$, and a copy of $C_{2l}$ is fat if all $l$ of its pairs of opposite vertices are fat.

The $(l,t)$-theta graph joins two vertices by $t$ internally disjoint paths of length $l$. For a graph $F$, the theta-$(n,F,l)$ graph replaces each edge of $F$ by an $(l,t)$-theta graph with $t=\lfloor (n-|V(F)|)/(|E(F)|(l-1))\rfloor$ and adds isolated vertices up to $n$; here $F=C_m$ for $m\ge3$ and $F=K_2$ for $m=2$.

Formalization targets

Goal: Theorem 14

For integers $k>l\ge2$ and $m\ge2$ with $2k\neq ml$,

$$\mathrm{ex}\big(n,C_{ml},\mathcal C_{2l-1}\cup\{C_{2k}\}\big)=\Theta(n^m)\qquad(n\to\infty).$$

Both bounds are part of the goal; the constants depend on $k,l,m$ only.

Milestones

1. Lemmas 25 and 26: forbidding additional odd cycles (Lemma 25) or shorter odd cycles (Lemma 26) does not change the order of magnitude of $\mathrm{ex}(n,C_{2k},\mathcal C_A)$ or $\mathrm{ex}(n,C_{2k+1},\mathcal C_A)$.
2. Lemma 27: a partition $V_1,\dots,V_s$ with no $P_3$ inside $V_i$ ($i<s$), no $P_{p+1}$ joining different parts and $V_s$ independent forces $|E(G)|\le p\,n$.
3. The lower bound: the theta graph has only cycles of lengths $2l$ and $ml$, hence avoids the forbidden family, and has $\Omega(n^m)$ cycles of length $ml$.
4. Claims 12 and 13: the structure of two $2l$-cycles through a common path, and short detours between fat pairs, in graphs of girth at least $2l$.
5. Counting $C_{2l}$'s in girth at least $2l$: at most $\binom{4l^2-1}{2}\binom n2$ non-fat ones; Claim 14 on the greedy multiplicities; at most $\frac{2k(k-l)}{l-2}\binom n2$ fat ones.
6. The case $m\ge3$: display (5), $\tfrac12\sum_{a\ne b}\binom{f_l(a,b)}{2}=O(n^2)$, and Claim 15, $\sum_{b\neq a}f_l(a,b)=O(n)$.

Significance

Theorem 14 locates $\mathrm{ex}(n,C_{ml},\mathcal C_{2l-1}\cup\{C_{2k}\})$ at $n^m$ for every admissible triple, so in graphs of girth $2l$ forbidding one further even cycle $C_{2k}$ (with $2k\neq ml$) caps the number of $ml$-cycles at the count achieved by a blown-up $m$-cycle of long paths. The paper uses it to settle the order of magnitude of $\mathrm{ex}(n,C_6,\mathcal C_A)$ for every family $A$ with $4\in A$, $6\notin A$ and $|A_e|\ge2$ (Theorem 20), and its case $l=2$ recovers Theorem 10.

The result is proved in the paper; nothing here is open mathematically. To the best of a platform search (2026-10-08), no part of it is formalized: Mathlib has copyCount, cycleGraph and pathGraph, but no generalized Turán numbers, no theta graphs and no counting of paths between two vertices. The mission produces a machine-checked proof of the theorem and of the counting lemmas of §5, which are reusable for other generalized Turán problems with cycles.

Difficulty

The lower bound is an explicit construction, and its difficulty is bookkeeping: proving that a subdivided multigraph has no cycles other than those of lengths $2l$ and $ml$, and counting the $ml$-cycles. The upper bound is the substance. A direct count of $C_{2l}$'s through codegrees, which works for $C_4$, fails here because paths of length $l$ between a pair are not controlled by a single neighbourhood. The paper's route separates fat from non-fat cycles and runs a greedy multiplicity procedure; Claim 14 then grows a $C_{2k}$ by an induction on the cycle length in steps of $l-1$, which needs the precise intersection pattern of Claim 12 and the detour paths of Claim 13. For $m\ge3$ the argument goes through layered neighbourhoods and Lemma 27. The $m=2$ argument divides by $l-2$, so for $l=2$ a different route (Theorems 10 and 11 of the paper) is needed.

Formalization scope

Graphs are SimpleGraph (Fin n) for the extremal function and graphs on an arbitrary finite type for the lemmas. Copies are unlabelled (copyCount, subgraphs isomorphic to the pattern); $C_a$ and $P_l$ are Mathlib's cycleGraph a and pathGraph l. exCyc n H A is the supremum, over $\mathcal C_A$-free graphs on Fin n, of the copy count; the set is finite and contains the empty graph's count whenever every length in $A$ is at least $3$, so it is a maximum. The forbidden family of the goal is Set.Icc 3 (2 * l - 1) ∪ {2 * k}, every length from $3$ to $2l-1$ together with $2k$. $\Theta$, $O$ and $\Omega$ are Mathlib's asymptotic relations along atTop, with constants fixed before $n$ and the graph. $f_l(a,b)$ counts injective vertex sequences (paths, not walks). The theta graph thetaCycle n m l is an explicit graph on Fin n.

Added or pinned hypotheses, all disclosed in the items: $l\ge2$ in the goal (the page writes only $k>l$; at $l=1$ the family $\mathcal C_{2l-1}$ is empty and the statement fails); $C\neq C'$ in Claim 12; $l\ge3$ where the page divides by $l-2$; Lemma 27 with the explicit bound $p\,n$ of its proof, which is uniform in $s$; Claim 15 under the full family $\mathcal C_{2l-1}\cup\{C_{2k}\}$, which its proof needs. Claim 14 assumes only girth $\ge 2l$, not $C_{2k}$-freeness, since on the page its conclusion at $r=k$ is the contradiction.

The statements rule out the trivializing readings: the goal is two-sided, so an upper bound alone does not close it; exCyc is a genuine maximum, not a junk supremum; copies are unlabelled; the constants come before $n$ and the graph; the forbidden family contains all short cycles, not only $C_{2l-1}$.

A complete development needs path counting in graphs of large girth (uniqueness of short paths), layered neighbourhoods, the degeneracy argument of Lemma 27, a random bipartition argument for Lemma 25, and cycle structure in theta graphs. Contributions of any milestone, and of general-purpose lemmas on paths and cycles in SimpleGraph, are welcome.

Selected references

• D. Gerbner, E. Győri, A. Methuku, M. Vizer, Generalized Turán problems for even cycles, J. Combin. Theory Ser. B (2020); arXiv:1712.07079v3 (2018). https://arxiv.org/abs/1712.07079, https://doi.org/10.1016/j.jctb.2020.05.005
• N. Alon, C. Shikhelman, Many T copies in H-free graphs, J. Combin. Theory Ser. B 121 (2016). https://doi.org/10.1016/j.jctb.2016.03.004
• J. A. Bondy, M. Simonovits, Cycles of even length in graphs, J. Combin. Theory Ser. B 16 (1974). https://doi.org/10.1016/0095-8956(74)90052-5

Motivation

An extremal graph problem asks how many copies of a chosen small graph can occur when a different graph is forbidden. The usual Turán problem counts edges; counting paths or cycles gives a more detailed view of the structure that can survive a forbidden subgraph. Gerbner, Győri, Methuku and Vizer study these generalized Turán numbers for paths and cycles in their paper on even-cycle problems. Their Theorem 23 asks for the leading number of paths when a specified odd cycle is absent. The answer has the same leading term as a balanced complete bipartite graph, despite the fact that excluding one odd cycle is weaker than requiring a graph to be bipartite. Gerbner et al., Theorem 23

The spectral theorem cited by the authors gives a useful threshold for this setting. For a graph with no cycle of length $2k+1$, it bounds the adjacency spectral radius once the vertex count exceeds $320(2k+1)$. This threshold is explicit and stays visible in the finite-size milestone. Gerbner et al., Theorem 32, citing Nikiforov (2008).

Setting

A simple graph $G$ has finitely many vertices and no loops or parallel edges. For $a\ge3$, $C_a$ is the cycle on $a$ vertices, and $P_l$ is the path on $l$ vertices. Thus $P_l$ has $l-1$ edges, following the paper's convention. A copy of $H$ in $G$ is a subgraph of $G$ isomorphic to $H$; copies are unlabelled, so reversing a path does not create a second copy. Write $\mathcal N(H,G)$ for their number. Gerbner et al., pp. 2–3

For a set $A$ of lengths, a graph is $\mathcal C_A$-free if it has no subgraph isomorphic to $C_a$ for any $a\in A$. The mission mainly uses $A=\{2k+1\}$: exactly one odd cycle length is forbidden, while shorter and longer cycles may still occur. The generalized Turán number is the maximum

$$\operatorname{ex}(n,H,\mathcal C_A) =\max_{\substack{|V(G)|=n\\G\text{ is }\mathcal C_A\text{-free}}}\mathcal N(H,G).$$

The adjacency matrix $A_G$ records whether each pair of vertices is adjacent. Because the graph is undirected, this is a real symmetric matrix. Its spectral radius $\mu(G)$ is the largest absolute value of an eigenvalue of $A_G$. The graph $B_{n,a}$ is the complete bipartite graph with parts of sizes $a$ and $n-a$; the balanced choice uses $a=\lfloor n/2\rfloor$. Gerbner et al., §§7.1–7.2

Formalization targets

Main result: Theorem 23

For each fixed $k\ge1$ and $l\ge2$, as $n\to\infty$,

$$\operatorname{ex}(n,P_l,\mathcal C_{\{2k+1\}}) =(1+o(1))\left(\frac n2\right)^l.$$

The equality gives both sides of the asymptotic estimate. The $o(1)$ term may depend on the fixed parameters $k,l$ and tends to zero as the number of vertices grows. Gerbner et al., Theorem 23, p. 8

Supporting targets

The milestone list records the balanced complete bipartite lower bound, the comparison between paths and walks in equation (7), a spectral bound on the walk sum, Nikiforov's stated spectral estimate, and the resulting finite-size upper bound. In particular, the last two targets retain the paper's constants:

$$n>320(2k+1),\qquad \mu(G)\le\sqrt{n^2/4},\qquad \mathcal N(P_l,G)\le(n/2)^l.$$

The milestone statements identify which assertions concern every graph and which require the forbidden-cycle condition. Gerbner et al., pp. 30, 32

Companion: even cycles (Theorem 24)

For fixed $k\ge1$ and $l\ge2$,

$$\operatorname{ex}(n,C_{2l},\mathcal C_{\{2k+1\}})=(1+o(1))\,\frac{1}{2l}\left(\frac{n^2}{4}\right)^{l},$$

and Remark 3 records the inequality $\mathcal N(P_{2l},G)\ge 2l\,\mathcal N(C_{2l},G)$ for every graph $G$, which links this count to Theorem 23. Gerbner et al., Theorem 24, p. 11; Remark 3, p. 32

Significance

Theorem 23 fixes the leading coefficient for the maximum path count for every fixed path length and forbidden odd-cycle length in its range. A balanced complete bipartite graph reaches that coefficient asymptotically, so the result identifies an extremal construction at first order. The lower-bound milestone formalizes this construction with balanced parts, including the one-vertex rounding needed when $n$ is odd. The matrix and spectral milestones can also be reused when counting walks or paths under different graph restrictions. Gerbner et al., §7.2

The paper proves these results on paper. In this mission, the definitions and theorem statements are checked by Lean, while proofs of the draft theorems remain to be supplied. A completed development would make the path-count theorem and its stated spectral dependency machine checked in the pinned Mathlib environment. It would also expose where a general graph identity suffices and where the odd-cycle prohibition matters.

Difficulty

Counting paths directly is difficult because the available information about a graph with one forbidden odd-cycle length does not control each vertex degree tightly enough to determine a sharp path count. Counting walks is easier algebraically, but walks may revisit vertices, so their number is generally larger than the number of paths. A graph-wide spectral bound is needed to control the walk total sharply, and the cited Nikiforov estimate has to be carried with its forbidden-cycle hypothesis and vertex threshold. A generic bound based only on the maximum degree would not yield the coefficient in Theorem 23. Gerbner et al., §§7.1–7.2

Formalization scope

Graphs on $n$ vertices are represented as SimpleGraph (Fin n). Mathlib's cycleGraph a and pathGraph l represent $C_a$ and the path on $l$ vertices, and copyCount counts unlabelled subgraph copies. The finite set of real adjacency eigenvalues defines $\mu(G)$ through a maximum of absolute values. On an empty vertex type this value is zero. The extremal number is a natural-number supremum over feasible graphs; for the odd-cycle family the feasible set is nonempty and finite, so this supremum is attained.

The goal has $k\ge1$ and $l\ge2$, exactly as Theorem 23 states. The lower-bound item chooses parts of sizes $\lfloor n/2\rfloor$ and $\lceil n/2\rceil$. Equation (7) requires $l\ge2$: for $l=1$ the claimed factor of two is false. The finite spectral and path bounds require $n>320(2k+1)$. These conditions are explicit in the Lean statements. Natural subtraction appears only in expressions whose hypotheses make the intended quantity meaningful, including $l-1$; the bipartite part size is computed with natural division. The asymptotic statements use real sequences tending to zero and eventual comparisons or equality.

The result must include the lower bound as well as the upper bound. It uses unlabelled path copies, an attained extremal maximum, and a forbidden family consisting of the specified odd cycle. An upper bound alone, labelled copies, or a supremum over an empty class would change the theorem. The needed infrastructure consists of graph-copy counts, adjacency-matrix walk counts, finite-dimensional spectral facts, and the cited odd-cycle spectral theorem. The page states Theorem 24 "for any $k,l$"; the Lean statement and Remark 3 require $k\ge1$ and $l\ge2$, the only values for which $C_{2k+1}$ and $C_{2l}$ are cycles. Contributions proving the milestones or developing reusable interfaces for those objects are within scope.

Selected references

• D. Gerbner, E. Győri, A. Methuku and M. Vizer, Generalized Turán problems for even cycles, Journal of Combinatorial Theory, Series B, 2020. arXiv:1712.07079v3; DOI:10.1016/j.jctb.2020.05.005.
• V. Nikiforov, A spectral condition for odd cycles in graphs, Linear Algebra and its Applications 428 (2008), 1492–1498. Cited as [34] in arXiv:1712.07079v3.

Motivation

The classical Turán problem asks for the maximum number of edges of an $n$-vertex graph that avoids a fixed subgraph. For even cycles this is one of the central open problems of extremal graph theory: Bondy and Simonovits proved that a $C_{2k}$-free graph has $O(n^{1+1/k})$ edges, and this order is known to be sharp only for $k=2,3,5$.

A generalized Turán problem replaces "edges" by "copies of a fixed graph $H$". The question of how many copies of one cycle a graph may contain while avoiding another cycle goes back to Erdős's question on pentagons in triangle-free graphs, and was taken up systematically by Alon and Shikhelman (2016). For two even cycles, Solymosi and Wong asked whether forbidding the single cycle $C_{2k}$ (instead of all cycles up to length $2k$) still forces few copies of $C_{2l}$. Gerbner, Győri, Methuku and Vizer answer this question by determining the order of magnitude: the maximum is $\Theta(n^l)$, much larger than in the girth-restricted setting. The same order of magnitude was obtained independently by Gishboliner and Shapira; the proof formalized here is different and gives explicit constants.

Timeline:

• 1959 — Erdős and Gallai: a graph on $n$ vertices with no cycle longer than $k$ has at most $k(n-1)/2$ edges.
• 1974 — Bondy and Simonovits: $\mathrm{ex}(n,C_{2k})=O(n^{1+1/k})$.
• 2016 — Alon and Shikhelman introduce the systematic study of $\mathrm{ex}(n,H,F)$.
• 2017–2018 — Gerbner, Győri, Methuku and Vizer (arXiv:1712.07079), and independently Gishboliner and Shapira, show $\mathrm{ex}(n,C_{2l},C_{2k})=\Theta(n^l)$.

Setting

All graphs are finite and simple. For graphs $H$ and $G$, $\mathcal N(H,G)$ is the number of subgraphs of $G$ isomorphic to $H$ (unlabelled copies). $C_a$ is the cycle on $a\ge3$ vertices. A graph is $C_{2k}$-free if it has no subgraph isomorphic to $C_{2k}$ (induced or not). The generalized Turán number is

$$\mathrm{ex}(n,C_{2l},C_{2k})=\max\{\mathcal N(C_{2l},G): G\text{ a }C_{2k}\text{-free graph on }n\text{ vertices}\}.$$

For a non-negative integer $m$ and $l\ge1$, the falling factorial is $(m)_l=m(m-1)\cdots(m-l+1)$.

For distinct vertices $a,b$ of $G$, the codegree $f(a,b)$ is the number of common neighbours of $a$ and $b$. Sums written $\sum_{a\neq b}$ range over unordered pairs $\{a,b\}$ of distinct vertices.

Two graphs appear in the lower bounds. The first is the complete bipartite graph $K_{k-1,n-k+1}$. The second is the blow-up of $C_{2l}$: keep $l$ alternate vertices $x_0,\dots,x_{l-1}$ of $C_{2l}$, and replace the vertex between $x_i$ and $x_{i+1}$ (indices mod $l$) by a class $S_i$ of new vertices, each joined to $x_i$ and $x_{i+1}$. The $n-l$ new vertices are split as evenly as possible among the $l$ classes.

Formalization targets

Goal: Theorem 10

As $n\to\infty$ with $k$ and $l$ fixed:

$$\mathrm{ex}(n,C_{2l},C_{2k})\le(1+o(1))\frac{2^{l-2}(k-1)^l}{2l}n^l\qquad(l\ge3,\ k\ge2),$$ $$\mathrm{ex}(n,C_{2l},C_{2k})\ge(1+o(1))\frac{(k-1)_l}{2l}n^l\qquad(k>l\ge2),$$ $$\mathrm{ex}(n,C_{2l},C_{2k})\ge(1+o(1))\frac{1}{l^l}n^l\qquad(l>k\ge3).$$

The goal is the conjunction of the three bounds, each with its own parameter range. Note that the upper bound has the power $(k-1)^l$, while the second lower bound has the falling factorial $(k-1)_l$.

Milestones

The lower bounds:

• $K_{k-1,n-k+1}$ is $C_{2k}$-free and has exactly $\frac1{2l}\binom{k-1}{l}\binom{n-k+1}{l}l!\,l!$ copies of $C_{2l}$.
• The blow-up of $C_{2l}$ is $C_{2k}$-free for $3\le k<l$, and its number of $C_{2l}$'s is $\prod_i|S_i|$.

The upper bound:

• The identity $2\,\mathcal N(C_4,G)=\sum_{a\neq b}\binom{f(a,b)}{2}$.
• Inequality (1): $\tfrac12\sum_{a\ne b}\binom{f(a,b)}2\le(1+o(1))\frac{(k-1)(k-2)}4n^2$ for $C_{2k}$-free $G$, which is the upper bound of Theorem 11.
• Theorem 2: the Erdős–Gallai bound, in its correct form.
• Claim 1: $\sum_{b\neq a}f(a,b)\le(2k-2)n$.
• Inequality (2): $\sum_{a\neq b}f(a,b)\le(k-1)n^2$.
• Inequality (3): $\mathcal N(C_{2l},G)\le\frac1{4l}\sum\prod_jf(v_j,v_{j+1})$, together with its AM–GM refinement.
• The final bound $\mathcal N(C_{2l},G)\le\frac1{2l}\sum_{u\neq v}f^2(u,v)(2k-2)^{l-2}n^{l-2}$.

Significance

Theorem 10, combined with Theorem 11 on $\mathrm{ex}(n,C_4,C_{2k})$, gives $\mathrm{ex}(n,C_{2l},C_{2k})=\Theta(n^l)$ for all $k,l\ge2$. The one exception is the lower bound at $k=2$, which comes from the Erdős–Rényi polarity graph. This answers the Solymosi–Wong question in the negative: forbidding one even cycle allows many more copies of a shorter or longer even cycle than forbidding all short cycles does. The codegree method of the upper bound, which bounds $\mathcal N(C_{2l},G)$ by sums of $f^2$ and controls those sums through $C_4$-counts and paths of length two, is reused in the paper's later results on graphs of given girth (Theorem 14).

On the formal side, none of these results is formalized in Lean. Mathlib has copyCount, cycleGraph and edge-extremal numbers, but no generalized Turán numbers, no Erdős–Gallai circumference theorem and no Bondy–Simonovits theorem. The mission produces:

• machine-checked exact counts of cycles in complete bipartite graphs and blow-ups;
• a formal Erdős–Gallai circumference bound;
• the codegree inequalities that turn local degree information into cycle counts.

The paper's printed version of the Erdős–Gallai bound, $(k-1)n/2$, is incorrect. The mission states the bound $k(n-1)/2$ that Erdős and Gallai proved, which is all the argument needs.

Difficulty

The two lower bounds are explicit counts. The difficulty there is combinatorial bookkeeping in Lean. One task is matching unlabelled copies (copyCount) with the $(l!)^2/(2l)$ Hamiltonian cycles of $K_{l,l}$. The other is showing that the blow-up contains no cycle other than 4-cycles and full $2l$-cycles, so that its $2l$-cycles are exactly one choice per class.

The upper bound rests on two classical theorems that are absent from Mathlib:

• the Erdős–Gallai circumference theorem (behind Claim 1);
• Theorem 11's upper bound on the number of $C_4$'s in a $C_{2k}$-free graph (behind (1)), which in turn uses Bondy–Simonovits.

Without (1) one has only $\binom{f}{2}\le f^2$ and no control of $\sum f^2$. Without Claim 1 the chained sums in (3) are not bounded by $(2k-2)n$ per step. The naive estimate, which bounds each $f(v_j,v_{j+1})$ by the maximum codegree, does not work: in a $C_{2k}$-free graph a single codegree can be of order $n$, and that only gives $O(n^{l+1})$.

Formalization scope

Graphs are SimpleGraph (Fin n). Cycles are Mathlib's cycleGraph. $\mathcal N(H,G)$ is G.copyCount H, the number of unlabelled copies (not labelledCopyCount, which is $|\mathrm{Aut}\,H|$ times larger). $\mathrm{ex}(n,H,\mathcal C_A)$ is exCyc n H A, an sSup over $\mathcal C_A$-free graphs on Fin n. The underlying set is finite and contains $0$, from the empty graph, so the value is an attained maximum and not a junk sSup.

Each $(1+o(1))$ is a function $\varepsilon:\mathbb N\to\mathbb R$ with $\varepsilon(n)\to0$, depending only on $k$ and $l$ and chosen before $n$, with the bound holding for all large $n$. Sums over $a\neq b$ are over unordered pairs (Sym2 off the diagonal). With ordered pairs every constant would change by a factor of two, and (2) would be false. Tuples of distinct vertices are embeddings Fin l ↪ V, with indices mod $l$. $(k-1)_l$ is Nat.descFactorial (k - 1) l.

Hypotheses added relative to the page:

• $k\ge2$ in Theorem 2, which fails for forests when $k\le1$;
• $n\ge k-1$ for $K_{k-1,n-k+1}$;
• $n\ge 2l$ for the blow-up count.

Theorem 2 states the corrected bound $2|E|\le k(n-1)$.

The following do not count as the goal: a one-sided goal with only the upper or only the lower bound; a version with labelled copies; a constant or $\varepsilon$ that depends on $n$ or on the graph; and a single unified parameter range.

A complete development needs:

• exact cycle counts in $K_{a,b}$;
• the cycle structure of a subdivided multi-cycle;
• the Erdős–Gallai circumference theorem;
• Theorem 11's upper bound, and with it Bondy–Simonovits;
• the double-counting identities for codegrees.

The Erdős–Gallai theorem, Bondy–Simonovits and the codegree identities are reusable well beyond this mission, and contributions of any of them are welcome.

Selected references

• D. Gerbner, E. Győri, A. Methuku, M. Vizer, Generalized Turán problems for even cycles, J. Combin. Theory Ser. B 145 (2020); preprint arXiv:1712.07079v3. https://arxiv.org/abs/1712.07079 , https://doi.org/10.1016/j.jctb.2020.05.005
• P. Erdős, T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959), 337–356. https://doi.org/10.1007/BF02024498
• J. A. Bondy, M. Simonovits, Cycles of even length in graphs, J. Combin. Theory Ser. B 16 (1974), 97–105. https://doi.org/10.1016/0095-8956(74)90052-5
• N. Alon, C. Shikhelman, Many T copies in H-free graphs, J. Combin. Theory Ser. B 121 (2016), 146–172. https://doi.org/10.1016/j.jctb.2016.03.004
• L. Gishboliner, A. Shapira, A generalized Turán problem and its applications, Int. Math. Res. Not. IMRN (2020). https://arxiv.org/abs/1712.00831

Why count cycles under a girth constraint?

An extremal graph question asks how many copies of one pattern can occur when other patterns are forbidden. When the counted pattern is a cycle, the answer depends strongly on which shorter cycles may occur. Excluding only an even cycle and excluding all cycles up to a given length are different constraints. The latter imposes a girth condition, meaning that nearby vertices cannot be connected by the many short alternative routes that otherwise create small cycles. For odd cycles, this makes a direct application of ordinary edge-count bounds inadequate: many graphs with relatively few edges can still arrange those edges into many copies of a fixed cycle.

Gerbner, Győri, Methuku and Vizer study generalized Turán numbers for cycles and paths. Their Theorem 17 bounds the number of copies of a particular odd cycle when every cycle of lengths $3$ through $2l$, and one further even cycle of length $2k$, is forbidden. The lower and upper exponents differ; the theorem supplies a nontrivial interval for the possible growth rate rather than an exact asymptotic formula. The preprint, Theorem 17 is the source used here; its printed page numbers agree with its PDF pages.

Graphs, copies, and forbidden families

Write $C_a$ for the simple cycle on $a$ vertices. For a set $A$ of integers at least $3$, let $\mathcal C_A=\{C_a:a\in A\}$. A graph $G$ is $\mathcal C_A$-free if no member of the family occurs as a subgraph of $G$. The copies need not be induced: an extra edge between vertices of a copy does not erase that copy. When $A=\{3,\ldots,t\}$, write $\mathcal C_t$ for this family. Thus $\mathcal C_{2l}\cup\{C_{2k}\}$ excludes every cycle of length from $3$ to $2l$ and also excludes the single cycle $C_{2k}$. This notation follows §1 of the paper.

For graphs $H$ and $G$, let $\mathcal N(H,G)$ be the number of unlabelled copies of $H$ in $G$: subgraphs of $G$ isomorphic to $H$, counted once each. The generalized Turán number is

$$\operatorname{ex}(n,H,\mathcal C_A) =\max\{\mathcal N(H,G): |V(G)|=n,\ G\text{ is }\mathcal C_A\text{-free}\}.$$

The graph with no edges is eligible for the forbidden families in this mission, and the finite vertex set makes the maximum well defined. For a vertex $v$ and integer $i\ge0$, $N_i(v)$ is the set of vertices whose graph distance from $v$ is exactly $i$. Vertices in another connected component lie in no $N_i(v)$ with finite $i$.

The lower-bound milestone also uses a hypergraph, a set of hyperedges that are subsets of a common vertex set. It is $r$-uniform when every hyperedge has exactly $r$ vertices. A Berge cycle of length $j$ alternates $j$ distinct vertices and $j$ distinct hyperedges; consecutive vertices lie in their connecting hyperedge. Hypergraph girth at least $s$ means that no Berge cycle has length less than $s$. These definitions are used in Theorem 29 and §6.2.

Formalization targets

Fix integers $k>l\ge2$. The goal is the two-sided statement of Theorem 17, p. 7:

$$\operatorname{ex}(n,C_{2l+1},\mathcal C_{2l}\cup\{C_{2k}\}) =\Omega\bigl(n^{1+1/(2k+1)}\bigr),$$ $$\operatorname{ex}(n,C_{2l+1},\mathcal C_{2l}\cup\{C_{2k}\}) =O\bigl(n^{1+l/(l+1)}\bigr).$$

Both estimates concern $n\to\infty$ with $k$ and $l$ fixed. The paper does not claim that either exponent is optimal for every pair $(k,l)$, and these formulas should not be read as an equality of growth rates.

The milestones record the source statements needed on the two sides. Theorem 29 gives $r$-uniform hypergraphs of prescribed Berge girth with at least $n^{1+1/s}$ hyperedges. The lower-bound paragraph of §6.2 turns such hypergraphs into graphs with many $C_{2l+1}$ copies. Lemma 27 bounds the edges of a graph under a path-restricting partition condition. The local layer identity and Claim 18 control edges in the distance layers $N_l(v)$ and $N_{l+1}(v)$. The final milestone is the low-cycle-vertex conclusion from the paper's deletion passage on p. 28.

What the result provides

The upper exponent $1+l/(l+1)$ is strictly below $2$, so the theorem rules out quadratic growth for this generalized Turán number under the stated forbidden family. The lower exponent $1+1/(2k+1)$ shows that the number of permitted odd cycles nevertheless grows faster than linearly. Together they locate the problem between two explicit power laws. These statements belong to a wider set of cycle-count results in the paper, where changing the forbidden family or the parity of its extra cycle changes the resulting bounds; see Theorems 17 and 18.

The paper proves these bounds. The work here is to state its objects and claims so that Lean can check future proofs: the maximum over admissible graphs, unlabelled cycle counts, Berge-cycle girth, and graph distance layers. The present proposal supplies proof targets; their Lean declarations have placeholders for proofs. The finite graph and hypergraph definitions can also serve later formalizations of generalized Turán and girth questions. The exact growth rate between the two exponents is left open by this theorem.

Where the proof is difficult

Counting cycles from an ordinary upper bound on the number of edges loses the relation between a cycle and its position around a vertex. The no-short-cycle condition constrains individual distance layers, but a layer can still contain edges that close a $C_{2l+1}$. Controlling those edges uniformly across all graphs and vertices is the central issue in the upper bound. A bound with a constant chosen after seeing the graph would say little about the asymptotic maximum; Claim 18 instead requires a constant depending only on $k$ and $l$. The lower side has a different requirement: the construction must preserve both the abundance of odd cycles and every exclusion in $\mathcal C_{2l}\cup\{C_{2k}\}$. The precise assertions are in §6.2, pp. 27–28.

Formalization scope

Graphs on $n$ vertices are represented as simple graphs on $\operatorname{Fin}(n)$, and $C_a$ is Mathlib's cycle graph. A copy is a subgraph isomorphic to $C_a$, counted without labels. The extremal number is the supremum of its finite, nonempty set of attainable natural-number counts; in this setting that supremum is the paper's maximum. Distance layers use extended graph distance, which assigns unreachable pairs infinity. The family of forbidden lengths is exactly $\{3,\ldots,2l\}\cup\{2k\}$; it does not omit any short cycle.

The hypergraph representation is a finite set of distinct finite vertex sets. Berge-cycle existence requires injective lists of vertices and hyperedges, and girth at least $s$ is expressed by absence of lengths $2$ through $s-1$ rather than a numerical infimum with an exceptional value on acyclic hypergraphs. Theorem 29's threshold is chosen after $r,s$ and before $n$. Claim 18's constant is chosen after $k,l$ and before the graph or vertex. The upper and lower asymptotic bounds are both present, with real exponents; neither is replaced by a one-sided or purely existential statement.

Lemma 27 is given with the explicit $m|V(G)|$ edge bound from its proof, uniform in the number of partition classes. The final deletion milestone uses an existential constant $D(k,l)$ because the page mixes several powers of its intermediate constant $c$; this is recorded in the accompanying audit notes. A complete proof development needs Mathlib's simple-graph copies, paths, graph metric, finite-set counting, and asymptotic notation, plus the hypergraph interface defined for this mission. Proofs of the goal and any of these milestones are welcome.

Selected references

• D. Gerbner, E. Győri, A. Methuku, and M. Vizer, Generalized Turán problems for even cycles, Journal of Combinatorial Theory, Series B, 2020. arXiv:1712.07079v3; DOI: 10.1016/j.jctb.2020.05.005.

Motivation

Which cycle lengths a graph must contain is a classical question of extremal graph theory. A graph on $n$ vertices is pancyclic if it has cycles of every length from $3$ to $n$; Bondy's meta-conjecture (Bondy 1971) and a long line of results ask which density or expansion conditions force pancyclicity or, more modestly, force the set of cycle lengths to contain a long interval. For sparse graphs, expansion is the natural hypothesis: random graphs and explicit expanders are sparse, yet very well connected.

Friedman and Krivelevich, Cycle lengths in expanding graphs (arXiv:1912.11011v2; Combinatorica 41, 2021), study two expansion conditions. For the usual vertex expanders they show that cycle lengths are numerous and well spread, but they also note that an expander need not contain any interval of cycle lengths of non-trivial length. Section 4 of the paper therefore introduces a different, two-set expansion condition, the β-graph, and shows that it does force a complete interval of cycle lengths of length linear in $n$. This mission formalizes that result, Theorem 3.

Timeline.

• Friedman and Pippenger (1987) proved that graphs with strong vertex expansion contain every bounded-degree tree of a given size.
• Haxell (2001) generalized that embedding theorem to expansion conditions on sets up to twice a threshold; the form used here is the one stated by Balogh, Csaba, Pei and Samotij (2010).
• Hefetz, Krivelevich and Szabó (2009) proved that for large $n$ and $\beta = O(\log\log n/\log n)$, every β-graph on $n$ vertices has a cycle of every length $\ell$ with $\frac{8\beta n\log n}{\log\log n}\le\ell\le(1-3\beta)n$, and conjectured that the lower end can be improved to $c\log n/\log(1/\beta)$.
• Friedman and Krivelevich (2019 preprint, 2021 journal) proved this for every fixed $\beta<1/20$, with the upper end $(1-O(\beta))n$ (Theorem 3).

Setting

All graphs are finite and simple. For a graph $G=(V,E)$ and a vertex set $U\subseteq V$, the external neighborhood of $U$ is

$$N_G(U)=\{v\in V\setminus U : v\text{ has a neighbor in }U\}.$$

Let $G$ have $n$ vertices and let $\beta>0$. $G$ is a β-graph if every two disjoint vertex sets $A,B\subseteq V$ with $|A|,|B|\ge\beta n$ are joined by an edge. For $n\ge1$, the complete graph is a β-graph for every $\beta>0$; when $\beta n\le 1$, only the complete graph is. No graph on zero vertices is a β-graph.

The set of cycle lengths of $G$ is $L(G)=\{\ell : G\text{ contains a cycle of length }\ell\}$. A cycle of length $\ell$ has $\ell\ge3$ distinct vertices.

The proof works with the tree $T_{k,t,p}$: two complete $k$-ary trees of depth $t$ (every internal vertex has $k$ children, every leaf is at distance $t$ from the root) whose roots are joined by a path of length $p$. A graph contains a copy of a tree $T$ if there is an injective map from the vertices of $T$ to those of $G$ sending edges to edges.

Logarithms are to base $2$.

Formalization targets

Goal: Theorem 3 (p. 3, restated p. 15)

For every $0<\beta<\frac{1}{20}$ there exist positive constants $b_1=O\bigl(\frac{1}{\log(1/\beta)}\bigr)$ and $b_2=O(\beta)$ such that every β-graph $G$ on $n$ vertices satisfies

$$\{\ell\in\mathbb Z : b_1\log n\le\ell\le(1-b_2)n\}\subseteq L(G).$$

The goal fixes the shape of the bound, not its constants: the proof's choice is $b_1=25/\log(1/\beta)$, and $b_2$ is a multiple of $\beta$. As $\beta\to0$ the interval widens towards $[O(\log n/\log(1/\beta)),\,(1-O(\beta))n]$. The upper end $(1-O(\beta))n$ is tight up to the constant: the disjoint union of $K_{n+1-\beta n}$ with $\beta n-1$ isolated vertices is a β-graph.

Milestones

In the order of the proof (pp. 15–18):

1. Lemma 4.1 (p. 15): every β-graph contains an induced subgraph $H$ on at least $(1-\beta)n$ vertices with $|N_H(U)|\ge\frac{1-3\beta}{2\beta}|U|$ for all $|U|\le\beta n$.
2. Large sets in $H$ (p. 16): $|N_H(U)|>(1-4\beta)n$ whenever $\beta n\le|U|\le2\beta n$.
3. Theorem 4.1 (Haxell, p. 16): expansion $d|U|+1$ on sets of size at most $m$ and $d|U|+M$ on sets of size in $(m,2m]$ forces every tree with $M$ vertices and maximum degree at most $d$.
4. Cycle from a tree (p. 16): a copy of $T_{k,t,\ell-2t-1}$ with $k\ge2$ and $k^t\ge\beta n$ in a β-graph yields a cycle of length $\ell$.
5. Condition 1 of Theorem 4.1 for $d=\lfloor1/(4\beta)\rfloor+1$ (p. 17) and for $d=3$ (p. 18).
6. The arithmetic of p. 17: $2\lceil\log(\beta n)\rceil+1<(\frac12-10\beta)n$ and $\frac{25}{\log(1/\beta)}\log n\ge2\lceil\log_k(\beta n)\rceil+1$ for large $n$.

Significance

The result. Theorem 3 proves the conjecture of Hefetz, Krivelevich and Szabó in a stronger form: β may be any constant below $1/20$ instead of tending to zero with $n$, and the lower end $O(\log n/\log(1/\beta))$ is of optimal order. Since spectral expanders satisfy the β-graph condition (by the expander mixing lemma an $(n,d,\lambda)$-graph with $d/|\lambda|\ge1/\beta^2$ is a β-graph), the theorem gives long intervals of cycle lengths in pseudo-random graphs. The method, embedding two large trees joined by a path and closing the cycle across their leaf sets, is a template for producing cycles of prescribed length in expanding graphs.

Formalizing it. The result is proved on paper. As far as the platform's records show, none of it is formalized: Mathlib has trees, walks, cycles and graph copies, but no tree-embedding theorem for expanders and no result on cycle lengths of this kind. The main piece of new infrastructure is Haxell's theorem (milestone 3), which the paper cites without proof. Its proof (in Haxell's paper and in Balogh–Csaba–Pei–Samotij) is a few pages of inductive embedding with a Hall-type invariant. A formal proof of Theorem 4.1 would be reusable for any embedding argument for bounded-degree trees, for example in Ramsey and size-Ramsey problems for trees and paths. The printed proof also has a rounding gap (below), so the formal proof will have to settle a slightly different argument from the printed one.

Difficulty

The β-graph condition only speaks about pairs of large sets, while cycles are built edge by edge, so short and long cycles both need a mechanism. The obvious approach, finding a long path and then shortcutting it, does not control which lengths occur. The proof instead needs a robust embedding theorem for trees with about $2\beta n$ leaves inside a subgraph with good expansion of small sets, and that is Theorem 4.1, a deep result.

A second difficulty is quantitative. In the printed verification of claims (1) and (2) on p. 17, a complete $k$-ary tree of depth $t=\lceil\log_k(\beta n)\rceil$ is counted as having about $k\beta n/(k-1)$ vertices, as if $k^t=\beta n$ exactly. In fact $k^t$ can be almost $k\beta n$, and for claim (2) the honest count only covers $\ell\le(1-18\beta)n$ rather than $(1-14\beta)n$. For $k=\lfloor1/(4\beta)\rfloor$ the gap is larger. Theorem 3 is unaffected, because its constants are only $O(\cdot)$ and pruning the trees to $\lceil\beta n\rceil$ leaves repairs the count. But a solver following the printed proof will need to repair that step. The two claims are therefore not posed as milestones.

Formalization scope

Graphs on $n$ vertices are SimpleGraph (Fin n). Vertex sets are Set with Set.ncard, and every inequality involving β, a logarithm or $n$ is stated in ℝ after casting. Logarithms are Real.logb 2. Cycles are Mathlib's Walk.IsCycle, so every cycle length is at least $3$. "Contains a copy" is SimpleGraph.IsContained (injective and edge-preserving, not induced). The subgraph $G'=H$ of Lemma 4.1 is the induced subgraph on a set $S$, with $N_H(U)=N_G(U)\cap S$. The tree $T_{k,t,p}$ is defined on words of length at most $t$ over $\{0,\dots,k-1\}$ (two tagged copies) plus $p-1$ path vertices.

Conventions of the goal:

• $O(\cdot)$: one absolute constant $K>0$ is quantified before β, with $b_1\le K/\log_2(1/\beta)$ and $b_2\le K\beta$. A constant chosen after β would make the $O(\cdot)$ claims empty, so that encoding is ruled out. Since $\beta<1/20$, $\log_2(1/\beta)>4$ and the division is by a positive number.
• Threshold: the statement holds for $n\ge n_0$ with $n_0$ depending on β only. This is a disclosed, necessary addition: without it the interval contains $\ell=2$ at $n=3$ for small β, and no graph has a cycle of length $2$.
• Every integer in the interval is a cycle length, not some integer.
• A cycle is a genuine cycle, not a closed walk.

Infrastructure needed: Haxell's theorem (reusable well beyond this mission), counting leaves and vertices of complete $k$-ary trees, and turning an embedded $T_{k,t,p}$ plus one edge into a Walk.IsCycle. Contributions to any milestone are welcome, in particular a proof of Theorem 4.1 and a repaired version of claims (1) and (2) with pruned trees.

Selected references

• L. Friedman and M. Krivelevich, Cycle lengths in expanding graphs, Combinatorica 41 (2021). arXiv:1912.11011v2. https://arxiv.org/abs/1912.11011v2, https://doi.org/10.1007/s00493-020-4434-0
• P. E. Haxell, Tree embeddings, Journal of Graph Theory 36 (2001), 121–130. https://doi.org/10.1002/1097-0118(200103)36:3<121::AID-JGT1000>3.0.CO;2-U
• J. Friedman and N. Pippenger, Expanding graphs contain all small trees, Combinatorica 7 (1987), 71–76. https://doi.org/10.1007/BF02579202
• J. Balogh, B. Csaba, M. Pei and W. Samotij, Large bounded degree trees in expanding graphs, Electronic Journal of Combinatorics 17 (2010), R6. https://doi.org/10.37236/279
• J. A. Bondy, Pancyclic graphs I, Journal of Combinatorial Theory, Ser. B 11 (1971), 80–84. https://doi.org/10.1016/0095-8956(71)90016-5
• D. Hefetz, M. Krivelevich and T. Szabó, Hamilton cycles in highly connected and expanding graphs, Combinatorica 29 (2009), 547–568. https://doi.org/10.1007/s00493-009-2362-1