Motivation

In a finite directed graph in which every vertex has an out-neighbour, following arcs must eventually return to a visited vertex, so a directed cycle exists; but it may be long. The Caccetta–Häggkvist conjecture quantifies how large minimum out-degree forces short directed cycles: out-degree at least $r$ on $n$ vertices should force a directed cycle of length at most $\lceil n/r\rceil$. The circulant digraph on $\mathbb Z/n$ with arcs $v\to v+1,\dots,v+r$ shows that nothing better is possible. The conjecture is a central open problem on digraphs, with connections to the Erdős–Szekeres-type and Ramsey-type questions on tournaments and to the "directed triangle" problem for dense digraphs (Sullivan 2006).

Timeline.

• 1978 — Caccetta and Häggkvist pose the conjecture and prove it for $r=2$ (Caccetta–Häggkvist 1978).
• 1987 — Hamidoune proves the case $r=3$ (Hamidoune 1987).
• 1987 — Hoàng and Reed prove the cases $r=4$ and $r=5$ (Hoàng–Reed 1987).
• 1998 — Shen shows that minimum out-degree at least $(3-\sqrt7)\,n\approx 0.3542\,n$ forces a directed triangle, the first step on the dense case $r=n/3$ (Shen 1998).
• 2000 — Shen proves the conjecture for every $r$ whenever $n\ge 2r^2-3r+1$ (Shen 2000).
• 2017 — Hladký, Král' and Norin lower the triangle threshold to $0.3465\,n$ (Hladký–Král'–Norin 2017).

The cases $r\ge 6$ are open for general $n$.

Setting

A digraph $D$ consists of a finite vertex set $V$ and a set of arcs, ordered pairs $(v,w)$ of distinct vertices; at most one arc from $v$ to $w$, no loops, and arcs in both directions between two vertices are allowed. The out-degree $d^+(v)$ is the number of $w$ with an arc $(v,w)$. A directed cycle of length $\ell\ge 2$ is a sequence $v_0,\dots,v_{\ell-1}$ of distinct vertices with an arc $(v_i,v_{i+1})$ for every $i$, indices modulo $\ell$. For $r\ge 1$ let $\mathrm{CH}(r)$ be the statement

$$\text{every digraph on } n\ge 1 \text{ vertices with } d^+(v)\ge r \text{ for all } v \text{ has a directed cycle of length at most } \lceil n/r\rceil .$$

The condition $\ell\le\lceil n/r\rceil$ is the same as $\ell r<n+r$.

Formalization targets

Goal

$$\forall r\ge 1:\quad \mathrm{CH}(r).$$

Rungs

$$\mathrm{CH}(1),\ \mathrm{CH}(2),\ \mathrm{CH}(3),\ \mathrm{CH}(4),\ \mathrm{CH}(5),$$

and the first open rung $\mathrm{CH}(6)$.

Significance

The conjecture would determine exactly the smallest girth a digraph of given order and minimum out-degree can have, a directed analogue of the Moore-type bounds for undirected graphs; its dense case, that out-degree $n/3$ forces a directed triangle, is itself a well-known open problem and implies results on the number of edges in digraphs without short cycles. Partial results have produced the main tools of extremal digraph theory: Shen's counting arguments, the flag-algebra computations of Hladký, Král' and Norin, and the structural approach of Chudnovsky, Seymour and Sullivan to the triangle case.

Formalizing the known rungs gives Mathlib a working theory of directed cycles and out-degrees, which it does not have. The rung $\mathrm{CH}(1)$ is an exercise; $\mathrm{CH}(2)$ is a two-page argument; $\mathrm{CH}(3)$, $\mathrm{CH}(4)$ and $\mathrm{CH}(5)$ are short papers. None of them has a machine-checked proof. $\mathrm{CH}(6)$ and beyond are open.

Difficulty

The natural induction, removing a vertex of small out-degree or contracting a short cycle, fails because contraction can create parallel arcs or loops and because the minimum out-degree is not preserved; the known proofs for $r\le 5$ are delicate counting arguments on the neighbourhoods of a shortest cycle, and each new value of $r$ has required a new idea. Shen's theorem settles the conjecture only when $n$ is quadratic in $r$, and the dense regime $r\approx n/3$ is open even for triangles.

Formalization scope

Digraphs are Mathlib's Digraph V with [Fintype V] [Nonempty V]; the adjacency relation is arbitrary, so looplessness is an explicit hypothesis ∀ v, ¬ G.Adj v v, while arcs in both directions between two vertices are permitted. The out-degree of $v$ is {w | G.Adj v w}.ncard. A directed cycle of length $\ell$ is an injective map $f\colon\mathrm{Fin}\,\ell\to V$ with an arc from $f(i)$ to $f(i+1)$ for every $i$, the successor taken cyclically (finRotate). CaccettaHaggkvistFor r states: if $0<r$, then every such digraph in which every vertex has out-degree at least $r$ has a directed cycle of some length $\ell$ with $2\le\ell$ and $\ell r<n+r$, where $n$ is the number of vertices. The rung statement_03 r is CaccettaHaggkvistFor r, and the goal quantifies over all $r$; the case $r=0$ is vacuous by the guard $0<r$. Vertex types are in Type (the lowest universe).

No trivialising reading: the length bound $\ell r<n+r$ is exactly $\ell\le\lceil n/r\rceil$, cycles of length $2$ are genuine directed cycles, and the out-degree condition is on every vertex. The Lean definitions are copied verbatim from the Ten Challenges repository. Because the definitions are identical, a proof of the goal or of any rung produced here can also be submitted on the Ten Challenges website, https://tenchallenges.github.io/ten-challenges/, which checks submissions automatically against the same statements and records accepted ones on its public leaderboard; contributors are welcome to do both. Contributions welcome: basic lemmas on HasCycleOfLength (closed walks contain cycles, reversal, blow-ups), the rung $\mathrm{CH}(1)$, and decompositions of $\mathrm{CH}(2)$.

Selected references

• Ten Challenges website: problem statements, automatic checker and leaderboard. https://tenchallenges.github.io/ten-challenges/
• V. Bajpai, N. Bowler, J. Carmesin, U. Okur, 10 Scalable Challenges in Combinatorics: A Public Benchmark Formalised in Lean, AI4Math workshop at CICM 2026. https://cicm-conference.org/2026/ai4math/04-okur.pdf — Lean sources: https://github.com/TenChallenges/ten-challenges (challenge 3).
• L. Caccetta, R. Häggkvist, On minimal digraphs with given girth, Proc. 9th Southeastern Conf. on Combinatorics, Graph Theory and Computing (1978), Congr. Numer. 21, 181–187.
• Y. O. Hamidoune, A note on minimal directed graphs with given girth, J. Combin. Theory Ser. B 43 (1987), 343–348. https://doi.org/10.1016/0095-8956(87)90009-8
• C. T. Hoàng, B. Reed, A note on short cycles in digraphs, Discrete Math. 66 (1987), 103–107. https://doi.org/10.1016/0012-365X(87)90122-1
• J. Shen, Directed triangles in digraphs, J. Combin. Theory Ser. B 74 (1998), 405–407. https://doi.org/10.1006/jctb.1998.1839
• J. Shen, On the girth of digraphs, Discrete Math. 211 (2000), 167–181. https://doi.org/10.1016/s0012-365x(99)00323-4
• B. D. Sullivan, A summary of results and problems related to the Caccetta–Häggkvist conjecture, 2006. https://arxiv.org/abs/math/0605646
• J. Hladký, D. Král', S. Norin, Counting flags in triangle-free digraphs, Combinatorica 37 (2017), 49–76. https://doi.org/10.1007/s00493-015-2662-5
• J. Bang-Jensen, G. Gutin, Digraphs: Theory, Algorithms and Applications, 2nd ed., Springer, 2009. https://doi.org/10.1007/978-1-84800-998-1