{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"49bfa44ace453cde66e68349496ff522e77d31a86b473a074a5f43c1eec78cb7","problem":{"id":10,"title":"Erdős–Hajnal conjecture for every forbidden induced graph","description":"For each fixed finite simple graph H, prove a polynomial lower bound on the largest clique or independent set in every H-free graph G. H-free means no induced copy, not merely no subgraph. The integer form asks for constants C ≥ 1 and k ≥ 1 depending only on H, with n ≤ C*s^k for a homogeneous set of size s in every n-vertex G. Graphs are Boolean adjacency functions on Fin n; symmetry, no loops, embeddings and homogeneous sets are all explicit. Results for particular H, including the recently settled five-vertex cases, leave the general quantification over H unresolved.\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":"∀ h : Nat, ∀ H : Fin h → Fin h → Bool,\n  (∀ i, H i i = false) → (∀ i j, H i j = H j i) →\n  ∃ C k : Nat, 1 ≤ C ∧ 1 ≤ k ∧\n    ∀ n : Nat, ∀ G : Fin n → Fin n → Bool,\n      (∀ i, G i i = false) → (∀ i j, G i j = G j i) →\n      (∀ f : Fin h → Fin n, (∀ i j, f i = f j → i = j) → ¬ (∀ i j, H i j = G (f i) (f j))) →\n      ∃ s : Nat, ∃ f : Fin s → Fin n,\n        (∀ i j, f i = f j → i = j) ∧ n ≤ C * s ^ k ∧\n        ((∀ i j, i ≠ j → G (f i) (f j) = true) ∨\n         (∀ i j, i ≠ j → G (f i) (f j) = false))","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := (∀ h : Nat, ∀ H : Fin h → Fin h → Bool,\n  (∀ i, H i i = false) → (∀ i j, H i j = H j i) →\n  ∃ C k : Nat, 1 ≤ C ∧ 1 ≤ k ∧\n    ∀ n : Nat, ∀ G : Fin n → Fin n → Bool,\n      (∀ i, G i i = false) → (∀ i j, G i j = G j i) →\n      (∀ f : Fin h → Fin n, (∀ i j, f i = f j → i = j) → ¬ (∀ i j, H i j = G (f i) (f j))) →\n      ∃ s : Nat, ∃ f : Fin s → Fin n,\n        (∀ i j, f i = f j → i = j) ∧ n ≤ C * s ^ k ∧\n        ((∀ i j, i ≠ j → G (f i) (f j) = true) ∨\n         (∀ i j, i ≠ j → G (f i) (f j) = false)))\n\n#check OA_statement\n","proof":null}