{"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/el/tracks/lean/exercises/collatz-conjecture/solutions/oxe-b","private_iterations_url":"https://exercism.org/el/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/el/tracks/lean/exercises/collatz-conjecture/solutions/efwhofmann","private_iterations_url":"https://exercism.org/el/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/el/tracks/lean/exercises/collatz-conjecture/solutions/takah29","private_iterations_url":"https://exercism.org/el/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/el/tracks/lean/exercises/collatz-conjecture/solutions/setsunica","private_iterations_url":"https://exercism.org/el/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/el/tracks/lean/exercises/collatz-conjecture/solutions/keiraville","private_iterations_url":"https://exercism.org/el/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/el/tracks/lean/exercises/collatz-conjecture/solutions/menketechnologies","private_iterations_url":"https://exercism.org/el/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/el/tracks/lean/exercises/collatz-conjecture/solutions/goiabae","private_iterations_url":"https://exercism.org/el/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/el/tracks/lean/exercises/collatz-conjecture/solutions/david82","private_iterations_url":"https://exercism.org/el/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/el/tracks/lean/exercises/collatz-conjecture/solutions/ramhuw","private_iterations_url":"https://exercism.org/el/tracks/lean/exercises/collatz-conjecture/iterations"}}],"meta":{"current_page":1,"total_count":9,"total_pages":1,"unscoped_total":9}}}}}

Γλώσσες προγραμματισμού

Μάθε προγραμματισμό με το Jiki

Το Ταξίδι σου

Τα Αγαπημένα σουΝέο

Προνόμια του Exercism

Βίντεο της Κοινότητας

Σειρά σύντομων εισαγωγών

Συνεντεύξεις και ιστορίες

Discord

Φόρουμ

Ξεκινώντας

Καθοδήγηση

Τεκμηρίωση

Συνεισφέροντες

ΜεταφραστέςΝέο

Κάνε δωρεά

Σχετικά με το Exercism

Ο αντίκτυπός μας

Συγχρονισμός GitHubΝέο

Insiders