关于埃尔德什 - 塞尔弗里奇奇数覆盖问题的内核检查排除：整数集\(\mathbb{Z}\)的任何奇数覆盖的最小公倍数超过10000
Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of $\mathbb{Z}$ Has lcm Exceeding 10000
浏览论文内容
中文总结 AI 辅助
研究埃尔德什 - 塞尔弗里奇奇数覆盖问题，通过Lean 4形式化证明，利用密度论证、丰富度下限、中国剩余容量证书及枚举等方法，得出整数集\(\mathbb{Z}\)的奇数覆盖其模最小公倍数超10000的结论，贡献在于提供内核检查的认知成果。
中文摘要 AI 辅助
埃尔德什 - 塞尔弗里奇奇数覆盖问题（埃尔德什问题#7）询问是否存在一个整数集\(\mathbb{Z}\)的覆盖系统，其模都是奇数、不同且大于1。该问题尚未解决。我们给出了一个由证明内核进行端到端检查的Lean 4形式化证明，即任何由有限多个具有不同奇数模且大于1的同余类对\(\mathbb{Z}\)的覆盖，其模的最小公倍数超过10000。证明包括形式化的密度论证（由大于1的\(N\)的除数覆盖会迫使\(2N \leq \sigma_1(N)\)，所以最小公倍数是丰富数或完全数）、内核检查的丰富度下限（没有奇数\(N < 945\)符合条件）、一族中国剩余容量证书——针对每个\(N\)可判定的算术不等式，每个都反驳了所有以大于1的不同模整除该\(N\)的覆盖——针对\(10^4\)以下的所有23个奇数丰富数，以及内核检查的枚举确定这23个是唯一的奇数非亏缺候选数。结果被转换到谷歌 - 深度思维/形式猜想中埃尔德什#7的官方严格覆盖系统\(\mathbb{Z}\)表述中，在\(\mathbb{Z}\)的覆盖和\(\mathbb{Z}/N\mathbb{Z}\)上的有限检查之间有一个双向周期性桥梁，适用于处理未来SAT风格的搜索输出。所有63个已发表的定理仅依赖于特定的扩展、链接，在可信基中没有歉意、没有原生判定、没有求解器。数学内容是已知的——密度论证是常见的，并且存在更大的未经认证的覆盖数分类——所以贡献是认知性的而非数学性的：这些排除是Lean内核的定理，在持续集成中通过机械强制的公理门实现。
英文摘要
The Erdős-Selfridge odd covering problem (Erdős problem #7) asks whether a covering system of $\mathbb{Z}$ exists whose moduli are all odd, distinct, and greater than 1. The problem is open. We present a Lean 4 formalization, checked end to end by the proof kernel, of the exclusion: any covering of $\mathbb{Z}$ by finitely many congruence classes with distinct odd moduli > 1 has lcm of the moduli exceeding 10000. The proof composes a formalized density argument (a covering by divisors of $N$ exceeding 1 forces $2N \le σ_1(N)$, so the lcm is abundant or perfect), a kernel-checked abundancy floor (no odd $N < 945$ qualifies), a family of Chinese-Remainder capacity certificates -- decidable per-$N$ arithmetic inequalities each refuting every covering with distinct moduli > 1 dividing that $N$ -- for all 23 odd abundant numbers below $10^4$, and a kernel-checked enumeration establishing that those 23 are the only odd non-deficient candidates. The result is transported to the official StrictCoveringSystem $\mathbb{Z}$ formulation of Erdős #7 in google-deepmind/formal-conjectures, with a bidirectional periodicity bridge between coverings of $\mathbb{Z}$ and finite checks over $\mathbb{Z}/N\mathbb{Z}$ suitable for consuming future SAT-style search output. All 63 published theorems depend on exactly propext, Classical.choice, and Quot.sound: no sorry, no native_decide, no solver in the trusted base. The mathematical content is known -- the density argument is folklore, and far larger uncertified classifications of covering numbers exist -- so the contribution is epistemic rather than mathematical: these exclusions are theorems of the Lean kernel, with an axiom gate enforced mechanically in continuous integration.
