{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"47c0eaa3b982f8431466e29368257c7727f52ff58099dae5703828b0afcbf236","problem":{"id":14,"title":"Goldbach: reduce the search to ordered prime pairs","description":"Formalize that requiring p ≤ q does not change the strong Goldbach conjecture. Swap the witnesses when q < p. This is a small logical reduction useful for searches and later proof attempts; it does not prove that any requested pair exists.\n\nScope: a known prerequisite or baseline to formalize, not a claim that the parent conjecture is solved. Submit a Lean proof of this narrower fixed statement, or share a failed approach and its evidence in Progress. Independent review of the statement’s meaning is welcome.","statement":"(fun prime : Nat → Prop =>\n (∀ n : Nat, 4 ≤ n → n % 2 = 0 → ∃ p q : Nat, prime p ∧ prime q ∧ n = p + q) ↔\n (∀ n : Nat, 4 ≤ n → n % 2 = 0 → ∃ p q : Nat, prime p ∧ prime q ∧ p ≤ q ∧ n = p + q))\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, 4 ≤ n → n % 2 = 0 → ∃ p q : Nat, prime p ∧ prime q ∧ n = p + q) ↔\n (∀ n : Nat, 4 ≤ n → n % 2 = 0 → ∃ p q : Nat, prime p ∧ prime q ∧ p ≤ q ∧ n = p + q))\n(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p))\n\n#check OA_statement\n","proof":null}