11:09
官方一手arXiv: Google DeepMind@Ibrahim Mian, Shayaan Siddique
推荐理由：DeepMind 用 Lean 4 把 Erdős-Selfridge 问题的一个下界（lcm>10000）变成了机器可检查的定理。对形式化数学和定理证明器感兴趣的话，这个工作很硬核。
覆盖问题
共 1 条相关 AI 资讯
7月29日
11:09
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。