素数奇偶性新算法细节：1 次 SAT 查询与 85 万区间数值验证

xennygrimmato_ · x · 2026-11-06

作者补充前述素数计数奇偶性算法的关键数据：时间复杂度从 x^(1/2+o(1)) 降至 x^o(1)；适用于任意区间 [A, B] 而非仅短区间；整个过程只需向 Anthropic 的 #SAT 引擎发起 1 次查询；形式化证明为 5,488 行 Lean 4（用 Claude Code 写成），0 个 sorry、仅 3 条标准公理，并对 855,150 个区间做了数值检查。

核心思路：Polymath4（Tao、Croot、Helfgott）在短区间上求得了奇偶性，但需要对每个 d ≤ √x 计算 Möbius 函数 μ(d)；关键洞察是 mod 2 意义下 μ(d) 等价于判断 d 是否无平方因子——同一问题规模减半，应用 log n 次后 π(x) mod 2 化为一次计数。