{"request":{"endpoint":"https://exercism.org/api/v2/tracks/lean/exercises/collatz-conjecture/community_solutions","query":{},"options":{"initial_data":{"results":[{"uuid":"b4d19ce2545f4f10b0d7994ab8819a31","snippet":"def Positive := { x : Nat // 0 < x } partial def steps : Positive → (acc : Nat := 0) → Nat | ⟨1, _⟩, acc => acc | ⟨n, h₀⟩, acc => let n' := if 2 ∣ n then n / 2 else 3 * n + 1 have h: 0 < n' := by if h₂: 2 ∣ n then simp [n', h₂]; omega else simp [n', h₂] steps ⟨n', h⟩ (acc + 1) ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":2,"num_iterations":2,"num_loc":11,"iteration_status":"analyzing","published_iteration_head_tests_status":"passed","published_at":"2026-01-26T17:02:15.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"oxe-b"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/oxe-b","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}},{"uuid":"a0eb19e8cfd0440fab97d55ea5bab791","snippet":"def Positive := { x : Nat // 0 < x } def steps (n : Positive) : Nat := Id.run do let mut num:= n.val let mut count:=0 while Ne num 1 do if num%2 == 0 then num:=num/2 else num:=3*num+1 ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":2,"num_loc":12,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-03-06T18:57:40.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"efwhofmann"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/efwhofmann","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}},{"uuid":"94c4925576db4f3883b8905eaf9d228e","snippet":"def Positive := { x : Nat // 0 < x } def steps (n : Positive) : Nat := let rec loop (n : Nat) (depth : Nat) : Nat := if n = 1 ∨ depth = 0 then 0 else if n % 2 = 0 then 1 + loop (n / 2) (depth - 1) else ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":13,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-04-09T11:25:28.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"takah29"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/takah29","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}},{"uuid":"1c28c9af73fa43019a1119839817fe0e","snippet":"def Positive := { x : Nat // 0 < x } instance : Coe Positive Nat := ⟨(·.val)⟩ private def collatzStep (n : Positive) : Positive := ⟨if n.val % 2 = 0 then n / 2 else n * 3 + 1, by grind⟩ partial def steps (n : Positive) : Nat := go n 0 where go n c := if n.val = 1 then c else go (collatzStep n) (c + 1) ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":10,"iteration_status":"analyzing","published_iteration_head_tests_status":"passed","published_at":"2026-06-27T05:41:36.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"setsunica"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/setsunica","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}},{"uuid":"9fd7e9264ee44a3ca89a260783328700","snippet":"namespace CollatzConjecture def Positive := { x : Nat // 0 < x } partial def steps (n : Positive) : Nat := let rec helper (number : Nat) (count : Nat) : Nat := if number == 1 then count else if number % 2 == 0 then helper (number / 2) (count + 1) else helper (3 * number + 1) (count + 1) helper n.val 0 ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":2,"num_loc":9,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-01-24T06:52:12.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"keiraville"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/keiraville","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}},{"uuid":"9347cab1f4e943daa5d1eba0c1b8d926","snippet":"def Positive := { x : Nat // 0 < x } partial def steps (n : Positive) : Nat := let rec aux (num cnt : Nat) : Nat := if num == 1 then cnt else aux (if num % 2 == 0 then num / 2 else 3 * num + 1) (cnt + 1) aux n.val 0 ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":8,"iteration_status":"analyzing","published_iteration_head_tests_status":"passed","published_at":"2026-05-18T17:48:25.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"menketechnologies"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/menketechnologies","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}},{"uuid":"af8123d070d4427485674e2080b5ead0","snippet":"def Positive := { x : Nat // 0 < x } partial def steps (n : Positive) : Nat := let rec aux (i : Nat) (n : Nat) : Nat := if n == 1 then i else if (n % 2) == 0 then aux (i + 1) (n / 2) else aux (i + 1) (3 * n + 1) ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":2,"num_loc":12,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-03-19T12:58:30.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"goiabae"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/goiabae","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}},{"uuid":"25ba62e75b2c4aa098179099f04fb282","snippet":"def Positive := { x : Nat // 0 < x } private partial def stepsU64 (n : UInt64) (acc : Nat) : Nat := if n ≤ 1 then acc else if n &&& 1 == 0 then stepsU64 (n >>> 1) (acc + 1) else stepsU64 (n * 3 + 1) (acc + 1) def steps (n : Positive) : Nat := stepsU64 n.val.toUInt64 0 ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":2,"num_loc":9,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-05-24T16:45:13.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"david82"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/david82","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}},{"uuid":"36c5d0dbe5554fb78ff9d3c9858b7077","snippet":"def Positive := { x : Nat // 0 < x } partial def steps (n : Positive) : Nat := if n.val == 1 then 0 else if h0 : n.val % 2 = 0 then have h : n.val / 2 > 0 := by simp have h1 := n.property ","num_views":0,"num_stars":0,"num_comments":0,"representation_num_published_solutions":1,"num_iterations":1,"num_loc":17,"iteration_status":"no_automated_feedback","published_iteration_head_tests_status":"passed","published_at":"2026-05-04T02:56:01.000Z","is_out_of_date":false,"language":"haskell","author":{"handle":"ramhuw"},"exercise":{"title":"Collatz अनुमान","icon_url":"https://assets.exercism.org/exercises/collatz-conjecture.svg"},"track":{"title":"Lean","icon_url":"https://assets.exercism.org/assets/graphics/missing-track-e3d861058d4702c1dc4036617689249659b8d37d.svg","highlightjs_language":"haskell"},"links":{"public_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/solutions/ramhuw","private_iterations_url":"https://exercism.org/hi/tracks/lean/exercises/collatz-conjecture/iterations"}}],"meta":{"current_page":1,"total_count":9,"total_pages":1,"unscoped_total":9}}}}}

भाषा ट्रैक

Jiki के साथ कोड करना सीखिए

आपकी यात्रा

आपके पसंदीदानया

Exercism के खास फायदे

कम्युनिटी वीडियो

संक्षिप्त परिचय शृंखला

इंटरव्यू और कहानियाँ

Discord

फोरम

शुरुआत करें

मेंटर बनें

डॉक्स

योगदानकर्ता

अनुवादकनया

दान करें

Exercism के बारे में

हमारा प्रभाव

GitHub सिंकरनया

इनसाइडर्स