自然密度でほとんど有界なCollatz軌道の対数時間（AI, Lean）
新しいLean形式証明により、ほとんどすべての正整数に対してCollatz過程が任意の増大する閾値以下に対数時間で到達することが示され、明示的な定数（Syracuseステップ145、Collatzステップ436）が与えられました。この結果は完全な予想を証明するものではありませんが、重要な密度結果です。
数論と力学系の分野において、Collatz予想は長年にわたり数学者の関心を集めてきました。最近、研究者Lech Mazurは証明プラットフォームLean上で重要な定理を形式化しました：自然密度でほとんど有界なCollatz軌道の対数時間です。この定理は、ほとんどすべての正整数に対して、Collatz過程が任意に増大する閾値以下に対数ステップで到達することを示しています。
具体的には、定理には2つのバージョンがあります。1つ目はSyracuseステップ（奇数から奇数の変換のみ）に関するもので、密度1の奇数出発点に対して、最大145·log Nステップ以内に閾値以下に達します。2つ目は生のCollatzステップ（すべての偶奇変換を含む）に関するもので、密度1の正整数出発点に対して、最大436·log Nステップ以内に閾値以下に達します。これらのバージョンは異なる定義域を持ち、混同してはなりません。
さらに、定理から系として、密度1の出発点に対して、log N/(2 log 2) < m ≤ 436·log Nを満たす指数mが存在し、Collatz^m(N) < √Nとなることが導かれます。つまり、平方根目標が対数時間ウィンドウ内で到達可能です。
証明の核心は、Rhin位相ギャップを利用し、定量速度エンジンを通じて固定目標制御をSyracuse結論に変換し、さらに2-adicリフトを用いて生のCollatz結論を得ることにあります。証明全体はLeanで完全に形式化されており、599個のLeanファイル、18万行以上のコードを含み、すべての証明ステップがチェックされています。
注意すべき点として、この定理はCollatz予想そのものを証明するものではなく、すべての出発点が1に到達することを保証しません。密度ゼロの例外集合を許容します。閾値は無限大に発散する必要がありますが、単調である必要はありません。この結果はTerrasの有限べき乗節約界とは独立であり、依存関係とはみなされません。
この形式化された成果は、Collatz問題に対する重要な密度の視点を提供し、より強い時間定数、明示的な収束速度、および類似の力学系の研究の基礎となります。