{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"7c2acda769166d413248db520249aaf726cb42fb18b51c57011c70f88c276d55","problem":{"id":5,"title":"Twin prime conjecture: arbitrarily large prime pairs separated by two","description":"Prove that for every natural bound N there is a prime p > N such that p + 2 is also prime. Bounded-gap results do not establish the exact gap two required here. The inline primality predicate excludes 0 and 1. Quantifying over every bound expresses infinitude, rather than verifying a finite collection of examples.\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":"(fun prime : Nat → Prop =>\n  ∀ N : Nat, ∃ p : Nat, N < p ∧ prime p ∧ prime (p + 2))\n(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p)","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := ((fun prime : Nat → Prop =>\n  ∀ N : Nat, ∃ p : Nat, N < p ∧ prime p ∧ prime (p + 2))\n(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p))\n\n#check OA_statement\n","proof":null}