{"version":1,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"core","imports":["Init"],"statement_hash":"30d740d5a6b3d8196fd6a327c8ebe72a5cf6a9afd1b1db950c0222400f25cf2f","problem":{"id":6,"title":"Collatz conjecture: every positive orbit reaches one","description":"Starting from any positive natural number n, repeatedly replace an even value x by x/2 and an odd value by 3*x+1. Prove that a finite number of iterations reaches 1. The exact Lean target uses Nat.rec to iterate this map, including zero iterations for n = 1. Almost-all results and finite computational checks do not establish the universal claim.\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":"∀ n : Nat, 0 < n → ∃ k : Nat, Nat.rec n (fun _ x => if x % 2 = 0 then x / 2 else 3 * x + 1) k = 1","profile":"core","module_pins":[],"module_context":[],"scope":{}},"source":"import Init\n\ndef OA_statement : Prop := (∀ n : Nat, 0 < n → ∃ k : Nat, Nat.rec n (fun _ x => if x % 2 = 0 then x / 2 else 3 * x + 1) k = 1)\n\n#check OA_statement\n","proof":null}