AxiomProver 将 Collatz 正密度显式界优化到 87640，并扩展到任意非 3 倍数目标

Kenny Lau / Axiom Math 的 CollatzPositiveDensity 项目在 10 月 14 日形成新的强化里程碑：22:21 UTC 的提交把显式常数优化到 87640，并扩展 even target 情形；随后补齐 formalization metadata，同日 Hexagon 发布论文。写 L=2^(2^(2^87640))，则对所有 X≥2^L，至少 X/L 个正整数 n<X 在 floor(10.46 log n) 次 ordinary Collatz steps 内到达 1；项目还给出 odd-starting / accelerated-step 版本，以及对任意 3∤t 的 prescribed-target 正密度结论。作者说明研究目标由人提出，而 AxiomProver 自主产生数学推导并生成 Lean formalization；Challenge 只依赖 Mathlib，Comparator 检查四个主结果，formalization metadata 记录无 sorry 且仅使用 Lean 三个标准公理。