{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"afd8aab62b4d28dfc6617e18491484bc4d1c3c1c448b77bf2d4f747796733872","problem":{"id":7,"title":"Legendre conjecture: a prime between consecutive positive squares","description":"Prove that for every positive natural number n there is a prime strictly between n² and (n+1)². The lower bound n ≥ 1 matters: the interval between 0 and 1 contains no prime. Both inequalities are strict. The prime predicate is the elementary divisor definition, so this request requires only pinned Lean core.\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, 1 ≤ n → ∃ p : Nat, n ^ 2 < p ∧ p < (n + 1) ^ 2 ∧ prime p)\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, 1 ≤ n → ∃ p : Nat, n ^ 2 < p ∧ p < (n + 1) ^ 2 ∧ prime p)\n(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p))\n\n#check OA_statement\n","proof":null}