证明写完，机器核过，才算数。

只有两种结案

• 存在 — 给出一组具体同余类，并在 Lean 中证明它们覆盖 ℤ（等价于覆盖 ℤ/Nℤ，N = lcm(nᵢ)）。
• 不存在 — 证明任意满足条件的有限组合同余类都留出空隙，并通过 Lean kernel。

历史立场相反：Erdős 倾向存在，悬赏 25 美元给「证明不存在」；Selfridge 倾向不存在，把「拿出显式例子」的赏金加到 2000 美元。QED 不预设哪一边对。

已知边界（QED 站在这些结果之上）

• 2 或 3 — 任意互异模覆盖至少有一个模被 2 或 3 整除。奇数情形 ⇒ 必须碰 3。Hough–Nielsen, Duke Math. J. 2019
• 9 或 15 — 若奇数覆盖存在，则模数的 lcm 被 9 或 15 整除；无平方因子的奇数覆盖不存在。Balister–Bollobás–Morris–Sahasrabudhe–Tiba, Invent. Math. 2022
• σ(N) ≥ 2N — 密度门槛：模均整除 N 且大于 1，则 Σ1/nᵢ ≥ 1，故 N 必为奇丰富数或奇完全数。经典密度论证
• lcm > 10000 — 任何奇数互异模覆盖的 lcm 超过 10000。已接入 formal-conjectures，Lean 已核。arXiv:2607.25628（2026-07）

怎么打

• 线 A · 搜例子 — 在 N > 10000 的奇丰富周期上，从大于 1 的奇因子中选互异模，搜索覆盖 ℤ/Nℤ。硬约束写进搜索器，赤字逐 N 记录。
• 线 B · 证不存在 — 复用密度、丰富数分类与逐 N 的 CRT 容量证书，寻找不依赖具体上限的结构引理，写成全称命题并过 Lean。
• 四个角色 — Auditor 对题查库；Prover 出例子或论证；Formalizer 写 Lean 4、lake build 无 sorry；Claimant 按官方 PR 模板提交。