Erdős-Mollin-Walsh 猜想在 $10^{14}$ 以下的核验证
A Kernel-Certified Verification of the Erdős-Mollin-Walsh Conjecture below $10^{14}$
浏览论文内容
中文总结 AI 辅助
该研究通过 Lean 4 证明内核端到端验证了 Erdős-Mollin-Walsh 猜想在 $10^{14}$ 以下成立，消除了受信任的枚举代码，首次实现了有限界下的机器检查证明。
中文摘要 AI 辅助
Erdős 问题 364 询问是否存在三个连续的高次幂数（powerful number），其中若 $p \mid n$ 蕴含 $p^2 \mid n$，则称 $n$ 为高次幂数。Erdős（1976年）以及 Mollin 和 Walsh（1986年）独立地猜想不存在这样的三个连续高次幂数；abc 猜想蕴含至多存在有限个。该猜想至今仍未解决。我们首次在有限界内对该猜想进行了由证明内核端到端检查的验证：在 Lean 4 中通过机器检查的定理确立了在 $10^{12}$ 以下和 $10^{14}$ 以下不存在三个连续的高次幂数，两个定理的公理足迹恰好为 {propext, this http URL, this http URL }——没有 sorry，没有 native_decide，没有受信任的外部计算。这些陈述使用了 google-deepmind/formal-conjectures 对该问题形式化的逐字节相同的词汇表，并且我们抽象地证明了开放猜想蕴含每个有界形式，从而确定了陈述的对应关系。该证明通过模 4 论证将搜索范围缩减到奇数，将每个奇数高次幂数表示为 $a^2 b^3$，其中 $a, b$ 为奇数且 $b$ 无平方因子，通过一个带燃料的、内核可归约的生成器枚举所有奇数高次幂数，该生成器的完备性被证明一次并实例化到 3,524 个逐区间布尔证书中，并通过显式的非高次幂性见证消除了七个幸存的距离为 2 的数对（即 OEIS A076445 中 $10^{14}$ 以下的成员）。每个证书的期望值由 Python 引擎独立计算，因此每个内核检查的等式同时充当跨实现的一致性验证。总认证内核时间约为 46 CPU 小时。更大的未经认证的计算存在（穷举至 $10^{22}$；有条件地至约 $7.38 \times 10^{28}$）；我们的贡献不是计算记录，而是从证据链中消除了受信任的枚举代码。
英文摘要
Erdős problem 364 asks whether three consecutive powerful numbers exist, where $n$ is powerful if $p \mid n$ implies $p^2 \mid n$. Erdős (1976) and, independently, Mollin and Walsh (1986) conjectured that none do; the $abc$ conjecture implies at most finitely many. The conjecture remains open. We present the first verification of the conjecture at any finite bound that is checked end to end by a proof kernel: machine-checked theorems in Lean 4 establishing that no triple of consecutive powerful numbers exists below $10^{12}$ and below $10^{14}$, with the axiom footprint of both theorems being exactly {propext, Classical.choice, Quot.sound} -- no sorry, no native_decide, no trusted external computation. The statements are phrased in the byte-identical vocabulary of the google-deepmind/formal-conjectures formalization of the problem, and we prove abstractly that the open conjecture implies each bounded form, pinning the statement correspondence. The proof reduces the search to odd numbers via a mod-4 argument, represents every odd powerful number as $a^2 b^3$ with $a, b$ odd and $b$ squarefree, enumerates all odd powerful numbers by a fueled, kernel-reducible generator whose completeness is proved once and instantiated across 3,524 per-interval Boolean certificates, and eliminates the seven surviving distance-2 pairs (the members of OEIS A076445 below $10^{14}$) by explicit non-powerfulness witnesses. Every certificate's expected values are computed independently by a Python engine, so each kernel-checked equality doubles as a cross-implementation agreement. Total certified kernel time is roughly 46 CPU-hours. Larger uncertified computations exist (exhaustive to $10^{22}$; conditionally to about $7.38 \times 10^{28}$); our contribution is not a computational record but the elimination of trusted enumeration code from the evidence chain.
发表机构
- Millennium Research（千年研究）
机构由 AI 辅助整理，请以论文原文为准。
