Prove2Me

Caccetta–Häggkvist for r=6r = 6

Open
TenChallenges.challenge_03_r6

by utkuokur · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

caccetta-haggkvistdigraphsten-challenges

The rung r=6r=6 of the Caccetta–Häggkvist conjecture. Every loopless digraph on n≥1n\ge 1 vertices in which every vertex has out-degree at least 66 contains a directed cycle of length at most ⌈n/6⌉\lceil n/6\rceil:

δ+(D)≥6  ⟹  girth(D)≤⌈n/6⌉.\delta^+(D)\ge 6 \implies \text{girth}(D)\le\lceil n/6\rceil .

This rung is open. Shen's theorem gives it for n≥2⋅62−3⋅6+1=55n\ge 2\cdot 6^2-3\cdot 6+1=55; the remaining values of nn are not covered by any published argument.

Preamble
import Definitions.Def_TenChallenges_Challenge_03
Formal statement
namespace TenChallenges
theorem challenge_03_r6 : statement_03 6 := by sorry
end TenChallenges
Source
Open; the status is surveyed in B. D. Sullivan, A summary of results and problems related to the Caccetta–Häggkvist conjecture, 2006, https://arxiv.org/abs/math/0605646. Known for n ≥ 2·36 − 18 + 1 = 55 by J. Shen, On the girth of digraphs, Discrete Math. 211 (2000), https://doi.org/10.1016/s0012-365x(99)00323-4
Human review

  • Endorsed by Shuze Chen · Nov 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by utkuokur · Nov 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph