Erdős Problem #306 · 高等证明逆向 · 阅读版

把 Tang 的 Lean 圆法证明
还原成人能读的数学

Yuren Tang 用 Lean 4 + Mathlib 给出了 Erdős #306 的完整、机器验证证明（Zenodo 10.5281/zenodo.20767390， GitHub Yuren-Tang/erdos-306 v0.0.3）。 它 sorry-free，只依赖两条经典素数论输入——但还没有写成论文（README：“A written mathematical account is in preparation”）。 本站从约 21,000 行 Lean 中逆向出数学结构，逐层讲清这台“机器”是怎么运转的。

Erdős Problem 306
设 $a/b\in\mathbb{Q}_{>0}$，且 $b$ 无平方因子（squarefree）。是否总存在整数 $1两个不同素数之积（$n_i=p_iq_i$，$p_i\neq q_i$），使得 $$\frac{a}{b}=\frac{1}{n_1}+\frac{1}{n_2}+\cdots+\frac{1}{n_k}\ ?$$ Tang 证明：是。
第一次看？先读「人人能懂版」
不想碰公式，只想搞懂这道题在问什么、以及高深证明的核心思路？ → 人人能懂版（只需小学分数）——用分数积木、旋转指针、主音压杂音三个画面把整条证明讲成人话，看完再回来读下面的技术细节会顺很多。
■ Lean 已证（kernel 保证） ■ 解析核心（圆法/能量–熵） ■ 命名公理（外部经典输入） ■ 待你决定的下一步

1. 题目什么意思？ semiprime / squarefree

半素数（squarefree semiprime）：两个不同素数的乘积 $n=pq$（$pIsSemiprime n，等价于算术函数 $\omega(n)=\Omega(n)=2$（不同素因子数 = 计重素因子数 = 2）。

无平方因子（squarefree）：$b$ 不被任何素数的平方整除。

为什么必须要求 $b$ squarefree？——这是必要条件
如果所有 $n_i$ 都是半素数，它们尤其都 squarefree，于是 $\mathrm{lcm}(n_1,\dots,n_k)$ 也 squarefree。任何有限和 $\sum 1/n_i$ 的既约分母都整除这个 lcm，因此本身 squarefree。 所以 $a/b$（既约）能被半素数单位分数表示 $\Rightarrow b$ 必 squarefree。题目要求 squarefree 正是刚好卡在可行的边界上。 （Lean：necessity_squarefree_denom，Defs.lean。）

Tang 证的是充分性：squarefree 就足以保证表示存在。而且更强——可以避开任意有限的“障碍集” $T$（denominators 全落在 $T$ 之外）。这个“可避开”版本是后面把 $a/b$ 拆成许多份 $1/b$ 时保证互不相同的关键。

2. 全局架构 the whole machine on one page

整条证明是一台三层的机器。顶层是纯初等的归约；中层是圆法正性引擎（一个抽象接口 ArcConstruction ⇒ 计数 $\mathrm{Wcount}>0$）；底层是真正把这个接口造出来的两根支柱，其中 minor-arc 的控制是全证明最硬的解析部分。所有数论只在最底层，通过两条 Rosser–Schoenfeld 公理进入。

顶层 · 归约（初等） 中层 · 圆法引擎（抽象） 底层 · 构造 + 解析核心 Erdős 306：每个 squarefree 分母的 $a/b$ 可表示 erdos_306 / erdos_306_unconditional 对分子 $a$ 归纳：拆成 $a$ 份互斥的 $1/b$ 对每个 $1/b$：造半素数表示（可避开 $T$） circle_method_positivity_R2 (b=1,2 特判) 存在子集 $S\subseteq E$，$\sum_{e\in S}1/e=1/b$ 圆法正性引擎：$\mathrm{Wcount}(E,\theta,b)>0$ Fourier 反演：$L\cdot\mathrm{Wcount}=\sum_{h Main arc（主项） Taylor + 高斯下界 $\ge c_3/\sigma_E$，正 $c_3=0.8\,e^{-\pi^2/2}/2$ Minor arc（误差） $\|\hat\mu(h)\|\le e^{-c\,Q_E(h)}$ 须证 $\ll 1/\sigma_E$（beat） Jordan：$\sin^2\!\ge\!4\|\cdot\|^2$ 引擎要求底层供给一个 ArcConstruction 支柱 ①：R2 构造 用 dyadic 素数块造边集与权重 $E=E_{\text{int}}\cup E_{\text{skel}}\cup E_{\text{mass}}\cup E_{\text{gad}}$ $\theta_e\in[\tfrac13,\tfrac23]$，质量恒等式 $\sum\theta_e/e=1/b$ lattice span $\gcd\{L/e\}=1$（无格障碍） exists_arcConstruction_final 支柱 ②：minor-arc 控制 Global Control Partition（Prop 8.1） 能量–熵 / Peierls：off-main ⇒ 能量高 SBEE 单块能量–熵（已证，非假设） CRT 能量 $Q_{\text{ctrl}}$、色散、fingerprint global_control_partition 耦合 两条命名公理（唯一的外部输入） Rosser–Schoenfeld 1962：dyadic 区间素数密度 · Mertens 和 $\sum_{p\le x}1/p$ rosser_schoenfeld_cor3 · rosser_schoenfeld_thm5
图 1 · 三层机器：初等归约（绿）→ 抽象圆法引擎（蓝虚线）→ 构造与 minor-arc 解析核心，所有数论收束到底部两条 Rosser–Schoenfeld 公理。

3. 第一层：从 $a/b$ 到一个正性问题 the elementary reductions

这一层在 Lean 里完全初等、完整无缺。它把原问题层层剥到“对单个 $1/b$ 证一条正性”。

3.1 $a/b\ \Rightarrow\ a$ 份 $1/b$（对分子归纳）

对 $a$ 做归纳。$a=0$ 用空集。$a\to a{+}1$：归纳假设给出表示 $a/b$ 的半素数集 $S$；对可避开版本取障碍集 $T=S$，得到一份新的 $1/b$ 表示 $U$，其分母与 $S$ 不相交；于是 $S\cup U$ 表示 $(a{+}1)/b$。可避开性正是让这 $a$ 份 $1/b$ 的分母两两不同的机关。 （Lean：reduction_to_unit_numerator_avoiding，MainTheorem.lean。）

3.2 小分母的基例 $b=1,2$

半素数的最小值是 $6$，所以 $1/1$、$1/2$ 不能直接由“$b\ge3$ 的机器”产出，需手工基例：

$$1=\tfrac12+\tfrac13+\tfrac16,\qquad \tfrac12=\tfrac13+\tfrac16,$$

而 $\tfrac13,\tfrac16$ 又回到 $b\ge3$ 的机器（$6=2\cdot3$ 本身是半素数，$1/3$ 走一般构造）。这些基例也全部保持“避开 $T$”。（Lean：egyptian_rep_eq2_R2、exists_semiprime_egyptian_one_R2。）

3.3 主战场 $b\ge3$

剩下的就是：给定 squarefree $b\ge3$ 和有限障碍集 $T$，找一组避开 $T$ 的半素数，其倒数和等于 $1/b$。这正是圆法引擎要解决的。

4. 第二层：圆法正性引擎 Wcount > 0

→ 逐引理详解见 圆法引擎详解页（Fourier 反演、主弧高斯下界、次弧字符衰减、拍频收口、正性抽取）。

思路是概率 + Fourier。给每条候选边 $e\in E$（一个半素数）配一个独立的 Bernoulli$(\theta_e)$ 开关 $\xi_e\in\{0,1\}$，被选中的边组成随机子集。定义加权计数

$$\mathrm{Wcount}(E,\theta,b)=\sum_{S\subseteq E}\Big[\textstyle\sum_{e\in S}\tfrac1e=\tfrac1b\Big]\ \prod_{e\in S}\theta_e\prod_{e\notin S}(1-\theta_e) =\ \mathbb{P}\!\Big(\sum_{e:\xi_e=1}\tfrac1e=\tfrac1b\Big).$$

只要证 $\mathrm{Wcount}>0$，就至少有一个子集 $S$ 真的满足 $\sum_{e\in S}1/e=1/b$——那就是要找的表示。（提取：exists_subset_of_Wcount_pos、Wcount_pos_imp_repr。）

Fourier 反演（引擎的主恒等式）
取一个公共模 $L$（$e\mid L$）。用有限正交性把示性函数展开，得到 $$L\cdot\mathrm{Wcount}=\sum_{h=0}^{L-1}\hat\mu(h)\,e(-h/b),\qquad \hat\mu(h)=\prod_{e\in E}\varphi_{\theta_e}(h/e),$$ 其中 $\varphi_\theta(t)=(1-\theta)+\theta e^{2\pi i t}$ 是 Bernoulli 特征函数，$|\varphi_\theta(t)|^2=1-4\theta(1-\theta)\sin^2(\pi t)$。 （Lean：wcount_fourier_identity，bernoulliCharFun。）

把频率 $h$ 分成两堆——主弧 (main arc) $S_M$（$h$ 使每个 $h/e$ 都接近整数）与次弧 (minor arc) $S_m$（其余）。正性来自“主项压过误差”：

4.1 Main arc：正的主项 $\asymp 1/\sigma_E$

在主弧上把 $\log\varphi_\theta$ 做二阶 Taylor（$\log(1-w)=-w-w^2/2+O(w^3)$），线性项因质量恒等式 $\sum\theta_e/e=1/b$ 恰好抵消相位，剩下一个高斯型的正实部。记方差 $\sigma_E^2=\sum_e\theta_e(1-\theta_e)/e^2$，则主弧实部有下界

$$\mathrm{Re}\sum_{h\in S_M}(\cdots)\ \ge\ \frac{c_3}{\sigma_E},\qquad c_3=0.8\cdot\frac{e^{-\pi^2/2}}{2}>0,$$

虚部按 $m\leftrightarrow -m$ 配对精确为 $0$。（Lean：bernoulli_log_taylor、main_arc_gaussian_lower、main_sum_re_lower。）

4.2 Minor arc：把特征衰减变成 CRT 能量

次弧上用 $|\varphi_\theta(t)|^2\le 1-c\sin^2(\pi t)$ 得乘积衰减 $\|\hat\mu(h)\|\le\exp(-c\sum_e\sin^2(\pi h/e))$。再用 Jordan 不等式 $\sin^2(\pi x)\ge 4\|x\|^2$（$\|x\|$=到最近整数距离）把它换成二次 CRT 能量

$$Q_E(h)=\sum_{e\in E}\big\|h/e\big\|^2,\qquad \|\hat\mu(h)\|\le \exp\!\big(-\tfrac{16}{9}\,Q_E(h)\big)\ (\theta_0=\tfrac13).$$

要收尾必须证明整个次弧的贡献远小于主项，即 beat 分离 $B_mproduct_charFun_bound_QE、minor_arc_bound、positivity_from_arcs。）

引擎的抽象接口 ArcConstruction
引擎本身不含任何数论：它是一条纯粹的“主项 > 误差 ⇒ 正”的推理。它把所有具体信息打包成一个结构 ArcConstruction 的字段：边集 $E$、权重 $\theta$、模 $L$、弧划分 $S_M/S_m$、质量恒等式、主弧的 CRT 双射、minor 界 $B_m$、以及关键的 hbeat：$B_mexists_pos_weighted_of_construction 消化这些字段，直接吐出 $\mathrm{Wcount}>0$。底层的全部工作，就是合法地填满这个结构。

5. 第三层：两大支柱 construction & minor-arc control

这两根支柱是全证明最重、最“高等”的部分。骨架如下，逐引理详解见 支柱①·R2 构造 与 支柱②·minor-arc/SBEE 两个详解页。

支柱 ①：R2 构造 Lean 已证

用 dyadic 素数块 $P_k=\{\text{primes in }[2^k,2^{k+1})\}$ 搭一个 BlockSystem，边集取这些块里两个不同素数的乘积（半素数），分成四族 $E_{\text{int}}$（块内）、$E_{\text{skel}}$（骨架）、$E_{\text{mass}}$（质量批次）、$E_{\text{gad}}$（gadget 微调），把权重 $\theta_e\in[\tfrac13,\tfrac23]$ 调到质量恒等式 $\sum_e\theta_e/e=1/b$ 精确成立。块可以从任意大的 $k_0$ 起步，于是能避开任意有限 $T$。质量下界（“乘积负载 $\ge 1/2$”）来自 Mertens 和 $\sum 1/p\ge 21/20$。

支柱 ②：minor-arc 控制 解析核心

要证次弧真的小，需要一条全局控制划分（Global Control Partition，对应文中 Prop 8.1）：任何“偏离主弧”的频率，其 CRT 能量都被顶到一个随块数增长的能量地板之上，从而其特征衰减 $e^{-cQ}$ 足够快、求和后可忽略。这背后是一套能量–熵 / Peierls 记账（label-charging：坏配置的“熵”被“能量”压过），核心引理是已被证明的 SBEE（Single-Block Energy–Entropy，单块能量–熵），配合色散引理与 per-vertex fingerprint 能量。

逐引理详解页已就绪

重要发现：SBEE 已无条件证明，靠“一个剩余类在 dyadic 区间至多命中 2 点”的初等区间计数，不需要 Irving 的 Kloosterman 界——后者只留在废弃的 SBEE.lean 与条件路径里，不在关键路径上。

6. 证明压在什么上？ the honest axiom & sorry ledger

这是审核一个形式化证明唯一真正需要人肉核对的地方：定理陈述对不对，以及它到底依赖哪些公理。结论令人放心：

整棵证明树：恰好 2 条非标准公理，0 个可达 sorry

审核入口：lake env lean RequestProject/Audit.lean 会打印定理陈述、#print axioms erdos_306 与两条公理原文；CI 每次 push 都重跑并 gate。

换句话说：只要你认可（a）Lean 定理 erdos_306 确实表达了 Erdős 306，（b）那两条公理忠实转写了 Rosser–Schoenfeld 1962——剩下的都由 Lean kernel 担保。这两点本站都给了逐条对照。

7. 原始材料 local archive

全部就地存档，方便你审核与下载：

来源：Zenodo 10.5281/zenodo.20767390 · GitHub Yuren-Tang/erdos-306（v0.0.3, commit e1c8711）· 作者 Yuren Tang（ORCID 0009-0006-0847-3330）。

8. 下一步 你来拍板

第一版已完整：总览 + 四个详解页（圆法引擎、构造、minor-arc/SBEE、公理）+ 原始材料就地存档，全部 HTML+SVG+TeX。整条证明已从约 21,000 行 Lean 逆向出人可读的数学结构。

接下来由你决定方向，可选项例如：

关于部署
域名 erdos306.shisheng.li 目前尚未上线。DNS 解析、nginx 配置、SSL 证书都是对外动作，我不会在你确认前擅自执行。你现在可以直接在本地打开 www/index.html 审核；确认无误并同意后我再上线。