すべての正の整数は、コラッツの操作で 1 に到達するか？

偶数なら n/2、奇数なら 3n+1 という操作を繰り返すと、どの正の整数から始めても 1 に到達するかを決定せよ。

Decide whether iterating n -> n/2 for even n and n -> 3n+1 for odd n reaches 1 from every positive starting value.

The strongest partial result is Tao's: almost all orbits attain almost bounded values. The strongest structural result is Conway's: closely related generalized problems are undecidable, which bounds what any general method can hope to do.

解決したかどうかは、問いではなくアプローチごとに決まります。Atlas は判定しません。外部の判定者が何をしたかを記録します。

• Lean 4 formalization (formal-conjectures)

  形式証明

  到達状況

  未着手

  判定者

  the Lean 4 typechecker, against the pinned toolchain · 型検査

  定式化

  Every positive n reaches 1 under iteration of the Collatz step, stated in Lean 4.問いと同値Lean v4.33.1 + mathlib@0df444a3 (formal-conjectures@fc2696b2)検証対象を見る

  保たれているもの

  • The iteration and the target value 1
  • The quantifier over all positive n

  加えられた仮定・条件

  • An explicit positivity hypothesis n > 0

  Statement only.

• Density and almost-all results

  査読付きの証明

  到達状況

  進行中

  判定者

  the analysis and number theory communities, through journal peer review · 査読

  定式化

  Prove that almost every orbit descends below any given growth function, and push 'almost every' to 'every'.問いより弱い

  保たれているもの

  • Handles almost all starting values, in a precise density sense

  弱まっているもの

  • Says nothing about any particular integer, and the conjecture is about every integer

  加えられた仮定・条件

  • A logarithmic density formulation that the original statement does not have

  閉じた道

  • Conway showed that natural generalizations of the Collatz problem are undecidable, so no general method can decide the whole family; a proof must use something specific to the 3n+1 map.無条件
    • paperJ. H. Conway, Unpredictable iterations, Proc. 1972 Number Theory Conference, Univ. of Colorado, Boulder (1972) 49-52Generalized Collatz-style problems are undecidable

  証拠

  • preprintarXiv:1909.03562T. Tao, Almost all orbits of the Collatz map attain almost bounded values (2019)

• Exhaustive computation

  計算による判定

  到達状況

  進行中

  判定者

  execution: the search can be repeated · 実行

  定式化

  Verify convergence for every starting value up to a bound.問いより弱い

  保たれているもの

  • The exact claim for each value checked

  弱まっているもの

  • Finitely many starting values

  加えられた仮定・条件

  • Trust in the search implementation

  閉じた道

  • A finite search cannot settle a statement about all integers; it can only refute it.無条件
    • paperdoi:10.1016/j.jpdc.2020.11.005D. Barina, Convergence verification of the Collatz problem, J. Supercomput. / J. Parallel Distrib. Comput.: verification beyond 2^68

  証拠

  • paperdoi:10.1016/j.jpdc.2020.11.005D. Barina, Convergence verification of the Collatz problem, J. Supercomput. / J. Parallel Distrib. Comput.: verification beyond 2^68

• repositoryhttps://github.com/google-deepmind/formal-conjectures@fc2696b2f863e642ef1452938b0f031f5af5bed3FormalConjectures/Wikipedia/CollatzConjecture.lean:50
• paperJ. H. Conway, Unpredictable iterations, Proc. 1972 Number Theory Conference, Univ. of Colorado, Boulder (1972) 49-52Generalized Collatz-style problems are undecidable

URI

https://atlasalt.com/q/e05bdc6d-3000-439b-8dcf-ff8fbfcc6ba2

登録

2026-09-17

最終レビュー

2026-09-19

次回レビュー期限

2027-09-19

版

68cab21c2655

ライセンス

CC-BY-4.0

立場

record_only（Atlas は判定しない）