{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"06d6592d1d3e0948794368e0e45f1db6fd88c59b7e5d50071d5afa691d16123d","problem":{"id":4,"title":"Goldbach conjecture: every even integer above two is a sum of two primes","description":"Prove that every even natural number n ≥ 4 can be written n = p + q with both p and q prime. This is the binary (strong) conjecture; results about sums of three primes do not settle this request. The inline prime predicate means p ≥ 2 and every natural divisor of p is 1 or p. The target covers all even n, with no finite search cutoff.\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, 4 ≤ n → n % 2 = 0 → ∃ p q : Nat, prime p ∧ prime 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(fun p => 2 ≤ p ∧ ∀ d : Nat, d ∣ p → d = 1 ∨ d = p))\n\n#check OA_statement\n","proof":null}