{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"6d071e335d1e612d0857066571437d66b5cb50d371c82d71c4a94adc4ba29dc5","problem":{"id":11,"title":"Caccetta–Häggkvist conjecture: force a short directed cycle","description":"Prove that a finite loopless digraph on n ≥ 1 vertices with minimum outdegree at least d has a directed cycle of length at most ceil(n/d), when d ≥ 1. The Lean formulation avoids division: for any positive r with n ≤ r*d it asks for a cycle of length at most r. Outdegree is witnessed by d distinct outgoing neighbours for each vertex. Cycle vertices are distinct, and the final edge returns to the first vertex. The graph need not be symmetric; reverse edges are allowed.\n\nResearch status checked 8 October 2026: no accepted general proof identified in the cited literature. This is a proposed formal statement; independent correspondence review is requested. A successful statement check establishes well-formedness, not the conjecture.","statement":"∀ n d r : Nat, 1 ≤ n → 1 ≤ d → 1 ≤ r → n ≤ r * d →\n  ∀ E : Fin n → Fin n → Bool, (∀ v, E v v = false) →\n  (∀ v, ∃ f : Fin d → Fin n, (∀ i j, f i = f j → i = j) ∧ (∀ i, E v (f i) = true)) →\n  ∃ k : Nat, k + 1 ≤ r ∧ ∃ f : Fin (k + 1) → Fin n,\n    (∀ i j, f i = f j → i = j) ∧\n    (∀ i, E (f i) (f ⟨(i.val + 1) % (k + 1), Nat.mod_lt _ (Nat.zero_lt_succ k)⟩) = true)","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := (∀ n d r : Nat, 1 ≤ n → 1 ≤ d → 1 ≤ r → n ≤ r * d →\n  ∀ E : Fin n → Fin n → Bool, (∀ v, E v v = false) →\n  (∀ v, ∃ f : Fin d → Fin n, (∀ i j, f i = f j → i = j) ∧ (∀ i, E v (f i) = true)) →\n  ∃ k : Nat, k + 1 ≤ r ∧ ∃ f : Fin (k + 1) → Fin n,\n    (∀ i j, f i = f j → i = j) ∧\n    (∀ i, E (f i) (f ⟨(i.val + 1) % (k + 1), Nat.mod_lt _ (Nat.zero_lt_succ k)⟩) = true))\n\n#check OA_statement\n","proof":null}