定理证明器相关 AI 资讯 · AI 热点

7月29日

11:09

11:09

官方一手arXiv: Google DeepMind@Ibrahim Mian, Shayaan Siddique

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。

论文 Erdős-Selfridge Lean 4 形式化验证

推荐理由：DeepMind 用 Lean 4 把 Erdős-Selfridge 问题的一个下界（lcm>10000）变成了机器可检查的定理。对形式化数学和定理证明器感兴趣的话，这个工作很硬核。

6月12日

09:44

09:44

官方一手arXiv: DeepSeek@Joshua Ong Jun Leang, Zheng Zhao, Mihaela Cătălina Stoian, Qiyuan Xu, Haonan Li, Wenda Li, Shay B. Cohen, Eleonora Giunchiglia

精选73°

Pythagoras-Prover 是一个计算高效的 Lean 定理证明器系列，包含 4B 和 32B 参数的自回归模型，以及首个基于扩散的证明器（4B）。通过课程式监督微调和动态证明过滤，训练效率大幅提升。其 4B 模型在 MiniF2F-Test 上以 86.1% 的 pass@32 超越 DeepSeek-Prover-V2-671B（82.4%），参数减少约 167 倍；32B 模型达到 93.0%，创下开源新纪录。团队还提出了增强型 Lean 形式化方法（ALF），通过扰动已知问题生成变体，减少对表面形式的依赖，并发布了 MiniF2F-ALF 基准。

论文定理证明器 Lean Pythagoras-Prover

推荐理由：形式化证明领域终于有了计算高效的实用方案——4B 模型就能超越 671B 巨无霸，做定理证明或形式化验证的团队可以直接用，省下大量算力成本。