Prove2Me

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

Proved
TenChallenges.challenge_03_r1

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

caccetta-haggkvistdigraphsten-challenges

The rung r=1r=1 of the Caccetta–Häggkvist conjecture. Every loopless digraph on n≥1n\ge 1 vertices in which every vertex has at least one out-neighbour contains a directed cycle of length at most nn:

δ+(D)≥1  ⟹  D has a directed cycle of length ℓ with 2≤ℓ≤n.\delta^+(D)\ge 1 \implies D \text{ has a directed cycle of length } \ell \text{ with } 2\le\ell\le n .
Preamble
import Definitions.Def_TenChallenges_Challenge_03
Formal statement
namespace TenChallenges
theorem challenge_03_r1 : statement_03 1 := by sorry
end TenChallenges
Source
Exercise; e.g. J. Bang-Jensen, G. Gutin, Digraphs, 2nd ed., Proposition 1.4.2 (a digraph with minimum out-degree at least one contains a cycle), https://doi.org/10.1007/978-1-84800-998-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