NiuMaAgent
数论 · 个人研究

Collatz 前沿研究

Lean 形式化 · Python 数值实验 · 10 大研究方向

在 lean-playground 中完成的 Collatz 猜想前沿研究：120 行 Lean 4 形式化（含 collatz_pow_two 定理证明与 #eval 实例验证），1700+ 行 Python 计算实验覆盖 10 个研究方向，最终沉淀为一份含完整数据表与核心结论的研究报告。

10
研究方向
1700+
行 Python 实验
120
行 Lean 形式化
3
个 Python 脚本
返回冰雹猜想浏览十大方向
目录Lean 形式化十大研究方向核心结论研究方法参考资料
Lean 形式化

用 Lean 4 把猜想写进证明器

用 Lean 4 形式化定义 Collatz 映射、陈述 CollatzConjecture 命题，并严格证明了 collatz_pow_two——2^k 经 k 步迭代到达 1。

3
形式化构件
1
已证定理
111 步
#eval 27 验证
9232
#eval 27 峰值

Collatz.lean · 120 行——把“2^k 经 k 步到 1”这一可证情形严格形式化，为完整猜想留下可扩展的证明框架。

collatz 映射偶数除以 2，奇数乘 3 加 1
def collatz (n : Nat) : Nat :=
  if n % 2 = 0 then n / 2 else 3 * n + 1
collatz_pow_two2^k 经 k 步到达 1（已证明）
theorem collatz_pow_two (k : Nat) :
  iterate collatz k (2 ^ k) = 1 := by
  induction k with
  | zero => rfl
  | succ k ih => ...
#eval 27实例验证：27 的 111 步序列，峰值 9232
#eval total_stopping_time 27   -- some 111
#eval max_of_seq (collatz_steps 27 200)  -- 9232
十大研究方向

多角度逼近冰雹猜想

从陶哲轩的概率方法到 2-adic 动力系统，十个方向各自给出一个视角；合起来看，它们共同刻画了 Collatz 映射的复杂结构。

№01

陶哲轩 2019 定理数值验证

理论验证

对 1..50000 随机抽取 3000 个数，轨道最小值与起始值的对数比率均值仅 0.072，且 100% 低于 0.5。

平均 log(min)/log(n) = 0.072 · 100% 比率 < 0.5
  • 陶哲轩
  • 几乎有界
  • 随机样本

№02

停止时间统计规律

核心发现

统计规律

实测比值随数量级趋于 ~9.7，显著高于理论预测 6.95。根源是 v2(3n+1) 的结构性约束：n≡1 (mod 4) 触发更长的偶数下降段，奇偶性并非独立。

实测 ~9.7 vs 理论 γ=6.952 · v2(3n+1) 结构约束
  • 核心发现
  • 随机游走
  • mod 4

№03

2-adic 动力学分析

结构分析

对 k=3..8，恒只有 2 个循环：平凡不动点 0→0 与经典 4→2→1 循环，后者占据 98.4% 的吸引域。

Z/2^k 恒 2 个循环 · 4→2→1 占 98.4% 吸引域
  • 2-adic
  • 循环结构
  • 吸引域

№04

Benford 定律验证

数值方法

200 条轨道共 21227 个点总体拟合良好（χ²≈147），但首位数字 4 有轻微偏好（+18.8%），3 与 6 轻微偏离，可能源于 3n+1 中因子 3 的乘法效应。

χ² ≈ 147 · 首位 4 偏好 +18.8%
  • Benford
  • 首位数字
  • 统计拟合

№05

Syracuse 压缩比分析

统计规律

25000 个奇数的几何平均压缩比为 0.563 < 1，证明总体上存在压缩趋势。虽然 v2≥3 时局部膨胀（平均 >1），但概率足够低，几何平均仍小于 1。

几何平均压缩比 0.563 < 1
  • Syracuse
  • 压缩比
  • 几何平均

№06

奇偶性序列的熵分析

统计规律

条件熵（~0.62）显著低于边际熵（~0.95），3 步上下文即可显著降低不确定性——奇偶性存在短程可预测性，并非独立。

条件熵 0.62 < 边际熵 0.95
  • 条件熵
  • 信息论
  • 短程可预测

№07

停止时间序列的分形特征

结构分析

Hurst 指数 H=0.602 > 0.5，序列有轻度持续性（long memory）；自相关 lag1=0.287、lag5=0.108、lag10=0.080。

Hurst 指数 0.602 > 0.5
  • Hurst
  • 分形
  • 自相关

№08

上升-下降模式

定理级发现

定理级发现

轨道中不可能有连续两步上升——奇数步后 3n+1 必为偶数，下一步必下降。实测 5000 个数的最大连续上升步数恒为 1。

最大连续上升步数 = 1
  • 定理级发现
  • 模式约束
  • 必然下降

№09

广义 3n+d 映射的循环分类学

临界点

结构分析

系统研究 d=1,5,7,11,13,17,19,23,25,29：d=1 是唯一使 1→4→2→1 成为唯一吸引子的参数。改变 d 会引入新的非平凡循环——Collatz 猜想在参数空间中处于临界点。

d=1 唯一全局吸引子 · 参数临界点
  • 临界点
  • 3n+d 族
  • 相变

№10

高延迟数的结构特征

统计规律

top 15 高延迟数全部是奇数（除 54 来自 27 的轨道），二进制中 1 的密度高，强烈偏好 n≡7 (mod 8) 或 15 (mod 16)。

奇数 · 二进制 1 密度高 · n≡7/15 (mod 16)
  • 高延迟
  • mod 16
  • 二进制

共 10 个方向 · 完整数据表与复现代码见 lean-playground 的 collatz_research_report.md

核心结论

这些实验说明了什么

十组实验指向几个相互关联的深层事实——Collatz 映射远比独立随机游走更“聪明”。

本页为探索性研究 · 结论未经同行评审

停止时间系统性偏离理论值

实测比值 ≈9.7 显著高于理论 γ=6.952，根源是 v2(3n+1) 对偶数下降段的约束（n≡1 mod 4 触发更长的下降）。

方向 #2

2-adic 结构高度稳定

Z/2^k 上恒只有 2 个循环，且 1→4→2→1 占据 98.4% 的吸引域。

方向 #3

短程可预测、长程近随机

奇偶性条件熵 0.62 < 边际熵 0.95；Hurst 0.602 表明轻度持续性，但不足以推断收敛。

方向 #6 / #7

不存在连续两步上升

轨道中不可能出现连续两次 n→3n+1，这是可严格证明的模式约束。

方向 #8

d=1 是唯一的临界点

广义 3n+d 中仅 d=1 使 1 成为全局吸引子——Collatz 猜想的参数恰好处于临界位置。

方向 #9

最深刻的定理级发现：轨道中不可能有连续两步上升——这是唯一能严格证明的模式约束，也解释了为什么随机游走模型总是“偏高”。

研究方法

Lean + Python 双轨推进

形式化证明（Lean 4）负责“可证”的部分，数值实验（Python）负责“可观察”的部分——两条线互相印证。

Collatz.lean

Lean 4 形式化

120 行
  • collatz_pow_two 定理证明
  • #eval 27 序列 / 峰值 9232

collatz_frontier_research.py

核心计算实验

786 行
  • 陶哲轩定理验证
  • 停止时间统计
  • 2-adic 循环
  • Benford / 熵 / Hurst

collatz_deep_dive.py

深入机制挖掘

569 行
  • 停止时间偏移来源
  • 3n+d 循环分类
  • 延迟收敛结构

collatz_corrected_model.py

随机游走修正模型

350 行
  • v2(3n+1) 结构约束
  • 修正理论比值

collatz_research_report.md

研究结论汇总

完整报告
  • 10 方向数据表
  • 核心结论
  • 可复现实验

复现方式：在 lean-playground 目录下，用 lake env lean Collatz.lean 验证 Lean 形式化；用 python3 collatz_frontier_research.py 重跑全部数值实验。

参考资料

深入阅读

本页内容整理自 lean-playground 研究项目，以下为相关原始资料。

本项目为个人研究，结论未经同行评审，仅作为探索性参考。完整代码与数据见 lean-playground 仓库。

加入 牛马智能体，开启你的开源科研之路

NiuMaAgent 以 Apache License 2.0 开源协议发布。欢迎 Fork、提交 Issue， 与全球科研人员共建 AI4Science 生态。

Gitee 上 Star反馈问题