结果族 020：Squarefree quartics and power-free polynomial values · 学科：Number theory · 验证状态：主结果已 Lean 形式化
多项式像一台吐整数的机器，”干净的”整数指不含任何素数平方因子（30=2·3·5 干净，12=2²·3 不干净）。这篇论文给四次机器做了完整体检：干净输出所占的比例，恰好等于每个素数处”存活率”的连乘。Erdős 1953 年以 n⁴+2 为例提出的无平方值问题就此解决，结论还覆盖 4 至 8 次多项式的 (d−2)-幂自由值。
关键词卡片
看个具体例子
看 n⁴+1（无固定平方因子的不可约四次式）：n=1,…,5 时输出 2, 17, 82, 257, 626，个个干净。定理说 @@M@@\#\{n\le X:\ n^4+1\ \text{无平方}\}=c_8X+o(X)@@，其中 @@M@@c_8=\prod_{p\equiv1\ (\mathrm{mod}\ 8)}(1-4/p^2)>3/4@@。原因很直观：只有 p≡1 (mod 8) 型素数能让 p² 整除 n⁴+1，且模 p² 恰有 4 个解，其余素数从不添堵。
为什么值得关心
此前的方法最多只能处理 9 次以上的多项式，四次恰好卡在临界指数 d−2 的方法极限上；论文靠数域分解、自适应行列式估计与低次几何三件工具啃下了它，并与 Browning 的高次定理合并，覆盖一切次数 ≥4 的多项式。
已 Lean 形式化
第一级台阶
导读把多项式想成”吐整数的机器”、”干净”指输出不含素数平方因子。换成半数学语言：对象是一台固定的机器（整系数多项式）和它随输入 n 逐个吐出的整数流；操作是逐个检查输出是否被某个素数的平方（或更高幂）污染，并统计未被污染的输入所占比例。猜想是：这个比例恰好等于”每个素数单独作案时存活率”的连乘——局部障碍互不打架。
第二级台阶
用本科术语：整数 a 称为 k-幂自由，若没有素数幂 p^k 整除 a；给定 Q 上不可约的 d 次整系数多项式 f，记 ρ_f(q) 为 f 模 q 的解个数，S_{f,k}(X) 为 1≤n≤X 中使 f(n) 为 k-幂自由的 n 的个数。必要条件”无固定 k 次幂因子”即每个素数 p 满足 ρ_f(p^k)<p^k，它排除了机器天生的污染；预测密度是 Euler 乘积，每个素数贡献存活比例 1−ρ_f(p^k)/p^k。
第三级台阶
定理 1.2 的语境：次数 4≤d≤8、取临界指数 k=d−2，在上述必要条件下 S_{f,k}(X)=c_{f,k}X+o_f(X)。不可约性挡住了”因子各自污染”的退化，不要求本原与首项系数为正则是结论的加强。全部难点集中在大素数尾部：使某个素数 p>X 整除 f(n) 的 k 次幂的 n 仅 O_f(X^{1−δ}) 个（尾部命题）。证明走数域路线：取 f 的根 θ 与域 K=Q(θ)，用理想分解与狄利克雷单位定理把 f(n)=yp^k 翻译成整元方程 α^kβ=μ(n−θ)，再对小盒对做阿基米德行列式切割、格基约化，并用自适应选取的辅助素数逐次降维计数；四次情形还须对困难曲面与曲线作显式低次几何分析。
每个无固定素数平方因子的不可约整系数四次多项式都按预期的正 Euler 乘积密度取无平方值——Erdős 1953 年提出的 @@M@@n^4+2@@ 无平方性问题就此解决；同时对 4–8 次不可约多项式建立 @@M@@(d-2)@@-幂自由值密度，并入 Browning 定理后覆盖一切次数 @@M@@d\ge4@@。
整数 @@M@@a@@ 称为 @@M@@k@@-幂自由（@@M@@k@@-power-free），若没有素数幂 @@M@@p^k@@ 整除它。给定整系数多项式 @@M@@f@@，经典的幂自由值问题问：当 @@M@@n@@ 取遍正整数时，@@M@@f(n)@@ 为 @@M@@k@@-幂自由的频率是否恰为各素数处局部存活比例的乘积？显然的必要条件是没有固定素数 @@M@@k@@ 次幂因子，即对每个素数 @@M@@p@@ 有 @@M@@\rho_f(p^k)<p^k@@，其中 @@M@@\rho_f(q)@@ 为 @@M@@f@@ 模 @@M@@q@@ 的根数。这个问题历史久远：Ricci（1933）处理 @@M@@k\ge d@@，Erdős 与 Hooley 解决指数 @@M@@d-1@@，Nair（1976）降到 @@M@@k\ge(\sqrt2-\tfrac12)d@@，Heath-Brown 与 Browning 的行列式方法（determinant method）进一步降到 @@M@@k\ge(3d+1)/4@@，但仍只能覆盖 @@M@@d\ge9@@。四次多项式的无平方值恰是临界指数 @@M@@k=d-2@@ 的第一个未解情形：Erdős 1953 年即以 @@M@@n^4+2@@ 为例，1965 年综述中再次指出 @@M@@d-2@@ 处的障碍。Granville 证明 @@M@@abc@@ 猜想可推出预测密度，而无条件结果一直缺失。
主定理（Theorem 1.2）：设 @@M@@f\in\mathbb{Z}[x]@@ 在 @@M@@\mathbb{Q}@@ 上不可约、次数 @@M@@4\le d\le8@@，取 @@M@@k=d-2@@。若对每个素数 @@M@@p@@ 有 @@M@@\rho_f(p^k)<p^k@@，则
@@M@@DS_{f,k}(X)=c_{f,k}X+o_f(X),\qquad c_{f,k}=\prod_p\Bigl(1-\frac{\rho_f(p^k)}{p^k}\Bigr)>0,@@
其中 @@M@@S_{f,k}(X)@@ 统计 @@M@@1\le n\le X@@ 中使 @@M@@f(n)@@ 为 @@M@@k@@-幂自由的 @@M@@n@@。定理不要求 @@M@@f@@ 本原（primitive），也不要求首项系数为正；误差项不宣称随 @@M@@f@@ 一致。@@M@@d=4@@ 时 @@M@@k=2@@，即无平方值（squarefree values）密度定理；@@M@@5@@ 至 @@M@@8@@ 次分别排除 @@M@@3,4,5,6@@ 次幂。两个推论随之而来：其一（Corollary 1.4），并入 Browning 的高次定理后，对一切次数 @@M@@d\ge4@@ 的不可约 @@M@@f@@，@@M@@(d-2)@@-幂自由值密度成立；其二（Corollary 1.6），对有限族可分离（separable）多项式给出”同时 @@M@@k@@-幂自由”的联合 Euler 乘积密度。实例：@@M@@T^4+1@@ 的模 @@M@@p^2@@ 根数当 @@M@@p\equiv1\pmod8@@ 时为 @@M@@4@@、否则为 @@M@@0@@，故密度为 @@M@@c_8=\prod_{p\equiv1\,(\mathrm{mod}\ 8)}(1-4/p^2)>3/4@@，即超过四分之三的 @@M@@n@@ 使 @@M@@n^4+1@@ 无平方。
全文骨架是”大素数尾部估计＋筛法转移”。筛法转移（第 2 节）先固定 @@M@@Y@@：对 @@M@@p\le Y@@ 的条件用中国剩余定理（Chinese remainder theorem）逐类精确计数，中间素数 @@M@@Y<p\le X@@ 至多贡献 @@M@@O(XY^{1-k}+\pi(X))@@；先令 @@M@@X\to\infty@@ 再令 @@M@@Y\to\infty@@，两级极限给出精确的 Euler 乘积，内容（content）素数处的局部因子按 @@M@@1-\rho_g(p^{k-e})/p^{k-e}@@ 精确保留。于是全部难点集中于尾部命题：使某素数 @@M@@p>X@@ 满足 @@M@@p^k\mid f(n)@@ 的 @@M@@n\in(X,2X]@@ 只有 @@M@@O_f(X^{1-\delta})@@ 个。
把素数按二进区间 @@M@@[P,2P]@@ 分档，记 @@M@@\eta=\log P/\log X@@、@@M@@b=d-k\eta@@。当 @@M@@\eta@@ 较小时走直接路线：三元组 @@M@@(n,f(n)/p^k,p)@@ 落在曲面 @@M@@f(x)=yz^k@@ 上，坐标量级为 @@M@@X,X^b,X^\eta@@；算出其上多项式函数空间的加权 Hilbert 函数主项，配合作者自证的一般仿射计数定理，得 @@M@@O(X^{1/2+\delta_2+\eps})@@ 且 @@M@@\delta_2<0.4999@@。其余区间走数域路线，这是本文核心：设 @@M@@\theta@@ 为 @@M@@f@@ 之根、@@M@@K=\mathbb{Q}(\theta)@@，用理想分解与狄利克雷单位定理（Dirichlet unit theorem）得整元 @@M@@\alpha,\beta@@ 满足 @@M@@\alpha^k\beta=\mu(n-\theta)@@，且各嵌入下 @@M@@\alpha,\beta@@ 的大小分别约为 @@M@@P^{1/d}@@ 与 @@M@@X^{b/d}@@。先在固定整基下得到两个坐标盒，再把射影方向切成成对小盒；对每对小盒做阿基米德行列式论证，得出点集上的多项式方程，并区分”混合方程”与”纯方程”——纯方程还会削减局部行列式中独立的泰勒单项式个数。继而用格基约化把整坐标缩小，异常短的格向量被证明只出现在极少数盒子中。最后反复调用仿射计数定理：在小辅助素数的剩余类处使维数逐次下降，辅助素数随先前选择自适应，随机删除论证控制坏素数；有限份”参数证书”（第 10 节）保证最终指数 @@M@@<24979/25000@@，留下一致的幂省。
四次情形还需精细几何（第 8、9 节）：困难曲面的投影次数只能是 @@M@@1@@ 或 @@M@@2@@，二次情形提供额外的域次数增益；平面情形若界不足，会同时逼出矛盾——要么一般直线上次数至多 @@M@@4@@ 的多项式有 @@M@@4@@ 个不同临界点与临界值（其导数至多三次，不可能），要么方向线上的二次有理映射有 @@M@@4@@ 个不同临界值（与次数 @@M@@2@@ 矛盾）。曲线的极限情形是带 @@M@@4@@ 个指定临界值的五次多项式：把两个临界点归一到 @@M@@0,1@@ 后只有有限多个，其整数值全体大小 @@M@@O_f(X^{1/5})@@，在区间求和之前一次性剔除。第 13 节以 @@M@@T^4+1@@ 为范例：@@M@@\mathbb{Z}[\zeta_8]@@ 是欧氏环，分解 @@M@@A^2B=n-\zeta@@ 用单位 @@M@@1+\sqrt2@@ 平衡，最大素数段交给 Pell 型方程 @@M@@n^4+1=Dq^2@@ 的 @@M@@O(1+\log N)@@ 解数估计。最后对 @@M@@O_f(\log X)@@ 个素数区间求和，完成证明。
任务元信息显示该主结果已有 Lean 形式化证明（结果族 020 的文档 lean/docs/020.md），这是目前最强的核验等级；且作者刻意不把 Carella 与 Zapata Ceballos–Jalalvand 的两份相关声明当作定理输入，大素数估计与筛法转移均系独立证明。需留意第 13 节分圆范例中的解析关系估计是条件性结论，依赖其所列假设。按 OpenAI 官方声明，未经形式化的结果可能有问题；本文主结果不在此列。族内本文与 Browning 高次定理互补，合并后覆盖全部 @@M@@d\ge4@@。
问 1：证明的命门在哪里？
（答：大素数尾部命题（prop:large-prime-tail）。筛法转移把密度定理整个归约到它，而它的证明是长级联：数域分解给出 α^kβ=μ(n−θ)、射影方向切成成对小盒、阿基米德行列式给出多项式方程、区分混合方程与纯方程（后者额外削减局部泰勒单项式）、格基约化缩短整坐标、最后反复调用均匀仿射计数定理——辅助素数随先前选择自适应，随机删除论证控制坏素数。任何一环的指数账算错，尾部省不够就全线崩。）
问 2：哪些假设是真正不可去的？
（答：局部可许性 ρ_f(p^k)<p^k 必要——违反它意味着某 p^k 整除一切值，存活率为零。定理限定 4≤d≤8 并非本质：k=d−2 在 d≤3 时退化（d=3 给 k=1，无素数因子者仅 ±1），d≥9 则由 Browning 的 k≥(3d+1)/4 直接覆盖（Corollary 1.4），四次到八次恰是无条件方法的空白带。误差项对 f 不一致、无幂省——论文明言这是两级极限次序（先 X→∞ 再 Y→∞）的代价。）
问 3：与已有工作相比新意何在？
（答：历史线是 Ricci（k≥d）→ Erdős–Hooley（d−1）→ Nair（(√2−1/2)d）→ Heath-Brown（(3d+2)/4）→ Browning（(3d+1)/4，d≥9），临界指数 d−2 自 Erdős 1953 年点出 n⁴+2 后悬置七十余年。方法上本文沿 Reuss 的”数域因子分解＋逼近行列式”框架，但均匀仿射计数定理、显式加权 Hilbert 计算与四次曲面/曲线的几何论证系自证。论文还明确不把 Carella 与 Zapata Ceballos–Jalalvand 的相关声明当输入，大素数估计独立给出。）
问 4：AI 生成证明在这篇上最可能的出错模式？
（答：指数账。第 10 节参数选择与第 12 节”参数证书”给出 24979/25000 这类显式有理数指标，混合/纯方程的区分影响独立单项式计数，自适应辅助素数的随机删除涉及坏素数概率上界——这类数值级联论证是 AI 最容易”看起来对”的地方。缓解因素：本文主结果已 Lean 形式化（formalized: true），是本批结果中核验等级最高的；但第 13 节分圆范例的解析关系估计仍是条件性结论，不在形式化覆盖内。）
问 5：四次情形到底难在哪，论文怎么破？
（答：四次曲面的困难投影次数只能是 1 或 2，二次情形借域次数增益；平面情形若界不足会同时逼出矛盾——一般直线上次数至多 4 的多项式不可能有 4 个不同临界点（导数至多 3 次），或方向线上的二次有理映射不可能有 4 个不同临界值；曲线极限情形归为带 4 个指定临界值的五次多项式，归一化后只有有限个，其整数值 O(X^{1/5})，求和前一次性剔除。）
问 6：谁会用到它？
（答：幂自由值问题的直接推进——与 Browning 合并后覆盖一切 d≥4 的 (d−2)-幂自由密度；可分乘积与族的同时幂自由推论（Corollary 1.6）服务于多多项式联立筛法；在 Granville 的 abc 蕴含（对该类多项式）意义上，这是 abc 的无条件兑现。Erdős 1953 的 n⁴+2 与 n⁴+1（第八分圆多项式）两个样板问题随之落定。）
总评
（临界指数上七十年老题的完整解决、且经 Lean 形式化，可信度罕见地高；剩余风险集中在形式化未覆盖的分圆范例与”参数证书”式数值论证的核验。）