{"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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/oxe-b","private_iterations_url":"https://exercism.org/uk/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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/efwhofmann","private_iterations_url":"https://exercism.org/uk/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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/takah29","private_iterations_url":"https://exercism.org/uk/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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/setsunica","private_iterations_url":"https://exercism.org/uk/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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/keiraville","private_iterations_url":"https://exercism.org/uk/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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/menketechnologies","private_iterations_url":"https://exercism.org/uk/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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/goiabae","private_iterations_url":"https://exercism.org/uk/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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/david82","private_iterations_url":"https://exercism.org/uk/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":"Гіпотеза Коллатца","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/uk/tracks/lean/exercises/collatz-conjecture/solutions/ramhuw","private_iterations_url":"https://exercism.org/uk/tracks/lean/exercises/collatz-conjecture/iterations"}}],"meta":{"current_page":1,"total_count":9,"total_pages":1,"unscoped_total":9}}}}}

Мовні треки

Вчимося програмувати з Jiki

Подорож

ОбранеНове

Переваги Exercism

Відео спільноти

Серія коротких вступів

Інтервʼю та історії

Discord

Форум

З чого почати

Наставництво

Документація

Учасники

ПерекладачіНове

Пожертвувати

Про Exercism

Наш вплив

Синхронізатор GitHubНове

Інсайдери