Prove2Me

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

Open
TenChallenges.challenge_03_r5

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

caccetta-haggkvistdigraphsten-challenges

The rung r=5r=5 of the Caccetta–Häggkvist conjecture (Hoàng and Reed, 1987). Every loopless digraph on n≥1n\ge 1 vertices in which every vertex has out-degree at least 55 contains a directed cycle of length at most ⌈n/5⌉\lceil n/5\rceil:

δ+(D)≥5  ⟹  girth(D)≤⌈n/5⌉.\delta^+(D)\ge 5 \implies \text{girth}(D)\le\lceil n/5\rceil .
Preamble
import Definitions.Def_TenChallenges_Challenge_03
Formal statement
namespace TenChallenges
theorem challenge_03_r5 : statement_03 5 := by sorry
end TenChallenges
Source
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
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