自然密度下幾乎有界的Collatz軌道在對數時間內（AI, Lean）
一項新的Lean形式化證明表明，對於幾乎所有正整數，Collatz過程能在對數時間內下降到任何增長閾值以下，並給出了明確的常數（Syracuse步驟145，原始Collatz步驟436）。該結果並未證明完整猜想，但代表了重要的密度結果。
在數論和動力系統領域，Collatz猜想長久以來吸引着數學家的關注。近日，研究者Lech Mazur在證明平台Lean上形式化了一個重要定理：自然密度幾乎有界的Collatz軌道在對數時間內。該定理表明，對於幾乎所有正整數，Collatz過程能在對數步驟內下降到任何給定的增長閾值以下。
具體而言，定理包含兩個版本。第一個版本針對Syracuse步驟（僅考慮奇數到奇數的變換），對密度為1的奇數起始點，在最多145·log N步內達到閾值以下。第二個版本針對原始Collatz步驟（包括所有奇偶變換），對密度為1的正整數起始點，在最多436·log N步內達到閾值以下。這兩個版本覆蓋了不同的域，不可混淆。
此外，定理還得出一個推論：對於密度為1的起始點，存在一個指數m滿足log N/(2 log 2) < m ≤ 436·log N，使得Collatz^m(N) < √N。即平方根目標在對數時間窗口內可達。
該證明的核心是利用Rhin相位間隙，通過定量速率引擎將固定目標控制轉化為Syracuse結論，再利用2-adic提升得到原始Collatz結論。整個證明在Lean中完全形式化，包含599個Lean文件，超過18萬行代碼，所有證明步驟均通過檢查。
值得注意的是，該定理並不證明Collatz猜想本身，也不保證所有起始點最終到達1。它允許一個密度為零的例外集存在。閾值必須趨向無窮，但不必單調。該結果與Terras的有限冪節省界是獨立的，不可視為依賴關係。
這一形式化成果為Collatz問題提供了重要的密度視角，併為後續研究更強的時間常數、顯式收斂速率以及類似動力系統提供了基礎。