DeepMind 用 Lean 4 把 Erdős-Selfridge 问题的一个下界（lcm>10000）变成了机器可检查的定理。对形式化数学和定理证明器感兴趣的话，这个工作很硬核。
Erdős-Selfridge 奇数覆盖问题（Erdős #7）询问是否存在模数全为奇数、互异且大于 1 的覆盖系统。该论文在 Lean 4 中形式化证明了如下排除结果：任何由有限个同余类组成的奇数覆盖（模数互异且 >1）的最小公倍数必须超过 10000。证明结合了形式化的密度论证（覆盖的 lcm 必须是丰数或完全数）、核检查的丰数下界（无奇数 N<945 满足条件）、对 10000 以下全部 23 个奇数丰数的中国剩余容量证明，以及核检查的枚举。结果被移植到 google-deepmind/formal-conjectures 中的官方 StrictCoveringSystem ℤ 表述。全部 63 个已发布定理仅依赖 propext、Classical.choice 和 Quot.sound，无 any sorry 或 native_decide。
Kernel-Checked Exclusions for the Erdős-Selfridge Odd Covering Problem: Any Odd Covering of $\mathbb{Z}$ Has lcm Exceeding 10000
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.