结果族 004：Hilbert’s tenth problem over ℚ · 学科：Number theory（数论） · 验证状态：暂无形式化证明，请以社区核验为准
想象一台”方程判题机”：塞进去任何整系数多项式，它都能回答”这方程有没有有理数解”。希尔伯特 1900 年为整数解提出这个愿望，1970 年被证明落空——机器造不出来。有理数版本又悬了五十多年，这篇论文给出同样的否定答案：在分数的世界里，判题机也永远造不出来。
关键词卡片
看个具体例子
有的方程一眼能判：@@M@@x^2+y^2+3=0@@ 没有有理解，因为左边恒为正。难的不是单个方程，而是”统一机器”：论文证明不存在算法对所有多项式（变量个数也任意）作答，而且你无法事先知道哪个多项式属于”答不出”的那类。归约思路是：假如有理判题机存在，就能拼出整数判题机，与 1970 年的著名否定结论矛盾。
为什么值得关心
这是数理逻辑与数论（椭圆曲线、模形式、Shimura 曲线、Green–Tao–Ziegler 素数定理）深度联手的成果，补上了丢番图不可判定版图上最大的空白。
暂无形式化证明（AI 结果待核验）
第一级台阶
导读的”判题机”里，对象是整系数多项式方程，操作是问它在分数世界里有没有解。归约思路是：假如分数判题机存在，就能拼出整数判题机，而 1970 年已证明整数判题机造不出来——于是分数机也造不出来。导读强调：难的不是某个方程，而是”统一机器”。
第二级台阶
精确化概念：一个整数关系称递归可枚举，指算法能逐一列出其全部解；称丢番图，指可表为”存在额外整数满足一个多项式方程”。DPRM–Matiyasevich 定理断言二者等价，整数情形因此不可判定。转到 ℚ 上，枚举总能找到存在的有理零点，却无法证明不存在——判定难点恰在否定侧。典范高度则是椭圆曲线上衡量点”大小”的标尺，随点指标平方增长。
第三级台阶
定理 1.1 的语境：最直接路线是只用存在量词在 ℚ 中定义 ℤ，但 Robinson、Poonen、Koenigsmann 的定义都离不开全称量词，Mazur 猜想甚至暗示丢番图式定义不可能——这条门被堵死。论文改走”有限测试”归约：对每个 f 有效枚举一列测试，f 有整数零点当且仅当全部测试通过；模型论（紧性定理）与算术（秩一椭圆曲线、Green–Tao–Ziegler 素数模式、五点高度估计）联手证明无整数零点时必有测试失败，收官靠高度平方增长与线性上界相矛盾。结论无附加假设，且第 7 节加强到图灵度 0’ 并给出四次正规形式。
论文证明 ℚ 上的希尔伯特第十问题（Hilbert’s tenth problem over ℚ）有否定答案：不存在算法能判定整系数多项式（变量个数任意）是否有有理零点。这一悬置五十余年的难题，由椭圆曲线、模形式与高度理论的深度组合攻克。
1900 年希尔伯特提出第十问题：寻找有限步骤，判定整系数多项式方程有无整数解。Davis–Putnam–Robinson 与 Matiyasevich（1961/1970）证明每个递归可枚举（recursively enumerable）关系都是丢番图（Diophantine）的，整数情形因此不可判定。把未知数改为取值于 @@M@@\mathbb{Q}@@ 后，问题长期开放：枚举总能找到存在的有理零点，却无法证明不存在。最直接的路线是用纯存在量词在 @@M@@\mathbb{Q}@@ 中定义 @@M@@\mathbb{Z}@@，但 Julia Robinson（1949）、Poonen（2009）、Koenigsmann（2016）的定义都离不开全称量词，Mazur 的猜想甚至暗示丢番图式定义不可能。近年 Koymans–Pagano 等人无条件解决了所有数域整数环上的同类问题，但 @@M@@\mathbb{Q}@@ 不是有限生成 @@M@@\mathbb{Z}@@-代数，有理域本身一直悬而未决——本文补上了这块拼图。
主定理（Theorem 1.1）：不存在算法，给定 @@M@@f\in\mathbb{Z}[X_1,\ldots,X_n]@@（@@M@@n@@ 属于输入的一部分），判定 @@M@@f@@ 在 @@M@@\mathbb{Q}^n@@ 中是否有零点。等价地说，论文把整数可解性归约到有理可解性：若有理情形可判定，则由 DPRM–Matiyasevich 定理已知不可判定的整数情形也将变得可判定，矛盾。论文引言还指出，文末第 7 节把结论加强到图灵度 @@M@@0'@@，并给出四次正规形式（quartic normal form）。
整体骨架是”有限测试”归约。对每个非常数 @@M@@f@@，论文有效地枚举一列有限测试，每个测试只含有限多个有理可解性查询，并证明 @@M@@f@@ 有整数零点当且仅当全部测试通过。若有理可解性可判定，便可并行搜索整数零点与失败测试，必有一个终止，从而整数可解性也可判定，与 DPRM 矛盾。整数零点自然充当所有测试的见证；难点是证明 @@M@@f@@ 无整数零点时必有测试失败。
先看模型论一侧。假设全部测试通过，紧性定理（compactness theorem）给出 @@M@@\mathbb{Q}@@ 的初等扩张（elementary extension）@@M@@{}^*\mathbb{Q}@@，其中嵌着环 @@M@@R@@ 与 @@M@@f@@ 的零点 @@M@@\mathbf a@@。理论给每个 @@M@@a\in R@@ 指派椭圆曲线 @@M@@E:\ y^2=x^3-d^2x@@（@@M@@d=75-53\sqrt2\in\mathbb{Q}(\sqrt2)@@）上的点 @@M@@T_a@@，满足 @@M@@T_{a+a'}=T_a+T_{a'}@@、@@M@@T_1=P@@、@@M@@a\ne0\Rightarrow T_a\ne O@@。第 5 节用二同源下降（two-isogeny descent）算出 @@M@@E(\mathbb{Q}(\sqrt2))@@ 秩为 1，故有 @@M@@m@@ 与非挠点 @@M@@P@@ 使 @@M@@mE(F)=\mathbb{Z} P@@，于是 @@M@@\widetilde T_a=\eta(a)P@@，指标 @@M@@\eta(a)\in{}^*\mathbb{Z}@@。@@M@@\eta@@ 加性、单射且 @@M@@\eta(1)=1@@，但不必保持乘法——这是核心障碍。
再补三项算术输入。局部比较引理合并两条测试：截断形式对数（formal logarithm）@@M@@\ell_K@@ 之比在好素数处以精度 @@M@@K@@ 逼近 @@M@@\widetilde a@@，共轭曲线 @@M@@E^\sigma@@ 上的参数赋值比保证指标比在该处可积，合起来给出 @@M@@v_q(\widetilde a-\eta(a))\ge K@@。第 6 节用 Green–Tao–Ziegler 线性素方程定理配合 Selberg 上界筛证明素数模式：任意整数都可写成三个分数之和，使十三个接触形式的值全为 @@M@@\pm kr@@（@@M@@k@@ 属固定有限集，@@M@@r@@ 为大分裂素数），测试因此在整数模型中可满足。第 3 节构造正存在公式 @@M@@\Phi@@ 排除固定素数外的奇极点，证明依赖 @@M@@y^2=x(x-l)(x+3l)@@ 型曲线的 Selmer 群（Selmer group）@@M@@\F_2@@-矩阵计算、姊妹篇的点态 2-逆定理与 Cassels–Tate 配对。
最后以高度矛盾收官。第 4 节证明五点高度估计 @@M@@h(s)\le HM(s)^c@@（@@M@@M(s)@@ 为与固定五个有理点奇接触的素数之积）：几何上取判别式 210 的不定四元数代数（quaternion algebra）对应的 Shimura 曲线——亏格 5，Atkin–Lehner 商为 @@M@@\mathbf P^1@@，恰五个有理分支值——及其上带四元数乘法的阿贝尔曲面族；算术上经”奇正则 Fontaine–Mazur”模性（modularity）定理、导子估计与定量同源定理完成。令 @@M@@\delta=f(\eta(a_1),\ldots,\eta(a_n))@@：若 @@M@@\delta=0@@，初等性直接给出普通整数零点；否则 @@M@@|\delta|\le C_fB^D@@（@@M@@B=\max|\eta(a_j)|@@），取 @@M@@K\ge cD@@ 后，一切表示式的接触素数均 @@M@@K@@ 次整除 @@M@@\delta@@，高度估计给出 @@M@@h(\widetilde A)\ll_f B@@（一切 @@M@@A\in R@@）。用于 @@M@@x(T_{a_j})@@ 的坐标得 @@M@@h(x(\eta(a_j)P))\ll_f B@@，而典范高度（canonical height）随指标平方增长，故 @@M@@B^2\ll_f B@@，各 @@M@@\eta(a_j)@@ 被逼入普通有限区间，均为普通整数；由 @@M@@\eta@@ 加性单射，@@M@@a_j@@ 即这些整数，@@M@@f@@ 有整数零点，与 @@M@@\delta\ne0@@ 矛盾，定理得证。
本文暂无 Lean 形式化证明，验证状态以社区核验为准。证明横跨模型论、椭圆曲线、Shimura 曲线与解析数论，多处调用极深的外部工具（Green–Tao–Ziegler 定理、定量同源定理、模性定理），核验门槛很高。同族姊妹篇《A pointwise 2-converse for elliptic curves with rational two-torsion》所证的 2-逆定理，正是第 3 节把 Selmer 类实现为有理点的关键输入，两篇互为支撑。按 OpenAI 官方声明，未经形式化的结果可能存在问题。
问 1：证明里最脆弱的一环是什么？
答：高度矛盾的”指数一致性”。收官需要 h(ã)≪_f B 对一切环元素一致成立，这依赖五点高度估计 h(s)≤HM(s)^c 中的指数 c 在扩大例外素数集后不变（第 1.2 节明言”Enlarging the exceptional set changes the height constant but preserves the exponent”）。若某处局部比较悄悄把 c 抬高一次，B²≪B 便退化为 B²≪B^{1+ε}，矛盾消失。整条高度链条的每个环节都必须守住同一个 c。
问 2：η 只加性不乘性，为什么还能导出矛盾？
答：这正是设计的精妙处：乘性缺失由两组局部比较补回——截断形式对数之比在好素数处以精度 K 追上指标，共轭曲线上的参数赋值比保证该比可积，合起来得 v_q(ã−η(a))≥K。再让一切接触素数 K 次整除 δ=f(η(a₁),…,η(a_n))，高度估计遂把 ã 的大小锁进 δ 的多项式界，最终用典范高度的平方增长夹死 B。
问 3：为什么不走”在 ℚ 中存在地定义 ℤ”这条直路？
答：引言花大量篇幅解释：Julia Robinson、Poonen（两个全称加七个存在）、Koenigsmann（全称定义）都绕不开全称量词；Mazur 猜想若真则连丢番图模型都不存在。判定问题并不要求解机器产生定义或模型——本文的有限测试接口（式 intro:finite-test-interface）绕开定义问题本身，这是与全部前人工作的根本区别。
问 4：与 Koymans–Pagano、Alpöge–Bhargava–Ho–Shnidman 相比新意何在？
答：那些结果解决的是数域整数环（无限有限生成 ℤ-代数）上的不可判定性；ℚ 不是有限生成 ℤ-代数，整条”整数环程序”够不着它。EMPS 的子环 Z[S^{-1}] 与 ℚ 的图灵等价性也只对特定子环成立。本文直接处理有理数域本身，且无条件。
问 5：外部输入有多深、AI 证明风险在哪？
答：极深：Green–Tao–Ziegler 线性素方程、Selberg 筛、奇正则 Fontaine–Mazur 模性定理、判别式 210 的 Shimura 曲线几何，以及姊妹篇的点态 2-逆定理加 Cassels–Tate 配对（第 3 节）。姊妹篇本身未形式化，是整栋楼的地基之一。AI 长文典型风险在”紧性转移”处：把普通整数模型的素数模式与高度估计搬进初等扩张 *ℚ 时，每个固定有限集、每个常数的依赖关系必须逐项核对，静默滑动一处即告失效。
问 6：下游推论是什么？
答：第 7 节把结论加强到图灵度 0’（判定难度恰停在停机问题一层）并给出四次正规形式。更大图景上，它补齐了丢番图不可判定版图上最大的空白——ℚ 这一基本数系的判定问题尘埃落定，后续方向只剩 ℂ(t)、p-进域等零星堡垒。
总评
这是数理逻辑与数论（椭圆曲线、Shimura 曲线、解析素数定理）空前深度的联姻，若核验通过则是里程碑级的否定解答；但其证据链横跨五六个领域且站在未形式化的姊妹篇之上，任何一环的精度滑动都会拆掉高度矛盾，社区核验前宜按”重大但待证”对待。