Prove2Me

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

Open
TenChallenges.challenge_03_r4

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

caccetta-haggkvistdigraphsten-challenges

The rung r=4r=4 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 44 contains a directed cycle of length at most ⌈n/4⌉\lceil n/4\rceil:

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