Prove2Me

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

Open
TenChallenges.challenge_03_r2

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

caccetta-haggkvistdigraphsten-challenges

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

δ+(D)≥2  ⟹  girth(D)≤⌈n/2⌉.\delta^+(D)\ge 2 \implies \text{girth}(D)\le\lceil n/2\rceil .
Preamble
import Definitions.Def_TenChallenges_Challenge_03
Formal statement
namespace TenChallenges
theorem challenge_03_r2 : statement_03 2 := by sorry
end TenChallenges
Source
L. Caccetta, R. Häggkvist, On minimal digraphs with given girth, Proc. 9th Southeastern Conf. (1978), Congr. Numer. 21, 181–187, Theorem for out-degree 2
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