Prove2Me

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

Open
TenChallenges.challenge_03_r3

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

caccetta-haggkvistdigraphsten-challenges

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

δ+(D)≥3  ⟹  girth(D)≤⌈n/3⌉.\delta^+(D)\ge 3 \implies \text{girth}(D)\le\lceil n/3\rceil .
Preamble
import Definitions.Def_TenChallenges_Challenge_03
Formal statement
namespace TenChallenges
theorem challenge_03_r3 : statement_03 3 := by sorry
end TenChallenges
Source
Y. O. Hamidoune, A note on minimal directed graphs with given girth, JCTB 43 (1987), 343–348, https://doi.org/10.1016/0095-8956(87)90009-8
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