发表机构
Millennium Research（千年研究）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对 Erdős 问题 414，利用 Lean 4 内核在公理门下形式化前沿引理并生成核校验证书，验证了 $N$ 达 $10^8$ 时所有低于 $N$ 的正整数对在 $h(n)=n+\tau(n)$ 下合并，证书仅含 44,530 个条目，但未证明猜想。
AI 中文摘要
设 $h(n) = n + \tau(n)$，其中 $\tau$ 表示除数计数函数。在 Spiro 之后，Erdős 和 Graham 提出如下问题：任意两个正整数在 $h$ 作用下的轨道是否最终共享一个点（Bloom 列表上的问题 414）。该问题尚未解决，有限计算无法将其闭合；关于该问题没有任何内容经过证明内核的校验，且形式化猜想仓库中的陈述带有 sorry。我们在一个公理门（公理恰好为 propext、this http URL、this http URL；无 sorry；无 native_decide）下，重放可通过 Lean 4 内核认证的内容。Li 记录的三个基本事实，即合并是等价关系、$\tau(n)$ 恰好对平方数为奇数、以及 $\tau(n)$ 以 $2\sqrt{n}$ 为界从而轨道不会跳过任何平方环 $[k^2, (k+1)^2)$，均被形式化，并且他的前沿引理以窗口形式被形式化：从低于水平 $N$ 开始的每个轨道在 $N$ 下方 $\lceil 2\sqrt{N} \rceil$ 范围内有一个点。前沿引理成为一个证书：$N$ 下方 $\lceil 2\sqrt{N} \rceil$ 个 $\tau(m)$ 值，以及 $N$ 上方直到穿过交叉点的轨道合并为止的轨道点。其可靠性是一个内核校验定理，且认证的阶梯表明：对于 $N = 10^5, 10^6, 10^7, 10^8$，每对低于 $N$ 的正整数都会合并；$10^8$ 处的证书有 44,530 个条目，而非 $10^8$ 个。每个账本和每个引用的计数均由两个不共享代码的程序生成，它们通过哈希一致。我们记录了关于非合并对的已知信息，并测量了 Li 所界的退出集大小。这里没有任何内容是该猜想的证明。
英文摘要
Let $h(n) = n + τ(n)$, where $τ$ counts divisors. Erdős and Graham asked, after Spiro, whether the orbits of any two positive integers under $h$ eventually share a point (Problem 414 on Bloom's list). The problem is open, and a finite computation cannot close it; nothing about it has been checked by a proof kernel, and the statement in the formal-conjectures repository carries a sorry. We replay what can be certified through the Lean 4 kernel under an axiom gate (axioms exactly propext, Classical.choice, Quot.sound; no sorry; no native_decide). Three elementary facts recorded by Li, namely that coalescence is an equivalence relation, $τ(n)$ is odd exactly for squares, and $τ(n)$ is bounded by $2\sqrt{n}$ so that orbits skip no square annulus $[k^2, (k+1)^2)$, are formalized, and his frontier lemma is formalized in a window form: every orbit started below a level $N$ has a point within $\lceil 2\sqrt{N} \rceil$ below $N$. The frontier lemma becomes a certificate: the $\lceil 2\sqrt{N} \rceil$ values $τ(m)$ just below $N$ and the orbit points above $N$ until the orbits through the crossing points have merged. Its soundness is a kernel-checked theorem, and the certified rungs state that every pair of positive integers below $N$ coalesces for $N = 10^5, 10^6, 10^7, 10^8$; the certificate at $10^8$ has 44,530 entries rather than $10^8$. Every ledger and every quoted count was produced by two programs sharing no code that agree by hash. We record what is known about a non-coalescing pair and measure the exit-set sizes Li bounds. Nothing here is a proof of the conjecture.
Comments6 pages. Lean sources, certificates, ledgers and verification logs at https://github.com/ibrahimmian36/hastatus (release v1)
