Erdős问题647的核检验排除证明
A Kernel-Checked Exclusion Certificate for Erdős Problem 647
浏览论文内容
中文总结 AI 辅助
该研究在Lean 4中构建了无问题特定公理的端到端核检验排除证明，证实24 < n ≤ 10^9的Erdős问题647无解，核心贡献是提升了结果的信任基础。
中文摘要 AI 辅助
Erdős问题647询问是否存在大于24的整数n满足max_{m<n}(m + τ(m)) ≤ n + 2，其中τ为除数计数函数。此前的计算搜索通过直接筛法排除了10^12以内的解，通过依赖native_decide的Lean组件进行模约化，排除了约9.17×10^18以内的解，但这些计算均不在任何证明核内。我们给出了首个由证明核端到端检验的排除结果：在Lean 4中，以公理闭包恰好为{propext, this http URL, this http URL}（无sorry、无native_decide、无问题特定公理）证明，24 < n ≤ 10^9范围内不存在解。该证明重放了6,685,922个因式分解见证的链，其排除区间在(24, 10^9]上拼接；仅需1024以下素数的素性事实，是支配区间论证的有限、完全证明形式，而该论证的渐近步骤是2026年1月撤回的该问题声明中被发现的漏洞。生成流水线由另外两个独立实现交叉检验：编译后的开发版本通过独立的lean4checker重放，两个源自源代码的验证分支（由gcc和clang从源代码编译的Lean工具链、无缓存重建的mathlib）在两种架构上的三次构建中逐字节复现了提交的证明，olean摘要完全一致。我们的范围比所引用的计算前沿低3至10个数量级；贡献在于信任基础，而非范围。
英文摘要
Erdős problem 647 asks whether any $n > 24$ satisfies $\max_{m<n}(m + τ(m)) \le n + 2$, where $τ$ is the divisor-count function. Computational searches have excluded solutions up to $10^{12}$ by direct sieve and up to roughly $9.17 \times 10^{18}$ within a modular reduction whose Lean component relies on native_decide; those computations sit outside any proof kernel. We give the first exclusion checked end to end by one: no solution exists with $24 < n \le 10^9$, proved in Lean 4 with axiom closure exactly {propext, Classical.choice, Quot.sound} -- no sorry, no native_decide, no problem-specific axiom. The proof replays a chain of 6,685,922 factorization witnesses whose excluded intervals concatenate across $(24, 10^9]$; it needs no primality facts beyond primes below 1024, and it is the finite, fully proved form of a domination-interval argument whose asymptotic step was the identified gap in a withdrawn January 2026 claim on this problem. The generation pipeline is cross-checked by two further independent implementations, the compiled development replays through the standalone lean4checker, and two from-source verification legs -- Lean toolchains compiled from source by gcc and by clang, mathlib rebuilt with no cache -- reproduce the committed certificates byte for byte, with olean digests identical across three builds on two architectures. Our range is three to ten orders of magnitude below the computational frontiers we cite; the contribution is the trust base, not the range.
